Contract Automata: A Specification Language for Mode-Based Systems
Pages 1 - 11
Abstract
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 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 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.
References
[1]
Shaun Azzopardi, Gordon J. Pace, Fernando Schapachnik, and Gerardo Schneider. 2016. Contract automata - An operational view of contracts between interactive parties. Artif. Intell. Law 24, 3 (2016), 203--243.
[2]
Joshua Bachmeier, Alexander Weigl, and Bernhard Beckert. 2024. Contract Machines: An Engineer-friendly Specification Language for Mode-Based Systems. In Methods and Description Languages for Modelling and Verification of Circuits and Systems, MBMV 2024, 27th Workshop, Kaiserslautern, Germany, 14--15 February 2023. VDE/IEEE. (to appear).
[3]
Davide Basile and Maurice H. ter Beek. 2023. A Runtime Environment for Contract Automata. In Formal Methods - 25th International Symposium, FM 2023, Lubeck, Germany, March 6--10, 2023, Proceedings (Lecture Notes in Computer Science, Vol. 14000), Marsha Chechik, Joost-Pieter Katoen, and Martin Leucker (Eds.). Springer, 550--567.
[4]
Bernhard Beckert, Mattias Ulbrich, Birgit Vogel-Heuser, and Alexander Weigl. 2022. Generalized Test Tables: A Domain-Specific Specification Language for Automated Production Systems. In Theoretical Aspects of Computing - ICTAC 2022 - 19th International Colloquium, Tbilisi, Georgia, September 27--29, 2022, Proceedings (Lecture Notes in Computer Science, Vol. 13572), Helmut Seidl, Zhiming Liu, and Corina S. Pasareanu (Eds.). Springer, 7--13.
[5]
Marco Bozzano, Alessandro Cimatti, Cristian Mattarei, and Stefano Tonetta. 2014. Formal Safety Assessment via Contract-Based Design. In Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014, Sydney, NSW, Australia, November 3--7, 2014, Proceedings (Lecture Notes in Computer Science, Vol. 8837), Franck Cassez and Jean-François Raskin (Eds.). Springer, 81--97.
[6]
Aaron R. Bradley. 2011. SAT-Based Model Checking without Unrolling. In Verification, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI 2011, Austin, TX, USA, January 23--25, 2011. Proceedings (Lecture Notes in Computer Science, Vol. 6538), Ranjit Jhala and David A. Schmidt (Eds.). Springer, 70--87.
[7]
Roberto Cavada, Alessandro Cimatti, Michele Dorigatti, Alberto Griggio, Alessandro Mariotti, Andrea Micheli, Sergio Mover, Marco Roveri, and Stefano Tonetta. 2014. The nuXmv Symbolic Model Checker. In CAV (Lecture Notes in Computer Science, Vol. 8559), Armin Biere and Roderick Bloem (Eds.). Springer, 334--342.
[8]
Adrien Champion, Arie Gurfinkel, Temesghen Kahsai, and Cesare Tinelli. 2016. CoCoSpec: A Mode-Aware Contract Language for Reactive Systems. In Software Engineering and Formal Methods - 14th International Conference, SEFM 2016, Held as Part of STAF 2016, Vienna, Austria, July 4--8, 2016, Proceedings (Lecture Notes in Computer Science, Vol. 9763), Rocco De Nicola and eva Kühn (Eds.). Springer, 347--366.
[9]
Chris Chilton, Bengt Jonsson, and Marta Z. Kwiatkowska. 2012. Assume-Guarantee Reasoning for Safe Component Behaviours. In Formal Aspects of Component Software, 9th International Symposium, FACS 2012, Mountain View, CA, USA, September 12--14, 2012. Revised Selected Papers (Lecture Notes in Computer Science, Vol. 7684), Corina S. Pasareanu and Gwen Salaün (Eds.). Springer, 92--109.
[10]
Alessandro Cimatti, Michele Dorigatti, and Stefano Tonetta. 2013. OCRA: A tool for checking the refinement of temporal contracts. In 2013 28th IEEE/ACM International Conference on Automated Software Engineering, ASE 2013, Silicon Valley, CA, USA, November 11--15, 2013, Ewen Denney, Tevfik Bultan, and Andreas Zeller (Eds.). IEEE, 702--705.
[11]
Edmund M. Clarke, Daniel Kroening, and Flavio Lerda. 2004. A Tool for Checking ANSI-C Programs. In Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, TACAS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 -- April 2, 2004, Proceedings (Lecture Notes in Computer Science, Vol. 2988), Kurt Jensen and Andreas Podelski (Eds.). Springer, 168--176.
[12]
Arie Gurfinkel, Temesghen Kahsai, Anvesh Komuravelli, and Jorge A. Navas. 2015. The SeaHorn Verification Framework. In Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18--24, 2015, Proceedings, Part I (Lecture Notes in Computer Science, Vol. 9206), Daniel Kroening and Corina S. Pasareanu (Eds.). Springer, 343--361.
[13]
Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski. 2013. Software Model Checking for People Who Love Automata. In Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13--19, 2013. Proceedings (Lecture Notes in Computer Science, Vol. 8044), Natasha Sharygina and Helmut Veith (Eds.). Springer, 36--52.
[14]
Charles Antony Richard Hoare. 1985. Mathematical logic and programming languages. Prentice-Hall, Chapter Programs are predicates.
[15]
Kim Guldstrand Larsen, Ulrik Nyman, and Andrzej Wasowski. 2006. Interface Input/Output Automata. In FM 2006: Formal Methods, 14th International Symposium on Formal Methods, Hamilton, Canada, August 21--27, 2006, Proceedings (Lecture Notes in Computer Science, Vol. 4085), Jayadev Misra, Tobias Nipkow, and Emil Sekerinski (Eds.). Springer, 82--97.
[16]
Barbara Liskov and Jeannette M. Wing. 1994. A Behavioral Notion of Subtyping. ACM Trans. Program. Lang. Syst. 16, 6 (1994), 1811--1841.
[17]
Marten Lohstroh, Christian Menard, Soroush Bateni, and Edward A. Lee. 2021. Toward a Lingua Franca for Deterministic Concurrent Systems. ACM Trans. Embed. Comput. Syst. 20, 4, Article 36 (may 2021), 27 pages.
[18]
Bertrand Meyer. 1992. Applying "Design by Contract". Computer 25, 10 (1992).
[19]
Alexander Weigl. 2023. Companion artifact for Contract Automata: A Specification Language for Mode-Based Systems.
[20]
Junbeom Yoo, Tai Hyo Kim, Sung Deok Cha, Jang-Soo Lee, and Han Seong Son. 2005. A formal software requirements specification method for digital nuclear plant protection systems. J. Syst. Softw. 74, 1 (2005), 73--83.
Recommendations
Contract-based specification of mode-dependent timing behavior
AbstractThe design of safety-critical systems calls for rigorous application of specification and verification methods. In this context, a comprehensive consideration of safety aspects, which inevitably include timing properties, requires explicit ...
Contract-based formal specification of safety critical systems
COMPSAC-W'05: Proceedings of the 29th annual international conference on Computer software and applications conferenceThe paper proposes an approach to light-weight formal specification for interfaces, connectors, contracts and integration of component systems based on UML 2.0 superstructure. Both of static and dynamic contracts are provided with formal models. Dynamic ...
A Formal Semantics for a Quality of Service Contract Language
Current interests in the context of system development include non-functional aspects of an application and the quality of the service (QoS) it provides. In video on demand applications, for instance, properties such as delay, bandwidth and CPU ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
April 2024
154 pages
ISBN:9798400705892
DOI:10.1145/3644033
- Chair:
- Nico Plat,
- General Chair:
- Stefania Gnesi,
- Program Chairs:
- Carlo A. Furia,
- Antónia Lopes
Copyright © 2024 Copyright held by the owner/author(s).
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, contact the owner/author(s).
Sponsors
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 06 June 2024
Check for updates
Badges
Qualifiers
- Research-article
Funding Sources
- Helmholtz-Gemeinschaft
- Federal Ministry for Econmic Affairs and Climate Action
Conference
FormaliSE '24
Sponsor:
FormaliSE '24: 2024 IEEE/ACM 12th International Conference on Formal Methods in Software Engineering (FormaliSE)
April 14 - 15, 2024
Lisbon, Portugal
Upcoming Conference
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 117Total Downloads
- Downloads (Last 12 months)117
- Downloads (Last 6 weeks)44
Reflects downloads up to 16 Nov 2024
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in