A FRAMEWORK AND PATTERNS FOR THE SPECIFICATION OF REACTIVE SYSTEMS

Frameworks have become popular as a vehicle for reuse of solutions in specific areas of application. We have extended the application of fra meworks to record and transmit our experience of applying formal speci fication methods. In this paper we deal specifically with dual approac hes to the specification of reactive systems. A dual approach uses a n otation for the specification of behaviour, preferably a graphical one , and a temporal logic to express formally, and reason about, this beh aviour. The combination of two representation schemes forms the basis of a generic framework that can be instantiated for any choice of nota tions. Two instantiations of the framework, illustrating its use, are discussed. To describe in detail one of the instantiations, the ArchSM method, we use the a pattern template. (C) 1998 Elsevier Science B.V.