A Metalanguage for the Formal Requirement Specification of Reactive Systems

The essential novelty of what we have presented lies in the possibility of specifying within the same formalism requirements about the static structure and the dynamic activity of a system. Compared to the many formalisms using various forms of temporal logics, we have two distinguished features: the possibility of dealing both with different entities (of different sorts) and with the subcomponents of an entity, without lowering the abstraction level of a specification; moreover our formalism includes the usual specifications of abstract data types and it allows also to give integrate specifications of the dynamic and of the static features of a system. The formalism has a clean mathematical support in the definition of an appropriate institution; to this end a key role is played by the definition of the class of models, which are entity algebras over extended signatures. There is no room here for illustrating the possibility of relating such abstract requirement specifications to the design level specifications (e.g. the SMoLCS specifications of [2]); this can be done following an algebraic approach based on a notion of implementation, due to Sannella-Wirsing [22] (see [8, 4] for some examples). Finally it may be of interest to mention the fact that the approach presented here is currently being used in some industrial case studies for relating requirements to more concrete design specifications, which have been already given (see Section 5.2).