Book chapter
CoCoSpec: A Mode-Aware Contract Language for Reactive Systems
Software Engineering and Formal Methods, pp.347-366
Lecture Notes in Computer Science, Springer International Publishing
06/23/2016
DOI: 10.1007/978-3-319-41591-8_24
Abstract
Contract-based software development has long been a leading methodology for the construction of component-based reactive systems, embedded systems in particular. Contracts are an effective way to establish boundaries between components and can be used efficiently to verify global properties by using compositional reasoning techniques. A contract specifies the assumptions a component makes on its context and the guarantees it provides. Requirements in the specification of a component are often case-based, with each case describing what the component should do depending on a specific situation (or mode) the component is in. We introduce CoCoSpec, a mode-aware assume-guarantee-based contract language for embedded systems built as an extension of the Lustre language. CoCoSpec lets users specify mode behavior directly, instead of encoding it as conditional guarantees, thus preventing a loss of mode-specific information. Mode-aware model checkers supporting CoCoSpec can increase the effectiveness of the compositional analysis techniques found in assume-guarantee frameworks and improve scalability. Such tools can also produce much better feedback during the verification process, as well as valuable qualitative information on the contract itself. We presents the CoCoSpec language and illustrate the benefits of mode-aware model-checking on a case study involving a flight-critical avionics system. The evaluation uses Kind\documentclass[12pt]{minimal}
\usepackage{amsmath}
\usepackage{wasysym}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsbsy}
\usepackage{mathrsfs}
\usepackage{upgreek}
\setlength{\oddsidemargin}{-69pt}
\begin{document}$$2$$\end{document}, a collaborative, parallel, SMT-based model checker extended to fully support CoCoSpec.
Details
- Title: Subtitle
- CoCoSpec: A Mode-Aware Contract Language for Reactive Systems
- Creators
- Adrien Champion - The University of Iowa, Iowa City, USAArie Gurfinkel - SEI/Carnegie Mellon University, Pittsburgh, USATemesghen Kahsai - NASA Ames/Carnegie Mellon University, Pittsburgh, USACesare Tinelli - The University of Iowa, Iowa City, USA
- Resource Type
- Book chapter
- Publication Details
- Software Engineering and Formal Methods, pp.347-366
- Publisher
- Springer International Publishing; Cham
- Series
- Lecture Notes in Computer Science
- DOI
- 10.1007/978-3-319-41591-8_24
- eISSN
- 1611-3349
- ISSN
- 0302-9743
- Language
- English
- Date published
- 06/23/2016
- Academic Unit
- Computer Science
- Record Identifier
- 9984002463902771
Metrics
22 Record Views