A process for specifying black box behavior, demonstrated in a case study

Prior to designing a system, customers and contractors should agree on required black box (externally apparent) system behavior. To define this behavior, practical, precise, design independent methods are needed. This paper describes results of a case study in which formal event-based approaches are used, demonstrating that a combination of history based traces and guarded event-action statements is practical for defining black box behavior. Externally apparent modes (states) simplify the specification to promote human understanding. The specifier is allowed to use both traces and event-action statements in a single specification, as requirements that define sequential events are best specified using traces, and requirements that are conditional are best specified using event-action statements. Graph generation from the model, as opposed to graph definition makes this type of specification easier to define and maintain