A mode-aware contract language for reactive systems

Abstract

Contract-based software development is a major methodology for the development of safety- and mission-critical embedded systems. Contracts are an effective mechanism to establish boundaries between components, and can be used efficiently to verify global, systemlevel properties by means of compositional reasoning techniques. A contract specifies the assumptions a component makes on its environment, and the guarantees it provides. Requirements in a component’s specification are often case-based, with each case referring to a particular behavioral mode for the component. This talk introduces CoCoSpec, a mode-aware assume-guarantee-based contract language for embedded systems. CoCoSpec, which is built as an extension of the synchronous data-flow language Lustre, lets users specify mode behavior directly, thus preserving mode-specific information contained in (natural language) system requirements. Mode-aware model checkers supporting CoCoSpec can increase the effectiveness and scalability of compositional analysis techniques based on the assume-guarantee paradigm. In particular, they can leverage the fine-tunable abstraction mechanism provided by modes in order to selectively abstract complex numerical operations by their contracts, thus facilitating the verification of systems with numerical components. The talk presents the CoCoSpec language and illustrates the benefits of mode-aware model-checking on a case study involving a flight-critical avionics system. The evaluation uses Kind 2, a collaborative, parallel, SMT-based model checker developed at the University of Iowa that provides full support for CoCoSpec.