Enhanced system abstractions (ESA): Semantics, methodology, and examples

The existing system abstraction (SA) specification approach is described and demonstrated via an example. An existing set of criteria requirements for reactive system specification approaches is modified and SA is assessed with respect to the modified criteria. This assessment highlights the strengths and weaknesses of the SA approach for reactive system specification.;A set of enhancements is proposed that improves the approach without degrading the desirable application aspects of SA that can be traced to its emphasis on informal specification. Specifically, the set of enhancements introduces a modified event specification approach that highlights enabling conditions and allows for the specification of exceptions. It also introduces a new construct called a constraint that allows one to gradually integrate requirements into a specification and to specify properties such as liveness that have traditionally been difficult to include in a specification. The resulting specification approach is referred to as Enhanced System Abstractions (ESA). A rigorous semantic definition of an ESA specification based on an abstract syntax and explicit computational model is provided. An example graphics window-dragging reactive system specification is used to demonstrate these enhancements.;A methodology is then proposed that allows one to use informal customer requirements as the basis for an iterative refinement toward an ESA functional specification. The informality associated with an ESA specification is shown to ease this task by providing a framework amenable to information exchange with one's customer. The formalized structure of an ESA specification is also shown to ease the transition to a formal specification during subsequent development. The methodology is demonstrated on an actual set of customer requirements for an RS-232 repeater device. Specifically, the original requirements are expressed as ESA constraints and a functional specification in terms of variables, states, and events is derived from these constraints.