Contract-based design is a paradigm for the design of complex artifacts. Each component is associated with a contract, i.e., a clear description of the expected interaction of the component with its environment. Contracts specify the expected behavior of a component by defining the assumptions that must be satisfied by the environment and the guarantees satisfied by the component in response. For example, a robot or an autonomous car might be guaranteed to avoid collisions with moving obstacles under the assumption that these obstacles do not actively try to hit it. The ultimate goal of contract-based design is to allow for modular or compositional reasoning, stepwise refinement, and a principled reuse of components.

Meyer introduced the idea of Design by Contract in the early 90ies [Meyer 1992, 1997]. Contract-based design was first conceived for software specification. A classical form of contracts are pre-postcondition specifications, dating back to the early 70ies, where they were used to specify the behavior of procedures [Hoare 1971]. As of today, contract-based design is at the core of many interactive and automated tools for software verification, with significant progress made (e.g., in Why3 [Filiâtre et al. 2013], KeY [Ahrendt et al. 2014], VerCors [Blom et al. 2014], and Viper [Müller et al. 2016]).

Somewhat independently, the same conceptual principles have been applied to the development of systems that not only comprise software, but also the execution environment, hardware, communication architecture, and the physical world. This has been done in various theoretical flavors (cf. [Benveniste et al. 2018]), including contract representations in terms of temporal logics [Lamport 1983], interface automata [Alfaro et al. 2001], and category theory [Incer et al. 2023]. Many tools for contract-based system design and verification have been developed and integrated within prominent design languages, including TICC [Adler et al. 2006], OCRA [Cimatti et al. 2013], AGREE [Liu et al. 2016], KeYmaera X [Müller et al. 2018], and PACTI [Incer et al. 2023]. PACTI, for example, defines a general theory of contracts and contract composition. Dedicated languages such as AADL, SysML, SCADE, Simulink, AUTOSAR are used to describe various aspects of the system, and cater for a decoupling between the higher level, e.g., algorithmic aspects and the lower level, e.g., embedded software or the execution platform.

Although contract-based methods for system and software contracts cover complementary phases of the design process for complex (possibly cyber-physical) systems, their integration has not been studied in depth. Clearly, system level and software level are associated with different requirements. The system level focuses on the architectural decomposition, while the software level typically abstracts from the concrete execution platform. In the broader context of system design there may be constraints related to a specific platform, specific communication protocols, time discretization, event-triggered executions, and possibly performance and energy constraints, which also require the consideration of quantitative aspects. A formalization of the interactions between the contracts at system and software level is a fundamental step towards an overarching, seamlessly integrated and effective development process.

In this Dagstuhl Seminar we aim at investigating the convergence of the theory, algorithms, and tools for contract reasoning at two complementary levels: system level and software level. The goal is to support the definition of a seamless, end-to-end integration of contract-based design from abstract system descriptions over verified software components down to the final deployment. We plan to bring together the two communities and to discuss the following themes: How can system and software contracts be harmonized, in order to ensure traceability? What is the required expressiveness to formalize quantitative properties? How can contract inference and abstraction be automated? How can contracts be validated?

While the topic of this seminar is broad, we have seen from previous seminars and workshops that the discussion between experts from the different communities is highly productive. In particular, the discussion of various notions of contracts and their semantics has been proven to be fruitful. We will focus on formal notions and semantic concepts to bind the seminar topics together.

Creative Commons BY 4.0

Alessandro Cimatti, Gidon Ernst, Paula Herber, and Kristin Yvonne Rozier