Formal specification and temporal proof techniques for mixed systems
Jean-Claude Royer · 2005
Formal specifications of mixed systems are one of the main issues in software engineering. However several diffi-culties remain. Amongst them is the ability to produce a co-herent mixed specification and to provide a fully integrated semantics. This paper presents a proposition trying to cope with this issue: the Graphic Abstract data Type (GAT) ap-proach. GAT is a mixed formalism based on Symbolic Tran-sition Systems (STSs) and algebraic specifications of partial abstract data types. The first part of this paper deals with the specification of a vending machine using the GAT ap-proach. The second part is devoted to prove temporal prop-erties on a GAT specification. Because it is a symbolic sys-tem with guards, variables and data values, classical model checking is not sufficient enough, furthermore the specified system is not bound. We rather advocate proofs with a gen-eral theorem prover and the use of functional operators ex-pressing temporal properties. We consider that properties are generally twofold, a simple part provable on the STS, considered as a classical finite state machine, and a sym-bolic part which needs a general theorem prover. We show several examples of properties and proofs. 1.