Contract Automata: A Specification Language for Mode-Based Systems

The comprehensive, understandable and effective formal specification of
complex systems is often difficult, especially for reactive and interactive
systems like web services or embedded system components.
In this paper, we propose \emph{contract automata}, a new specification
formalism for describing the expected behaviour of stateful systems. Contract
automata combine two established concepts for formal system specification:
contract-based specification and nondeterministic finite state automata.
Contract automata restrict the effects that the operations of the specified
system may have using input-output-contracts. The automaton structure of a
contract automaton describes when contracts are applicable.
Contract automata support the refinement and composition of reactive systems,
enabling modular verification of systems assembled of multiple subsystems.
In this paper, we formally define the semantics of contract automata based on
a two-party game between the system under test and its environment.
We define the proof obligations and present techniques to prove a refinement
relationship between contract automata, the validity of system compositions, and
... mehr
the compliance of source code against a contract automaton.
We provide a tool for the generation of the proof obligation that can be
discharged with model-checkers or static program analyses.
We exemplify the use of contract automata by presenting the specification and
verification of an emergency brake assistant.