Modular Formal Specification of Data and Behaviour

Jaco van de Pol, Jozef Hooman and Edwin de Jong

Appeared in: Proceedings 1st Conference on Integrated Formal Methods (IFM'99), Springer-Verlag, pp. 109-128, 1999.

ABSTRACT

We propose a modular approach to the formal specification of the requirements on embedded systems. In this approach, requirements on data are specified as invariants on states. Requirements on behaviour are specified assertionally by temporal logic formulae, restricting the runs of the system. The proposed method is modular, because components can be specified and analyzed in isolation, and the views of several components can be combined in an easy way. Requirements can be combined by simply putting them in conjunction. A mathematical framework supporting this approach is developed and implemented in the theorem prover PVS. The method is illustrated by formalising the requirements of a miniature embedded system. This specification is then analysed using the theorem prover, revealing some errors in the original specification.