Albert Benveniste
email: albert.benveniste@inria.fr

Benoît Caillaud

Dejan Nickovic

Roberto Passerone

Jean-Baptiste Raclet

Philipp Reinkemeier

Alberto Sangiovanni-Vincentelli

Werner Damm

Tom Henzinger

Kim Larsen

Contracts for Systems Design

Keywords: system design, component based design, contract, interface conception des systèmes, composant, contrat, interface

Systems design has become a key challenge and differentiating factor over the last decades for system companies. Aircrafts, trains, cars, plants, distributed telecommunication military or health care systems, and more, involve systems design as a critical step. Complexity has caused system design times and costs to go severely over budget so as to threaten the health of entire industrial sectors. Heuristic methods and standard practices do not seem to scale with complexity so that novel design methods and tools based on a strong theoretical foundation are sorely needed. Model-based design as well as other methodologies such as layered and compositional design have been used recently but a unified intellectual framework with a complete design flow supported by formal tools is still lacking albeit some attempts at this framework such as Platform-based Design have been successfully deployed. Recently an "orthogonal" approach has been proposed that can be applied to all methodologies proposed thus far to provide a rigorous scaffolding for verification, analysis and abstraction/refinement: contractbased design. Several results have been obtained in this domain but a unified treatment of the topic that can help in putting contract-based design in perspective is still missing. This paper intends to provide such treatment where contracts are precisely defined and characterized so that they can be used in design methodologies such as the ones mentioned above with no ambiguity. In addition, the paper provides an important link between interfaces and contracts to show similarities and correspondences. Examples of the use of contracts in design are provided as well as in depth analysis of existing literature.

System companies such as automotive, avionics and consumer electronics companies are facing significant difficulties due to the exponentially raising complexity of their products coupled with increasingly tight demands on functionality, correctness, and time-to-market. The cost of being late to market or of imperfections in the products is staggering as witnessed by the recent recalls and delivery delays that system industries had to bear.

In 2010, Toyota had to recall 10 Million cars worldwide for reasons that ranged from the infamous sticky accelerator pedals to steering and engine problems. The last recall at the end of August 2010 was for the engine control module. Toyota is not alone in this situation. Most of the automotive makers had one or more major recalls in the recent past (see e.g., http://www.autorecalls.us) involving electronics as well as mechanical parts. Boeing and Airbus Industries had significant delays in the delivery of their latest planes (787 and A380). For the A380, underlying causes were cited as issues in the cabling system, configuration management and design process. In particular, the complexity of the cabin wiring (100,000 wires and 40,300 connectors) was considered a major issue (see http://en.wikipedia.org/wiki/Airbus_A380). The delays caused the departure of both the EADS and Airbus CEOs and of the program manager for the A380 and caused an overall earning shortfall of 4.8 Billion Euros. Boeing originally planned the first flight of the 787 for August 2007 (see http://en.wikipedia.org/wiki/Boeing_787), but after a stream of delay announcements, the actual first flight occurred on December 15, 2009. The delays were caused by a number of unfortunate events and design errors and caused at least a 2.3 Billion USD write-off not counting the claim of Air India of 1 Billion USD damages for delayed delivery and the revenue shortfalls.

These are examples of the devastating effects that design problems may cause. The specific root causes of these problems are complex and relate to a number of issues ranging from design processes and relationships with different departments of the same company and with suppliers to incomplete requirement specification and testing.

B. The Future: CPS and SoS

Many products and services require to take into consideration the interactions of computational and physical processes. Systems where this interaction is tight and needs special care are called Cyber-Physical Systems (CPS) [START_REF] Lee | Cyber physical systems: Design challenges[END_REF]. The broad majority of these new applications can be classified as "distributed sense and control systems" that go substantially beyond the "compute" or "communicate" functions, traditionally associated with information technology. These applications have the potential to radically influence how we deal with a broad range of crucial problems facing our society today: for example, national security and safety, including surveillance, energy management and distribution, environment control, efficient and reliable transportation and mobility, and effective and affordable health care. A recurring property of these applications is that they engage all the platform components simultaneously-from data and computing services on the cloud of large-scale servers, data gathering from the sensory swarm, and data access on mobile devices-with significant heterogeneity. These large scale systems composed of subsystems that are themselves systems are now called Systems of Systems (SoS) and are heavily investigated.

As the complexity of these systems increases, our inability to rigorously model the interactions between the physical and the cyber sides creates serious vulnerabilities. Systems become unsafe, with disastrous inexplicable failures that could not have been predicted. The challenges in the realization and operation of these CPS and SoS are manifold, and cover a broad range of largely unsolved design and run-time problems. These include: modeling and abstraction, verification, validation and test, reliability and resiliency, multi-scale technology integration and mapping, power and energy, security, diagnostics, and run-time management. Failure to address these challenges in a cohesive and comprehensive way will most certainly delay if not prohibit the widespread adoption of these new technologies.

C. The Need for a Methodological Effort

We believe the most promising means to address the challenges in systems engineering is to employ structured and formal design methodologies that seamlessly and coherently combine the various dimensions of the design space (be it behavior, space or time), that provide the appropriate abstractions to manage the inherent complexity, and that can provide correct-by-construction implementations. The following technology issues must be addressed when developing new approaches to the design of complex systems, CPS and SoS:

• The overall design flows for heterogeneous systemsmeant here both in a technical and also an organizational sense-and the associated use of models across traditional boundaries are not well developed and understood. Relationships between different teams inside a same company, or between different stake-holders in the supplier chain, are not well supported by solid technical descriptions for the mutual obligations.

• System requirement capture and analysis is in large part a heuristic process, where the informal text and natural language-based techniques in use today are facing significant challenges. Formal requirement engineering is in its infancy: mathematical models, formal analysis techniques and links to system implementation must be developed. • Dealing with variability, uncertainty, and life-cycle issues, such as extensibility of a product family, are not welladdressed using available systems engineering methodology and tools. • Design-space exploration is rarely performed adequately, yielding suboptimal designs where the architecture selection phase does not consider extensibility, re-usability, RR n°8147

and fault tolerance to the extent that is needed to reduce cost, failure rates, and time-to-market. • The verification and validation of "complex systems," particularly at the system integration phase, where any interactions are complicated and extremely costly to address, is a common need in defense, automotive, and other industries. The challenge is to address the entire process and not to consider only point solutions of methodology, tools, and models that ease part of the design.

D. Contract based design

It is our goal to offer a new approach to the system design problem that is rigorous and effective in dealing with the problems and challenges described before, and that, at the same time, does not require a radical change in the way industrial designers carry out their task as it cuts across design flows of different type: contract-based design.

Contracts in the layman use of the term are established when an OEM must agree with its suppliers on the subsystem or component to be delivered. Contracts involve a legal part binding the different parties and a technical annex that serves as a reference regarding the entity to be delivered by the supplier-in this work we focus on the technical facet of contracts. Contracts can also be used through their technical annex in concurrent engineering, when different teams develop different subsystems or different aspects of a system within a same company.

In this paper, we argue that contracts can be actually used almost everywhere and at nearly all stages of system design, from early requirements capture, to embedded computing infrastructure and detailed design involving circuits and other hardware. Contracts explicitly handle pairs of properties, respectively representing the assumptions on the environment and the guarantees of the system under these assumptions. Intuitively, a contract is a pair C = (A, G) of {Assumptions, Guarantees}, characterizing in a formal way 1) under which context the design is assumed to operate, and 2) what its obligations are. Assume/Guarantee reasoning has been known for quite some time, but it has been used mostly as verification mean for the design of software. Our purpose is more ambitious: contract based design with explicit assumptions is a philosophy that should be followed all along the design, with all kinds of models, whenever necessary. Here, the models we mean are rich-not only profiles, types, or taxonomy of data, but also models describing the functions, performances of various kinds (time and energy), and safety. The consideration of rich contracts as above in the industry is still in its infancy. To make contract-based design a technique of choice for system engineers, we must develop:

• Mathematical foundations for contract representation and requirement engineering that enable the design of frameworks and tools;

• A system engineering framework and associated methodologies and tool sets that focus on system requirement modeling, contract specification, and verification at multiple abstraction layers. The framework should address cross-boundary and cross-organizational design activities. This paper intends to provide a unified treatment of contracts where they are precisely defined and characterized so that they can be used in design with no ambiguity. In addition, the paper provides an important link between interfaces and contracts to show similarities and correspondences. Examples of the use of contracts in design will be provided as well as in depth analysis of existing literature.

E. Reader's guide

The organization of the paper is explained in Table I. In Section II a review of the challenges that are faced by the system industry is proposed, followed, in Section III, by an analysis of the design methodologies that have been deployed to cope with them.

Section IV develops a primer on contracts by using a very simple example requiring only elementary mathematical background to be followed. Its purpose is to smoothly introduce the different concepts and operations we need for a contract framework-the restricted case considered is by no means representative of the kind of system we can address using contracts. We then introduce a motivating example representative of requirement engineering. In a third sub-section, "requirements" on a theory of contracts are identified from analyzing what is expected from contract-based design, and in particular the support for: 1) the development of different aspects or viewpoints of a system such as its function, safety, timing, and resource use, by different teams and how to fuse these different aspects, and 2) the possibility for different suppliers to develop independently the different subsystems subcontracted to them. This section concludes with the related bibliography.

Section V is the cornerstone of this paper and it is a new vista on contracts. The so-called "meta-theory" of contracts is introduced and developed in detail. By meta-theory we mean the collection of concepts, operations, and properties that any formal contract framework should offer. Concepts, operations, and properties are thus stated in a fairly generic way. Every concrete framework compliant with this metatheory will inherit these generic properties. The meta-theory focuses on assumptions and guarantees, its formalizes how different aspects or viewpoints of a specification can be integrated, and on which basis independent development by different suppliers can be safely performed.

So far the meta-theory is non effective in that it is not said how component and contracts are effectively represented and manipulated. The subsequent series of sections propose a panorama of major concrete contract frameworks. Section VII develops the Assume/Guarantee contracts. This framework is the most straightforward instance of the meta-theory. It deals with pairs (A, G) of assumptions and guarantees explicitly, A and G being both expressed as properties. This framework is flexible in that it allows for different styles of description of such properties-computational efficiency depends on the style adopted. Section VIII develops the Interface theories, in which assumptions and guarantees are specified by means of a single object: the interface. Interface theories turn out to include the most effective frameworks. They can easily be adapted to encompass timing (Section IX) and probabilistic (Section X) characteristics of systems.

In Section XI, a toy example in requirements engineering is developed. This example is simple but rich enough to illustrate the very difficulties in formalizing requirements. It also illustrates well the added value of contract based requirements engineering. First, the different responsibilities (assumptions versus obligation or guarantees) that requirement implicit refer to are made explicit and captured in our contract framework. Second, contracts offer a formal meaning for documents of requirements structured into chapters or viewpoints. Contracts offer formal support for checking important properties such as consistency, compatibility, completeness, and more. Finally, contracts offer significant assistance in the process of deducing, from the top specification, an architecture of specifications for the different sub-systems for independent development. While our application example is a toy one, is it nevertheless too complex for dealing with it by hand. We handle it by using a proof-of-concept tool for contract management.

Finally, Section XII develops a case study in the context of AUTOSAR. AUTOSAR is a recently established standard in the automobile sector. This standard was developed with the objective of allowing for better flexibility in component reuse and OEM/supplier relations. This section illustrates how contracts can be used to break into simple pieces of reasoning the difficult task of correct system integration.

II. SYSTEM DESIGN CHALLENGES

Many challenges face the system community to deliver products that are reliable and effective. We summarize some of them below.

A. Complexity of Systems

The ever-expanding use of electronic embedded systems to control increasingly many aspects of the real world, and the trend to interconnect more and more such systems (often from different manufacturers) into a global network are creating a challenging scenario for system designers. In this scenario, the three challenges that are taking center stage are as follows.

The Hardware Platform Complexity: Most system companies rely on Components off-the-shelf (COTS) and programmability to implement their applications. For companies who build "physically large" systems such as avionics and automotive companies, the complexity of the hardware platform is reflected in the number of Electronic Control Units and in their interconnections. For a top-of-the-line automobile, the number of processors to manage and interconnect is above 50. The layout of the cables that connect these processing elements with sensors and actuators is a serious concern. Initial production of the Airbus A380 was troubled by delays in part attributed to the 530 km (330 mi) of wiring in each aircraft.

The Embedded Software Complexity: Given the cost and risks associated to developing hardware solutions, system companies are selecting hardware platforms that can be customized by reconfiguration and/or by software programmability. In particular, software is taking the lion's share of the implementation budgets and cost. In cell phones, more than 1 million lines of code is standard today, while in automobiles the estimated number of lines by 2010 is in the order of hundreds of millions and in the Boeing 787 is in the order of 20 million lines. However, as this happens, the complexity explosion of the software component causes serious concerns for the final quality of the products and the productivity of the engineering teams.

The Integration Complexity: A standard technique to deal with complexity consists in decomposing top-down the system into subsystems. This approach, which has been customarily adopted by the semiconductor industry for years, has a limitation as a designer or a group of designers has to fully comprehend the entire system and to partition appropriately its various parts, a difficult task given the enormous complexity of today's systems.

Hence, the future is one of developing systems by composing pieces that all or in part have already been predesigned or designed independently by other design groups or even companies. This has been done routinely in vertical design chains for example in the avionics and automotive sectors, albeit in a heuristic and ad hoc way. The resulting lack of an overall understanding of the interplay of the subsystems and of the difficulties encountered in integrating very complex parts cause system integration to become a nightmare in the system industry, as demonstrated by Table II. 1In addition, heterogeneity comes into play. Integration of electronic and mechanical design tools and frameworks will be essential in the near future. Integration of chemical, electronic, and biology tools will be essential in the further future for nano-systems. Data integration and information flow among the companies forming the chain have to be supported. In other words, it is essential that the fundamental steps of system design (functional partitioning, allocation on computational resources, integration, and verification) be supported across the entire design development cycle and across different disciplines.

B. Complexity of OEM-Supplier Chains

The source of the above problems is clearly the increase in complexity. It is, however, also the difficulty of the OEMs in managing the integration and maintenance process with subsystems that come from different suppliers who use different design methods, different software architectures, and different hardware platforms.

There are also multiple challenges in defining technical annexes to commercial contracts between OEM and suppliers. Specifications used for procurement should be precise, unambiguous, and complete. However, a recurrent reason for failures causing deep iterations across supply chain boundaries rests in incomplete characterizations of the environment of the system to be developed by the supplier, such as missing information about failure modes and failure rates, missing information on possible sources for interferences through shared resources, and missing boundary conditions. This highlights the need to explicate assumptions on the design context in OEM-supplier commercial contracts. In light of an increased sharing of hardware resources by applications developed by multiple suppliers, a contract-based approach seems indispensable for resolving liability issues and allowing applications with different criticality levels to co-exist (such as ASIL levels [175], [START_REF]Road vehicles -functional safety[END_REF] in automotive).

C. Managing Requirements

We argued that the design chains should connect seamlessly to minimize design errors and time-to-market delays. Yet, the boundaries among companies and between different divisions of the same company are often not as clean as needed and design specs move from one company (or one division) to the RR n°8147 next in non-executable and often unstable and imprecise forms, thus yielding misinterpretations and consequent design errors. In addition, errors are often caught only at the final integration step as the specifications were incomplete and imprecise; further, nonfunctional specifications (e.g., timing, power consumption, size) are difficult to trace. Further, it is common practice to structure system level requirements into several "chapters", "aspects", or "viewpoints". Examples include the functions, safety, timing, and energy viewpoints. Quite often, these different viewpoints are developed by different teams using different skills, frameworks, and tools. Yet they are not unrelated, as we already mentioned. Without a clean approach to handle multiple viewpoints, the only sensible way is to collect these viewpoints into a single requirements document, which is then seen as a flat collection of requirements for subsequent design. Since this is clearly impracticable, the common practice instead is to discard some of the viewpoints in a first stage, e.g., by considering only functions and safety. Designs are then developed based on these only viewpoints. Other viewpoints are subsequently taken into account (timing, energy), thus resulting in late and costly modifications and re-designs.

Requirement engineering is a discipline that aims at improving this situation by paying close attention to the management of the requirement descriptions and traceability support (e.g., using commercial tools such as DOORS 2 in combination with Reqtify3 ) and by inserting whenever possible precise formulation and analysis methods and tools. Research in this area is active but we believe more needs to be done to make this essential step a first class citizen in system design. Indeed, if the specification quality is low, then the entire design process is marred since the very beginning! The overall system product specification is somewhat of an art today since to verify its completeness and its correctness there is little that it can be used to compare with.

D. Managing Risks

System design processes are highly concurrent, distributed, and typically multi-domain, often involving more than one hundred sub-processes. The complexity of the entire design process and of the relationships between players in the supply chain creates the need to elaborate risk sharing and risk management plans because of the potential enormity of the impact that design errors and supplier solidity may have on the economics of a company. Risk management has thus become a requirement of most of public companies, as financial, social and political risks are analyzed and appropriate countermeasures have to be prepared as a requirement from the regulatory bodies. Risk mitigation measures typically cover all phases of design processes, ranging from assuring high quality initial requirements to early assessments of risks in meeting product requirements during the concept phase, to enforcing complete traceability of such requirements with requirements management tools, to managing consistency and synchronization across concurrent sub-processes using PLM tools. 4 If we will be able to change the design process along the lines of more formal approaches, better complexity handling, better requirement engineering, then risks will be substantially lower than they are today.

E. System-wide Optimization

We believe that since the design process is fragmented, product optimization is rarely carried out across more than one company boundary and even then, it is limited due to:

• The lack of appropriate models encompassing both functional and non-functional (Quality of Service) aspects, covering both internal use and export outside the company; • The time pressure to meet the product deadlines;

• The functional description that is over-constrained by architectural considerations which de facto eliminate potentially interesting implementation alternatives. If the design process were carried out as in a unique, wellintegrated, virtual company including all the players shown above, the overall ecosystem would greatly benefit. The issue here is to allow a reasonably efficient design space exploration by providing a framework where different architectures could be quickly assembled and evaluated at each layer of abstraction corresponding to the design task being considered in the chain.

III. HOW CHALLENGES HAVE BEEN ADDRESSED SO FAR

In this section we present a review and a critical analysis of the design methodologies that have been deployed to cope with the challenges exposed in the previous section.

A. Complexity of Systems and System-wide Optimization

Multiple lines of attack have been developed by research institutions and industry to cope with the exponential growth in systems complexity, starting from the iterative and incremental development several decades ago [START_REF] Larman | Iterative and incremental developments: a brief history[END_REF]. Among them, of particular interest to the development of embedded controllers are: Layered design, Component-based design, the V-model process, model-based development, virtual integration and Platform-Based Design (PBD). There are two basic principles followed by these methods: abstraction/refinement and composition/decomposition. Abstraction and refinement are processes that relate to the flow of design between different layers of abstraction (vertical process) while composition and decomposition operate at the same level of abstraction (horizontal process). Layered design, the V-model process, and model-based development focus on the vertical process while component-based design deals principally with the horizontal process. PBD combines the two aspects in a unified framework and hence subsumes and can be used to integrated the other methodologies. Contracts are ideal tools to solidify both vertical and horizontal processes providing the theoretical background to support formal methods.

1) Layered design: Layered design copes with complexity by focusing on those aspects of the system pertinent to support the design activities at the corresponding level of abstraction. This approach is particularly powerful if the details of a lower layer of abstraction are encapsulated when the design is carried out at the higher layer. Layered approaches are well understood and standard in many application domains. As an example, consider the AUTOSAR standard. 5 This standard defines several abstraction layers. Moving from "bottom" to "top", the micro-controller abstraction layer encapsulates completely the specifics of underlying micro-controllers, the second layer abstracts from the concrete configuration of the Electronic Control Unit (ECU), the employed communication services and the underlying operating system, whereas the (highest) application layer is not aware of any aspect of possible target architectures, and relies on purely virtual communication concepts in specifying communication between application components. Similar abstraction levels are defined by the ARINC standard in the avionic domains.

The benefits of using layered design are manifold. Using the AUTOSAR layer structure as example, the complete separation of the logical architecture of an application (as represented by a set of components interconnected using the so-called virtual function bus) and target hardware is a key aspect of AUTOSAR, in that it supports decoupling of the number of automotive functions from the number of hardware components. In particular, it is flexible enough to mix components from different applications on one and the same ECU. This illustrates the double role of abstraction layers, in allowing designers to focus completely on the logic of the application and abstracting from the underlying hardware, while at the same time imposing a minimal (or even no) constraint on the design space of possible hardware architectures. In particular, these abstractions allow the application design to be re-used across multiple platforms, varying in number of bus-systems and/or number and class of ECUs. These design layers can, in addition, be used to match the boundaries of either organizational units within a company, or to define interfaces between different organizations in the supply chain. The challenge, then, rests in providing the proper abstractions of lower-level design entities.

2) Component-based design: Whereas layered designs decompose complexity of systems "vertically", component-based approaches reduce complexity "horizontally" whereby designs are obtained by assembling strongly encapsulated design entities called "components" equipped with concise and rigorous interface specifications. Re-use can be maximized by finding the weakest assumptions on the environment sufficient to establish the guarantees on a given component implementation. While these interface specifications are key and relevant for any system, the "quality attribute" of perceiving a subsystem as a component is typically related to two orthogonal criteria, that of "small interfaces", and that of minimally constraining the deployment context, so as to maximize the potential for reuse. "Small interfaces", i.e., interfaces which are both small in terms of number of interface variables or ports, as well as "logically small", in that protocols governing the invocation of component services have compact specifications not requiring deep levels of synchronization, constitute evidence of the success of encapsulation-still, small interfaces must encompass dynamic properties of the system. The second quality attribute is naturally expressible in terms of interface specifications, where re-use can be maximized by finding the weakest assumptions on the environment sufficient to establish the guarantees on a given component implementation.

One challenge, then, for component-based design of embedded systems, is to provide interface specifications that are rich enough to cover all phases of the design cycle. This calls for including non-functional characteristics as part of the component interface specifications, which is best achieved by using multiple viewpoints. Current component interface models, in contrast, are typically restricted to purely functional characterization of components, and thus cannot capitalize on the benefits of virtual integration testing, as outlined above.

The second challenge is related to product line design, which allows for the joint design of a family of variants of a product. The aim is to balance the contradicting goals of striving for generality versus achieving efficient component implementations. Methods for systematically deriving "quotient" specifications to compensate for "minor" differences between required and offered component guarantees by composing a component with a wrapper component (compensating for such differences as characterized by quotient specifications) exists for restricted classes of component models [START_REF] Passerone | Convertibility verification and converter synthesis: Two faces of the same coin[END_REF].

3) The V-model process: A widely accepted approach to deal with complexity of systems in the defense and transportation domain is to structure product development processes along variations of the V diagram originally developed for defense applications by the German DoD. 6Its characteristic V-shape splits the product development process into a design and an integration phase. Specifically, following product level requirement analysis, subsequent steps would first evolve a functional architecture supporting product level requirements. Sub-functions are then re-grouped taking into account re-use and product line requirements into a logical architecture, whose modules are typically developed by different subsystem suppliers. The realization of such modules often involves mechanical, hydraulic, electrical, and electronic system design. Subsequent phases would then unfold the detailed design for each of these domains, such as the design of the electronic subsystem involving among others the design of electronic control units. These design phases are paralleled by integration phases along the right-hand part of the V, such as integrating basic-and application software on the ECU hardware to actually construct the electronic control unit, integrating the complete electronic subsystems, integrating the mechatronic subsystem to build the module, and integrating multiple modules to build the complete product. Not shown, but forming an integral part of V-based development processes are testing activities, where at each integration level testsuites developed during the design phases are used to verify compliance of the integrated entity to their specification.

This presentation is overly simplistic in many ways. The design of electronic components in complex systems such as aircrafts inherently involves multi-site, multi-domain and cross-organizational design teams, reflecting, e.g., a partitioning of the aircraft into different subsystems (such as primary and secondary flight systems, cabin, fuel, and wing), different domains such as the interface of the electronic subsystem to hydraulic and/or mechanical subsystems, control-law design, telecommunications, software design, hardware design, diagnostics, and development-depth separated design activities carried out at the OEM and supplier companies. This partitioning of the design space (along perspectives and abstraction layers) naturally lends itself to a parallelization of design activities, a must in order to achieve timely delivery of the overall product, leading often into the order of hundreds of concurrent design processes. To summarize, while being popular and widely referenced, the V-model process has become a "slogan" hiding the complexity of actual design processes. In reality, large system companies develop their own processes and then struggle for their application, both in-house and across the supplier chain.

4) Model-Based Design:

Model-based design (MBD) is today generally accepted as a key enabler to cope with complex system design due to its capabilities to support early requirement validation and virtual system integration. MBD-inspired design languages and tools such as SysML7 [START_REF]System modeling language specification v1[END_REF] and/or AADL [START_REF] Hudak | The Architecture Analysis and Design Language (AADL): An Introduction[END_REF] for system level modeling, Catia and Modelica [START_REF] Fritzson | Principles of Object-Oriented Modeling and Simulation with Modelica 2[END_REF] for physical system modeling, Matlab-Simulink [START_REF] Karris | Introduction to Simulink with Engineering Applications[END_REF] for control-law design, and UML8 [START_REF] Booch | Unified Modeling Language User Guide, The (2nd Edition)[END_REF], [START_REF]Unified Modeling Language (UML) specification[END_REF] Scade [START_REF] Berry | The effectiveness of synchronous languages for the development of safety-critical systems[END_REF] and TargetLink for detailed software design, depend on design layer and application class. The state-of-the-art in MBD includes automatic code-generation, simulation coupled with requirement monitoring, co-simulation of heterogeneous models such as UML and Matlab-Simulink, model-based analysis including verification of compliance of requirements and specification models, model-based test-generation, rapid prototyping, and virtual integration testing as further elaborated below.

In MBD today non-functional aspects such as performance, timing, power or safety analysis are typically addressed in dedicated specialized tools using tool-specific models, with the entailed risk of incoherency between the corresponding models, which generally interact. To counteract these risks, meta-models encompassing multiple views of design entities, enabling co-modeling and co-analysis of typically heterogeneous viewpoint specific models have been developed. Examples include the MARTE UML [148] profile for real-time system analysis, the SPEEDS HRC metamodel [START_REF] Passerone | Metamodels in Europe: Languages, tools, and applications[END_REF] and the Metropolis semantic meta-model [START_REF] Balarin | A formal approach to system level design: Metamodels and unified design environments[END_REF], [START_REF] Davare | A next-generation design framework for platform-based design[END_REF], [START_REF] Balarin | Platform-based design and frameworks: METROPOLIS and METRO II[END_REF], [START_REF] Sangiovanni-Vincentelli | Metamodeling: An emerging representation paradigm for system-level design[END_REF]. In Metropolis multiple views are accommodated via the concept of "quantities" that annotate the functional view of a design and can be composed along with subsystems using a suitable algebra. The SPEEDS meta-model building on and extending SysML has been demonstrated to support co-simulation and co-analysis of system models for transportation applications allowing co-assessment of functional, real-time and safety requirements. It forms an integral part of the meta-model-based inter-operability concepts of the CESAR reference technology platform. 9Meta-modeling is also at the center of the model driven (software) development (MDD) methodology. MDD is based on the concept of the model-driven architecture (MDA), which consists of a Platform-Independent Model (PIM) of the application plus one or more Platform-Specific Models (PSMs) and sets of interface definitions. MDA tools then support the mapping of the PIM to the PSMs as new technologies become available or implementation decisions change [START_REF]Object Management Group (OMG). Model driven architecture (MDA) FAQ[END_REF]. The Vanderbilt University group [START_REF] Karsai | Modelintegrated development of embedded software[END_REF] has evolved an embedded software design methodology and a set of tools based on MDD. In their approach, models explicitly represent the embedded software and the environment it operates in and capture the requirements and the design of the application, simultaneously, using domain-specific languages (DSL). The generic modeling environment (GME) [START_REF] Karsai | Modelintegrated development of embedded software[END_REF] provides a framework for model transformations enabling easy exchange of models between tools and offers sophisticated ways to support syntactic (but not semantic) heterogeneity. The KerMeta metamodeling workbench [START_REF] Fleurey | Weaving executability into object-oriented meta-languages[END_REF] is similar in scope.

5) Virtual Integration:

Rather than "physically" integrating a system from subsystems at integration stages, model-based design allows systems to be virtually integrated based on the models of their subsystem and the architecture specification of the system. Such virtual integration thus allows detecting potential integration problems up front, in the early design phases. Virtual system integration is often a source of heterogeneous system models, such as when realizing an aircraft function through the combination of mechanical, hydraulic, and electronic systems. Heterogeneous composition of models with different semantics was originally addressed in Ptolemy [START_REF] Eker | Taming heterogeneity -the ptolemy approach[END_REF], Metropolis [START_REF] Balarin | Metropolis: An Integrated Electronic System Design Environment[END_REF], [START_REF] Davare | A next-generation design framework for platform-based design[END_REF], [START_REF] Balarin | Platform-based design and frameworks: METROPOLIS and METRO II[END_REF], [START_REF] Burch | Overcoming heterophobia: Modeling concurrency in heterogeneous systems[END_REF], and in the SPEEDS meta-model of heterogeneous rich components [START_REF] Damm | Boosting reuse of embedded automotive applications through rich components[END_REF], [START_REF] Benveniste | Multiple viewpoint contract-based specification and design[END_REF], [START_REF] Benvenuti | A contract-based formalism for the specification of heterogeneous systems[END_REF], albeit with different approaches. Virtual integration involves models of the functions, the computer architecture with its extra-functional characteristics (timing and other resources), and the physical system for control. Some existing frameworks offer significant support for virtual integration: Ptolemy II, Metropolis, and RT-Builder. Developments around Catia and Modelica as well as the new offer SimScape by Simulink provide support for virtual integration of the physical part at an advanced level.

6) Platform

Based Design: Platform-based design was introduced in the late 1980s to capture a design process that could encompass horizontal (component-based design, virtual integration) and vertical (layered and model-based design) decompositions, and multiple viewpoints and in doing so, support the supply chain as well as multi-layer optimization.

The idea was to introduce a general approach that could be shared across industrial domain boundaries, that would subsume the various definition and design concepts, and that would extend it to provide a framework to reason about design. Indeed, the concepts have been applied to a variety of very different domains: from automotive, to System-on-Chip, from analog circuit design, to building automation to synthetic biology.

The basic tenets of platform-based design are as follows: The design progresses in precisely defined abstraction layers; at each abstraction layer, functionality (what the system is supposed to do) is strictly separated from architecture (how the functionality could be implemented). This aspect is clearly related to layered design and hence it subsumes it.

Each abstraction layer is defined by a design platform. A design platform consists of

• A set of library components. This library not only contains computational blocks that carry out the appropriate computation but also communication components that are used to interconnect the computational components. • Models of the components that represent a characterization in terms of performance and other non-functional parameters together with the functionality it can support. Not all elements in the library are pre-existing components. Some may be "place holders" to indicate the flexibility of "customizing" a part of the design that is offered to the designer. In this case the models represent estimates of what can be done since the components are not available and will have to be designed. At times, the characterization is indeed a constraint for the implementation of the component and it is obtained top-down during the refinement process typical of layered designs. This layering of abstractions based on mathematical models is typical of model-based methods and the introduction of non-functional aspects of the design relates to viewpoints. • The rules that determine how the components can be assembled and how the the functional and non-functional characteristics can be computed given the ones of the components to form an architecture.Then, a platform represents a family of designs that satisfies a set of platform-specific constraints [START_REF] Balarin | Constraints specification at higher levels of abstraction[END_REF]. This aspect is related to component-based design enriched with multiple viewpoints. This concept of platform encapsulates the notion of re-use as a family of solutions that share a set of common features (the elements of the platform). Since we associate the notion of platform to a set of potential solutions to a design problem, we need to capture the process of mapping a functionality (what the system is supposed to do) with the platform elements that will be used to build a platform instance or an "architecture" (how the system does what it is supposed to do). The strict separation between function and architecture as well as the mapping process have been highly leveraged in AUTOSAR. This process is the essential step for refinement and provides a mechanism to proceed towards implementation in a structured way. Designs on each platform are represented by platformspecific design models. A design is obtained by a designer's creating platform instances (architectures) via composing platform components (process that is typical of component-based design), by mapping the functionality onto the components of the architecture and by propagating the mapped design in the design flow onto subsequent abstraction layers that are dealt with in the same way thus presenting the design process as an iterative refinement. This last point dictates how to move across abstraction layers: it is an important part of design space exploration and offers a way of performing optimization across layers. In this respect PBD supports multiple viewpoints in a general way.

B. Complexity of OEM-Supplier Chains: Standardization and Harmonization

So far the main answer to the complexity of OEM-supplier chains has been standardization. Standardization concerns both the design entities and the design processes, particularly through the mechanism of certification.

1) Standardization of design entities: By agreeing on (domain specific) standard representations of design entities, different industrial domains have created their own lingua franca, thus enabling a domain wide shared use of design entities based on their standardized representation. Examples of these standards in the automotive sector include the recently approved requirement interchange format standard RIF 10 , the AUTOSAR11 de-facto standard, the OSEK12 operating system standard, standardized bus-systems such as CAN 13and Flexray14 , standards for "car2X" communication, and standardized representations of test supported by ASAM 15 . Examples in the aerospace domain include ARINC standards 16 such as the avionics applications standard interface, IMA, RTCA 17 communication standards. In the automation domain, standards for interconnection of automation devices such as Profibus 18 are complemented by standardized design languages for application development such as Structured Text.

As standardization moves from hardware to operating system to applications, and thus crosses multiple design layers, the challenge increases to incorporate all facets of design entities required to optimize the overall product, while at the same time enabling distributed development in complex supply chains. As an example, to address the different viewpoints required to optimize the overall product, AUTOSAR extended in transitioning from release 3.1 to 4 its capability to capture timing characteristics of design entities, a key prerequisite for assessing alternate deployments with respect to their impact on timing. More generally, the need for overall system optimization calls for the standardization of all nonfunctional viewpoints of design entities, an objective yet to be achieved in its full generality. in order to allow cross layer optimization. Within the EDA domain, such richness of design interface specifications is industrial practice. Within the systems domain, the rich component model introduced in the Integrated Projects SPEEDS tackles this key objective: in covering multiple design layers (from product requirements to deployment on target architectures) and in providing means of associating multiple viewpoints with each design entity, it is expressive enough to allow for cross-supply chain optimization of product developments. This approach is further elaborated and driven towards standardization in the Artemis flagship project CESAR.

2) Harmonization of processes and certification: Harmonizing or even standardizing key processes (such as development processes and safety processes) provides for a further level of optimization in interactions across the supply chain. As an example, Airbus Directives and Procedures (ADBs) provide requirements for design processes of equipment manufactures. Often, harmonized processes across the supply chain build on agreed maturity gates with incremental acceptance testing to monitor progress of supplier development towards final acceptance, often building on incremental prototypes. Shared use of Product Lifcycle Management (PLM) 19databases across the supply chain offers further potentials for cross-supply chain optimization of development processes. Also, in domains developing safety related systems, domain specific standards clearly define the responsibilities and duties of companies across the supply chain to demonstrate functional safety, such as in the ISO 26262 20 for the automotive domain, IEC 61508 21 for automation, its derivatives Cenelec EN 50128 and 50126 22 for rail, and Do 178 B23 for civil avionics.

Yet, the challenge in defining standards rests in balancing the need for stability with the need of not blocking process innovations. As an example, means for compositional construction of safety cases are seen as mandatory to reduce certification costs in the aerospace and rail domains. Similarly, the potential of using formal verification techniques to cope with increasing system complexity is considered in the move from DO 178 B to DO 178 C standards.

C. Managing Requirements: Traceability and Multiple Viewpoints

Depending on application domains, up to 50% of all errors result from imprecise, incomplete, or inconsistent and thus unfeasible requirements. Requirements are inherently ill structured. They must address all aspects of the system and thus cannot be constrained by the lingua franca of a particular domain. They are fragmented in the form of large and sometimes huge DOORS files, 24 structured into viewpoints. Two issues have thus been identified by systems industries as essential for requirement management: powerful and flexible traceability tools to relate requirements between them and to link them to tests for validation purposes, and the development of domain specific ontologies as part of the PLM suite. Further, based on an assessment by the system companies processes in the CESAR project 25 and the German Embedded Systems Innovation alliance 26 , and building on the finding of the Integrated Project SPEEDS 27 , multiple viewpoints have been categorized into perspectives and aspects to provide a solid requirement and property modeling scaffold. Perspectives are viewpoints relevant to architecture modeling, as carried out by different stake-holders during the development process. Aspects are viewpoints that are orthogonal to the system structure. Aspects are used to demonstrate compliance of the architecture to end-user concerns. Example of aspects are safety, cost, maintainability, performance, and weight. The meta-model underlying the CESAR RTP is able to maintain links such as the satisfy, derive, verify, refine and allocate relationships between design artifacts of different perspectives and across abstraction layers.

In addition, to cope with the inherently unstructured problem of (in)completeness of requirements, industry has set up domain-and application-class specific methodologies. As particular examples, we mention learning process, such as employed by Airbus to incorporate the knowledge base of external hazards from flight incidents, the Code of Practice proposed by the Prevent Project 28 using guiding questions to assess the completeness of requirements in the concept phase of the development of advanced driver assistance systems. Use-case analysis methods as advocated for UML based development process follow the same objective. All together, requirement engineering misses the support of formal approaches for its structuring and analysis.

D. Cross-company Shared Risk Management

The realization of complex systems calls for design processes that mitigate risks in highly concurrent, distributed, and typically multi-domain engineering processes, often involving more than one hundred sub-processes. Risk mitigation 24 Typical sub-systems in aeronautics would have a few thousands top-level requirements. An aircraft can have up to several hundred thousands of them. 25 www.cesarproject.eu 26 http://spes2020.informatik.tu-muenchen.de 27 http://www.speeds.eu.com 28 Albert: http://...

RR n°8147

measures typically cover all phases of design processes, ranging from ensuring high quality initial requirements to early assessments of risks in realizability of product requirements during the concept phase, to enforcing complete traceability of such requirements with requirements management tools, to managing consistency and synchronization across concurrent sub-processes using PLM tools. A key challenge rests in balancing risk reduction versus development time and effort: completely eliminating the risks stemming from concurrent engineering essentially requires a complete synchronization along a fine-grained milestone structure, which would kill any development project due to the induced delays. Another key challenge is the "not my fault" syndrome in the OEM-supplier chain when errors call for costly re-design and the issue of penalties arises. Properly assigning responsibilities to risks is still out of reach today.

E. The Need for Contracts

The way system design challenges have been addressed so far leaves huge opportunities for improvements by relying on contract-based design. In this section we briefly summarize, for each existing approach to address the design challenges, how contracts could improve the current situation.

Contribution 1: Addressing Complexity of Systems and System-wide Optimization. While layered design (Section III-A1) and component based design (Section III-A2) have been critical steps in breaking systems complexity, they do not by themselves provide the ultimate answer. When design is being performed at a considered layer, implicit assumptions regarding other layers (e.g., computing resources) are typically invoked by the designer without having these explicated. Hence, actual properties of these other layers cannot be confronted against these hidden assumptions. Similarly, when components or sub-systems are abstracted via their interfaces in component based design, it is generally not true that such interfaces provide sufficient information for other components to be safely implemented based on this sole interface. Contract-based design provides the due discipline, concepts, and techniques to cope with these difficulties.

Model-based development (Section III-A4) has reached significant maturity by covering nearly all aspects of the system (physics, functions, computing resources), albeit not yet in a fully integrated way. To offer a real added value, any newly proposed technology should be rich enough for encompassing all these aspects as well. Contract-based design offers, in large part, this desirable feature.

Virtual integration and virtual modeling (Section III-A5) is a step beyond basic model-based development, by offering an integrated view of all the above different aspects, e.g., physics + functions + performances. Contract-based design supports the fusion of different systems aspects.

Contract-based design is compliant with the V-model process (Section III-A3), just because it does not impose any particular design process. Using contracts only imposes a small set of rules that any process should accommodate, see Section IV-D for a discussion of this.

Finally, Platform-Based Design (PBD, Section III-A6), which is being deployed in some large systems industries such as United Technologies Corporation (UTC), is a systematic and comprehensive methodology that unifies the various design methodologies that have been described in this section. Contracts offer theory and methodological support for both the successive refinement aspect, the composition aspect and the mapping process of PBD allowing formal analysis and synthesis processes.

Contribution 2: Addressing the Complexity of OEM-Supplier Chains. The problems raised by the complexity of OEM-Supplier Chains (Section II-B) are indeed the core target of contractbased design. By making the explication of implicit assumptions mandatory, contracts help assigning responsibilities to a precise stake holder for each design entity. By supporting independent development of the different sub-systems while guaranteing smooth system integration, they orthogonalize the development of complex systems. Contracts are thus adequate candidates for a technical counterpart of the legal bindings between partners involved in the distributed and concurrent development of a system. Contribution 3: Managing Requirements. So far the task of getting requirements right and managing them well (Section III-C) has only got support for sorting the complexity out (traceability services and ontologies, which is undoubtely necessary). However, requirements can only be tested on implementations and it is not clear whether proper distinctions are made when performing tests regarding the following: fusing the results of tests associated to different chapters or viewpoints of a requirement document versus fusing the results of tests associated to different sub-systems; testing a requirement under the responsibility of the designer of the considered sub-system versus testing a requirement corresponding to an assumption regarding the context of use of this sub-system-such distinctions should be made, as we shall see. Also, requirements are barely executable and cannot, in general, be simulated. Requirements engineering is the other primary target of contract-based design: the above issues are properly handled by contracts and contracts offer improved support for evidencing the satisfaction of certification constraints.

Contribution 4: Managing Risks. Risk metrics and risk mitigation measures are the essential tools in managing risks (Section III-D). By offering improved support for sub-contracting and distributing design to different teams, contracts are likely to significantly reduce the "not my fault" syndrome.

Contribution 5: Addressing Certification. As explained in Section III-B2, the design of critical systems is subject to a number of certification standards. While certification steps are mostly concerned with the processes, not the designs themselves, the recent move from DO 178B to DO 178C for level A critical systems in aeronautics has shown for the first time the consideration of formal proofs or validations as valid evidences. We believe that the same will eventually hold for contracts. In particular, by providing adequate formal support for completeness, consistency, compatibility, and more, for sets of requirements, contracts would provide a valuable contribution to certification.

IV. CONTRACTS: WHAT? WHY? WHERE? AND HOW?

As we argued in the previous section, there are two basic principles followed by design methods so far developed: abstraction/refinement and composition/decomposition. Abstraction and refinement are processes that relate to the flow of design between different layers of abstraction (vertical process) while composition and decomposition operate at the same level of abstraction (horizontal process). In this section, we present briefly contracts and the basic operations they support and then me make the point that contracts are ideal tools to solidify both vertical and horizontal processes providing the theoretical background to support formal methods. We conclude the section by providing a (non exhaustive) bibliography on the general concept of contract.

A. Contracts

Here we propose a "primer" on contracts using a simple example as the reference for their use.

1) Components and their Environment, Contracts: We start from a model that consists of a universal set M of components, each denoted by the symbol M . A component M is typically an open system, i.e., it contains some inputs that are provided by other components in the system or the external world and it generates some outputs. This collection of other components and the exterior world is referred to as the environment of the component. The environment is often not completely known when the component is being developed. Although components cannot constrain their environment, they are designed to be used in a particular context.

In the following example, we define a component M 1 that computes the division between two real inputs x and y, and returns the result through the real output z. The underlying assumption is that M 1 will be used within a design context that prevents the environment from giving the input y = 0. Since M 1 cannot constrain its input variables, we handle the exceptional input y = 0 by generating an arbitrary output:

M 1 :        variables: inputs: x, y outputs: z types: x, y, z ∈ R behaviors: (y = 0 → z = x/y) ∧ (y = 0 → z = 0)
A contract contract, denoted by the symbol C, is a description of a component with the following characteristic properties:

1) Contracts are intentionally abstract; 2) Contracts distinguish responsibilities of a component from that of its environment Property 1) of a contract highlights the goal of handling complexity of the systems. Thus, contracts expose enough information about the component, but not more than necessary for the intended purpose. We can see a contract as an underspecified description of a component that can be either very close to the actual component, or specify only a single property of a component's behavior. Regarding Property 2), and in contrast to components, a contract explicitly makes a distinction between assumptions made about the environment, and guarantees provided, mirroring different roles and responsibilities in the design of systems.

A contract can be implemented by a number of different components and can operate in a number of different environments. Hence, we define a contract C at its most abstract level as a pair C = (E C , M C ) of subsets of components that implement the contract and of subsets of environments in which the contract can operate. We say that a contract C is

consistent if M C = ∅ and compatible if E C = ∅.
This definition of contracts and the implementation relation is very general and, as such, it is not effective. In concrete contract-based design theories, a contract needs to have a finite description that does not directly refer to the actual components, and the implementation relation needs to be effectively computable and establish the desired link between a contract and the underlying components that implement it. For our present simple example of static systems, we propose the following way to specify contracts:

C 1 :            variables:
inputs: x, y outputs: z types: x, y, z ∈ R assumptions: y = 0 guarantees: z = x/y C 1 defines the set of components having as variables {inputs: x, y; output: z} of type real, and whose behaviors satisfy the implication "assumptions ⇒ guarantees"

i.e., for the above example, y = 0 ⇒ z = x/y. Intuitively, contract C 1 specifies the intended behavior of components that implement division. It explicitly makes the assumption that the environment will never provide the input y = 0 and leaves the behavior for that input undefined. This contract describes an infinite number of environments in which it can operate, namely the set E C 1 of environments providing values for x and y, with the condition that y =0. It describes an infinite number of components that implement the above specification, where the infinity comes from the underspecified case on how an implementation of C 1 should cope with the illegal input y = 0. In particular, we have that M 1 implements C 1 . Thus, contract C 1 is consistent. We now show a variant of contract C 1 that is not consistent:

C 1 :            variables: inputs: x, y outputs: z types: x, y, z ∈ R assumptions: T guarantees: z = x/y RR n°8147
where symbol T denotes the boolean constant "true". In contrast to C 1 , the contract C 1 makes no assumption on values of the input y. Hence, every component that implements C 1 has to compute the quotient x/y for all values of y, including y = 0, which makes no sense.

B. Contract Operators

There are three basic contract operators that are used in support of the design methodologies we presented previously: composition, refinement and conjunction.

1) Contract Composition and System Integration: Intuitively, the composition operator supports component-based design and, in general, horizontal processes. The composition operator, that we denote by the symbol ×, is a partial function on components. The composition is defined with respect to a composability criterion, where two components M and M are composable if their variable types match. Composability is a syntactic property on pairs of components that defines conditions under which the two components can interact. Composition × must be both associative and commutative in order to guarantee that different composable components may be assembled together in any order.

Consider the component M 2 , defined as follows:

M 2 :        variables: inputs: x outputs: y types: x, y ∈ R behaviors: y = e x
The component M 2 computes the value of the output variable y as the exponential function of the input variable x. M 1 and M 2 are they are composable, since both common variables x and y have the same type, x is an input variable to both M 1 and M 2 , and the output variable y of M 2 is fed as an input to M 1 . It follows that their composition M 1 × M 2 has a single input variable x, and computes the output z as a function of x, that is z = x/e x . Now, consider component M 2 that consists of an input variable x and an output variable z, both of type real, where z = abs(x):

M 2 :        variables: inputs: x outputs: z types: x, z ∈ R behaviors: z = abs(x)
The component M 2 is not composable with M 1 , because the two components share the same output variable z. Their composition is illegal, as it would result in conflicting rules for updating z.

We now lift the above concepts to contracts. The composition operator between two contracts, denoted by ⊗, shall be a partial function on contracts involving a more subtle compatibility criterion. Two contracts C and C are compatible if their variable types match and if there exists an environment in which the two contracts properly interact. The resulting composition C ⊗ C should specify, through its assumptions, this set of environments. By doing so, the resulting contract will expose how it should be used. Unlike component composability, contract compatibility is a combined syntactic and semantic property.

Let us formalize this. For C a contract, let A C and G C be its assumptions and guarantees and define

G C1⊗C2 = G C1 ∧G C2 A C1⊗C2 = max    A A∧G C2 ⇒A C1 and A∧G C1 ⇒A C2    (1)
where "max" refers to the order of predicates by implication; thus A C1⊗C2 is the weakest assumption such that the two referred implications hold. Thus, this overall assumption will ensure that, when put in the context of a component implementing the second contract, then the assumption of the first contract will be met, and vice-versa. Since the two assumptions were ensuring consistency for each contract, the overall assumption will ensure that the resulting composition is consistent. This definition of the contract composition therefore meets our previously stated requirements. The two contracts C 1 and C 2 are called compatible if the assumption computed as in (1) differs from F, the " false" predicate.

Consider contracts C 2 and C 2 that we define as follows:

C 2 :          
C 1 ⊗ C 2 :           
variables: inputs: u, y outputs: x, z types: x, y, u, z ∈ R assumptions: y = 0 guarantees: x > u ∧ z = x/y C 1 and C 2 can also be composed and their composition yields:

C 1 ⊗ C 2 :            variables: inputs: v, x outputs: y, z types: v, x, y, z ∈ R assumptions: v = 0 guarantees: y = -v ∧ z = x/y
Both compositions possess a non-empty assumption (observe also that they are both free of exception), reflecting that the two pairs (C 1 , C 2 ) and (C 1 , C 2 ) are compatible.

In our example, we require that compositions C 1 ⊗(C 2 ⊗C 3 ) and (C 1 ⊗ C 2 ) ⊗ C 3 result in equivalent contracts, as well as compositions C 1 ⊗ C 2 and C 2 ⊗ C 1 , thus providing support for incremental system integration.

A quotient operation can be defined that is dual to the composition operation. Given a system-wide contract C and a contract C 1 that specifies pre-existing components and their interactions, the quotient operation C/C 1 defines the part of the system-wide contract that still needs to be implemented. It formalizes the practice of "patching" a design to make it behave according to another contract.

2) Contract Refinement and Independent Development:

In all vertical design processes, the notions of abstraction and refinement play a central role. The concept of contract refinement must ensure the following: if contract C refines contract C, then any implementation of C should 1) implement C and, 2) be able to operate in any environment for C. Hence the following definition for refinement pre-order between contracts: we say that the contract C refines the contract C, if In Figure 4 we start with the contract C 1 that represents the general system-wide requirements. We decompose these requirements into requirements of three subsystems, resulting in three contracts C For all contracts

E C ⊇ E C and M C ⊆ M C .
C 1 , C 2 , C 1 and C 2 , if C 1 is compatible with C 2 and C 1 C 1 and C 2 C 2 , then C 1 is compatible with C 2 and C 1 ⊗ C 2 C 1 ⊗ C 2 .
We now give a concrete example, where we start with very abstract requirements for a component that implements a function z = x/e x . Consider contracts C 1 and C 2 , that we define as follows:

C 1 :            variables: inputs: y outputs: z types: y, z ∈ R assumptions: y = 0 guarantees: z ∈ R C 2 :          
× M 2 implements C 1 ⊗ C 2 .
3) Contract Conjunction and Viewpoint Fusion: We now introduce the conjunction operator between contracts, denoted by the symbol ∧. Conjunction is complementary to composition:

1) In the early stages of design, the system-level specification consists of a requirements document that is a conjunction of requirements; 2) Full specification of a component can be a conjunction of multiple viewpoints, each covering a specific (functional, timing, safety etc.) aspect of the intended design and specified by an individual contract; see Figure 4 for an illustration. 3) Conjunction supports reuse of a component in different parts of a design; see Figure 5 for an illustration. We state the desired properties of the conjunction operator as follows: Let C 1 and C 2 be two contracts. If C 1 and C 2 are shared refinable, then

C 1 ∧ C 2 C 1 and C 1 ∧ C 2 C 2 , and for all contracts C, if C C 1 and C C 2 , then C C 1 ∧ C 2 .
To illustrate the conjunction operator, we consider a contract C T 1 that specifies the timing behavior associated with C 1 . For this contract, we introduce additional ports that allow us to specify the arrival time of each signal.

C T 1 :           
variables: inputs: t x , t y outputs: t z types: t x , t y , t z ∈ R + assumptions: T guarantees: t z ≤ max(t x , t y ) + 1

The contract C T 1 is shared refinable with C 1 . Their conjunction C 1 ∧ C T 1 yields a contract that guarantees, in addition to C 1 itself, a latency with bound 1 (say, in ms) for it. Because there are no assumptions, this timing contract specifies the same latency bound also for handling the illegal input y = 0. In fact, the contract says more: because it does not mention the input y, it assumes any value of y is acceptable. As a result, the conjunction inherits the weakest T assumption of the timing contract, and cancels the assumption of C 1 . This, however, is clearly not the intent, since the timing contract is not concerned with the values of the signals, and is a manifestation of the weakness of this simple contract framework in dealing with contracts with different alphabets of ports and variables. We will further explain this aspect, and show how to address this problem, in Section VII. For the moment, we can temporarily fix the problem by introducing y in the interface of the contract, and use it in the assumptions, as in the following contract

C T 2 C T 2 :           
variables: inputs: y, t x , t y outputs: t z types: y ∈ R; t x , t y , t z ∈ R + assumptions: y =0 guarantees: t z ≤ max(t x , t y ) + 1

Note that this timing contract does not specify any bound for handling the illegal input y = 0, since the promise is not enforced outside the assumptions. So far this example was extremely simple. In particular, it was stateless. Extension of this kind of Assume/Guarantee contracts to stateful contracts will be indeed fully developed in the coming sections and particularly in Section VII.

C. Contracts in requirement engineering

In this section we introduce a motivating example that is representative of early requirements capture-the specification of a parking garage. Its full development requires technical material that we introduce later and we thus defer it to Section XI. This example illustrates the following features of contract based requirements capture, namely:

• Top-level system specification is by writing a requirements document. Different formalisms may be used for different kinds of requirements. Here we illustrate this by blending textual requirements written in constrained English (possibly obtained using boilerplates) with small sized automata. • The document itself is structured into chapters describing various aspects of the system, such as how gates should behave, how payment should proceed, plus some overall rules. • Some requirements are under the responsibility of the system under development; they contribute to specifying the guarantees that the system offers. Other requirements are not under the responsibility of the system under development; they contribute to defining the assumptions regarding the context in which the system should operate as specified. • Requirements are written in constrained English language or by using automata. We now begin with the top-level requirements. The system under specification is a parking garage subject to payment by the user. At its most abstract level, the requirements document comprises the different chapters gate, payment, and supervisor, see Table III. The gate chapter will collect the generic requirements regarding entry and exit gates. These generic requirements will then be specialized for entry and exit gates, respectively.

Focus on the "gate" chapter. It consists of the three requirements shown on Table III by means of an i/o-automaton, shown in Figure 1-we provide an informal textual explanation for it, between quotes. Suppose that some requirement says: "?gate_open never occurs". This is translated by having no mention of ?gate_open in the corresponding i/o-automaton. To express this "negative" fact we must keep track of the fact that ?gate_open belongs to the alphabet of actions of the i/o-automaton. Thus, when performing the translation, the explicit list of inputs and outputs should be explicitly given. To avoid such additional notational burden, we have cheated by omitting this unless necessary. The other two requirements are written using constrained natural language, which can be seen as a boilerplate style of specification. Prefix "?" indicates an input and prefix "!" indicates an output.

The first two requirements are not under the responsibility of the system, since they rather concern the car driver. Thus it does not make sense to include them as part of the guarantees offered by the system. Should we remove them? This would be problematic. If drivers behave the wrong way unexpected things can occur for sure. The conclusion is that 1) we should keep requirements R g.1 and R g.2 , and 2) we should handle them differently than R g.3 , which is a guarantee offered by the system. Indeed, R g.1 and R g.2 are assumptions under which the gate operates as guaranteed. We take the convention that assumptions are written in italics.

So far we have specified gate as a list of requirements. Requirement R g.1 specified as an i/o-automaton can be considered formal. Requirements R g.2 and R g.3 are formulated in constrained natural language and are ready for subsequent formalization, e.g., as i/o-automata. Are we done? Not yet! We need to give a formal meaning to what it means to have a collection of requirements, and what it means to distinguish assumptions from guarantees. Similarly, we must give a formal meaning to what it means to combine different chapters of a requirements document. Intuitively, all requirements must be RR n°8147 met for a chapter to be satisfied, and, similarly, all chapters must be satisfied for the whole specification to be correctly implemented. Thus, we propose to write the top-level specification C as the following conjunction:

C = C gate ∧ C payment ∧ C supervisor
As we said, formally defining what conjunction ∧ is, requires technical material that is developed later in this paper. The following issues arise regarding this top-level specification. First of all, since a conjunction operator is involved in the construction of C, there is a risk of formulating contradicting requirements-this is referred to as the issue of consistency. Second, are we sure that the top-level specification C is complete, i.e., precise enough to rule out undesirable implementations? One good way of checking for completeness is to be able to execute or simulate this top-level specification C. We provide answers to all these issues in Section XI, where this example is fully developed. Having the top-level specification C at hand, the designer then specifies an architecture "à la SysML", as shown on Figure 2. Some comments are in order regarding this architecture. The considered instance of a parking garage consists of one entry gate, one exit gate, and one payment machine. Compare with the top-level specification of Table III. The latter comprises a generic gate, a payment machine, and a supervisor, each one with its set of requirements. In contrast, the architecture of Figure 2 involves no supervisor. The supervisor is meant to be distributed among the two gates. The architecture of Figure 2 seems to be very loosely coupled. First, the PaymentMachine seems to be totally independent. In fact, the ticket that is inserted in the exit gate must coincide with the one issued by the PaymentMachine. It turns out that this reflects a missing assumption regarding the environment of the system (namely the user of the parking). Then, the two gates seem to have the shared input "?vehicle exit" as their only interaction. But this shared input is involved in requirement R s.3 , which forbids the entry if the parking is full.

The next step in the design consists in subcontracting the development of each of the three sub-systems of the architecture of Figure 2. This amounts to specifying three subcontracts C EntryGate , C ExitGate , and C PaymentMachine , such that:

C EntryGate ⊗ C ExitGate ⊗ C PaymentMachine C (2)
The symbol in [START_REF] Abarbanel | FoCs -Automatic Generation of Simulation Checkers from Formal Specifications[END_REF] means that any implementation of the left hand side is also a valid implementation of the toplevel C. Then, the contract composition operator ⊗ ensures that each supplier can develop its sub-system based on its own sub-contract only, and, still, integrating the so designed sub-systems yields a correct implementation of the top-level specification. Once the three sub-contracts are found, checking that they satisfy (2) requires formalizing the contract composition operator ⊗. Furthermore, guessing such sub-contracts is a difficult task. In our development of this example in Section XI, we propose adequate answers to these issues.

D. Contract Support for Design Methodologies

The three operators introduced above fit naturally in any design methodology developed so far. In particular, contract composition and conjunction supports horizontal processes and contract refinement supports vertical processes. We show how this is so by first analyzing the use of contract conjunction for requirement management, then of composition and refinement for design chain management, re-use and independent development to close with conjunction, composition and refinement for deployment and mapping.

1) Supporting open systems: When designing components for reuse, their context of use is not fully known in advance. We thus need a specification of components exposing both the guarantees offered by the component and the assumptions on its possible context of use-its "environment". This states what contracts should be.

2) Managing Requirements and Fusing Viewpoints: Referring to Section III-C, complex systems involve a number of viewpoints (or aspects) that are generally developed by different teams using different skills. As a result, there is a need for fusing these viewpoints in a mathematically sound way. Structuring requirements or specifications is a desirable objective at each step of the design. Finally, we must formalize some key properties that must be evidenced as part of certification processes.

This process is illustrated in Figure 3. In this figure, we show three viewpoints: the behavioral viewpoint where the functions are specified, the timing viewpoint where timing budgets are allocated to the different activities, and the safety viewpoint where fault propagation, effect, and handling, are specified. Typically, different viewpoints are developed by different teams using different frameworks and tools. Development of each viewpoint is performed under assumptions regarding its context of use, including the other viewpoints. To

C = i C i C B 1 C B 2 C T C S 1 C S 2 C B 1 ∧ C B 2 ∧ C T ∧ C S 1 ∧ C S 2 Figure 3
. Conjunction of requirements and viewpoints in top-level design get the full system specification, the different viewpoints must be fused. As the notations of Figure 3 suggest, conjunction is used for fusing viewpoints, thus reflecting that the system under design must satisfy all viewpoints. Similarly, each viewpoint is itself a conjunction of requirements, seen as the "atomic" contracts-all requirements must be met.

3) Design Chain Management, Re-using, and Independent Development: In Figure 4, we show three successive stages of the design. At the top level sits the overall system specification as developed by the OEM. As an example, it can be obtained as the conjunction of several viewpoints as illustrated on Figure 3. is delegated for implementation by a supplier is delegated for implementation by a supplier

C11 ⊗ (C121 ⊗ C122) ⊗ (C131 ⊗ C132) C11 C12 C13 C11 C121 C122 C131 C132 C121 ⊗ C122 C131 ⊗ C132 C11 ⊗ C12 ⊗ C13 C1
is refined by the OEM As a first design step, the OEM decomposes its system into an architecture made of three sub-systems for independent development by (possibly different) suppliers. For each of these sub-systems, a contract C 1j , j = 1, 2, 3 is developed. A contract composition, denoted by the symbol "⊗",

C 11 ⊗ C 12 ⊗ C 13
mirrors the composition of sub-systems that defines the architecture. For our method to support independent development, this contract composition operator must satisfy the following: if designs are independently performed for each sub-contract C 1j , j = 1, 2, 3, then integrating these sub-systems yields an implementation that satisfies the composed contract C 11 ⊗ C 12 ⊗ C 13 .

(3) This contract composition must then be qualified against the top-level contract C 1 . This qualification must ensure that any development compliant with C 11 ⊗ C 12 ⊗ C 13 should also comply with C 1 . To ensure substitutability in any legal context, compliance concerns both how the system behaves and what its allowed contexts of use are: any legal context for C 1 should be also legal for C 11 ⊗ C 12 ⊗ C 13 and, under any legal context, the integrated system should behave as specified by C 1 . This is formalized as the refinement relation, denoted by the symbol :

C 11 ⊗ C 12 ⊗ C 13 C 1 (4)
Overall, the satisfaction of ( 4) guarantees the correctness of this first design step performed by the OEM.

Obtaining the three sub-contracts C 11 , C 12 , and C 13 , is the art of the designer, based on architectural considerations. Contract theories, however, offer the following services to the designer:

• The formalization of parallel composition and refinement for contracts allows the designer to firmly assess whether (4) holds for the decomposition step or not. • In passing, the compatibility of the three sub-contracts C 11 , C 12 , and C 13 , can be formally checked. • Using contracts as a mean to communicate specifications to suppliers guarantees that the information provided to the supplier is self-contained: the supplier has all the needed information to develop its sub-system in a way that subsequent system integration will be correct. Each supplier can then proceed with the independent development of the sub-system it is responsible for. For instance, a supplier may reproduce the above procedure.

Alternatively, this supplier can develop some sub-systems by reusing off-the-shelf components. For example, contract C 121 would be checked against the interface specification of a pre-defined component M 121 available from a library, and the following would have to be verified: does component M 121 satisfy C 121 ? In this context, shared implementations are of interest. This is illustrated on Figure 5 where the same offthe-shelf component implements the two referred contracts.

To conclude on this analysis, the two notions of refinement, denoted by the symbol " ", and composition of contracts, denoted by the symbol "⊗", are key. Condition (3) ensures independent development holds.

4) Deployment and Mapping:

Here we address a specific but important point related to Contribution 1. At some point in the design of the system, specifications must be realized by using resources. Resources can be pre-defined sub-systems or components, or they can consist of computing resources comprising computing units and communication media (networks, busses, and protocols). This methodology was advocated and When deploying an application over a computing platform, in addition to the functional viewpoint, non-functional viewpoints (safety, timing, energy and possibly other) are of importance as well. The safety viewpoint is concerned with the risk of primary faults and failures, how they could propagate throughout the system, and what the consequences for the resilience of the overall system would be in terms of failure probability. The timing viewpoint collects timing requirements regarding the application (requirements on latencies, throughput, jitter, and schedulability). The effective satisfaction of safety or timing viewpoints by a considered deployment depends on 1) the supporting execution platform and 2) the mapping of the application to this execution platform. We thus need to formalize what "mapping" means. The reader is referred to Figure 6 for the following discussion. Suppose one has a virtual model of the execution platform as an architecture composed of several components. Such components would, in the context of Figure 6, consist of a description of the available computing units, a description of the bus protocol and frame structure, and/or a library of RTOS (Real-Time Operating System) services. The resulting components are enhanced with timing information (for the timing viewpoint) and fault propagation information (for the safety viewpoint). Application contracts are attached to the different sub-systems or components as described on the top part of the figure. Similarly, platform contracts are attached to the different sub-systems or components of the execution platform, as described on the bottom part of the figure. Accordingly, we assume

C 11 C 121 C 122 C 131 C 132 C 11 ⊗ (C 121 ⊗ C 122 ) ⊗ (C 131 ⊗ C 132 ) C 121 ⊗ C 122 C 131 ⊗ C 132 C 122 ∧ C 132
M4 M3 M5 M6 M 1 M 2 M 3 M 1 M 4 M 2 M 5 M 6 x 34 x d
C = k i∈I k C ik P = j∈J ∈Lj P j
where:

• The overall platform contract P decomposes as j∈J P j (e.g., the bus and the different computing units in Figure 6) where each P j is the conjunction of its different viewpoints (the function: what can be computed; and the associated performance: how much time it takes and how much energy it consumes); • The overall application contract is the conjunction of its different viewpoints C i with their own architectural decomposition.

In Figure 6 we only show a single viewpoint 29 and we assume that distant communication between C 2 and C 3 has already been refined to a communication medium compliant with the communication resources offered by the execution platform.

The mapping of the application over the architecture is modeled by the conjunction C ∧P defined by the following set of synchronization tuples, 30 depicted in red in the Figure 6: • The wire x 34 linking M 3 to M 4 in the application is synchronized, in the deployment P, with the variable x 34 of the left computing unit, where x 34 represents the output of the module implementing M 3 and the input of the module implementing M 4 . And similarly for the wire linking M 5 to M 6 . • In the deployment, the wire x 63 linking M 6 to M 3 must traverse the bus. To capture this, we first refine the application architecture by distinguishing the origin x o 63 of this wire from its destination x d 63 . In the refined application architecture, we assume that x o This formalizes the deployment as the conjunction

C ∧ P = k i∈I k C ik j∈J ∈Lj P j
ensuring that C ∧ P refines C, by construction. There is, however, no free lunch. The formula C ∧ P expressing deployment involves a conjunction, and is, as such, a possible source of inconsistencies. If this happens, then C ∧ P cannot be implemented. Finding an execution platform P causing no inconsistency in C ∧ P requires a good understanding of the application and its needs. The more advanced techniques developed in Section XI provide assistance for this.

Since C ∧ P relates application and computing platformwhich sit at different layers of the design-we call such contracts vertical contracts. Contracts that are not vertical are sometimes called horizontal, in that they are meant to relate components sitting at a same level of the design hierarchyapplication level, or computing platform level, or ECU (Electronic Computing Unit) level.

Techniques of mapping application to its execution platform that are similar to the above one, are used in the RT-Builder tool 31 and in the Metropolis platform [START_REF] Balarin | Metropolis: An Integrated Electronic System Design Environment[END_REF], [START_REF] Densmore | Microarchitecture Development via Metropolis Successive Platform Refinement[END_REF].

E. Bibliographical note

Having collected the "requirements" on contract theories, it is now timely to confront these to the previous work referring to or related to the term "contract".

It is difficult to write a comprehensive bibliography on the general aspects of contract based design. The topic is multi faceted and has been addressed by several communities: software engineering, language design, system engineering, and formal methods in a broad sense. We report here a partial and limited overview of how this paradigm has been tackled in these different communities. While we do not claim being exhaustive, we hope that the reader will find her way to the different literatures.

Contracts in SW engineering: This part of the bibliographical note was inspired by the report [START_REF] Payne | Evaluation of Architectural Frameworks Supporting Contract-Based Specification[END_REF]. Design by Contract is a software engineering technique popularized by Bertrand Meyer [139], [START_REF] Meyer | Touch of Class: Learning to Program Well Using Object Technology and Design by Contract[END_REF] following earlier ideas from Floyd-Hoare logic [START_REF] Floyd | Assigning meaning to programs[END_REF], [START_REF] Hoare | An axiomatic basis for computer programming[END_REF]. Floyd-Hoare logic assigns meaning to sequential imperative programs in the form of triples of assertions {P, C, Q} consisting of a precondition on program states and inputs, a command, and a postcondition on program states and outputs. Meyer's contracts were developed for Object-Oriented programming. They expose the relationships between systems in terms of preconditions and postconditions on operations and invariants on states. A contract on an operation asserts that, given a state and inputs which satisfy the precondition, the operation will terminate in a state and will return a result that satisfy the postcondition and respects any required invariant properties. Contracts contribute to system substitutability. Systems may be replaced by alternative systems or assemblies that offer the same or substitutable functionality with weaker or equivalent preconditions and stronger/equivalent postconditions. With the aim of addressing service oriented architectures, Meyer's contracts were proposed a multiple layering by Beugnard et al. [START_REF] Beugnard | Making components contract aware[END_REF]. The basic layer specifies operations, their inputs, outputs and possible exceptions. The behavior layer describes the abstract behavior of operations in terms of their preconditions and postconditions. The third layer, synchronisation, corresponds to real-time scheduling of component interaction and message passing. The fourth, quality of service (QoS) level, details non-functional aspects of operations. The contracts proposed by Beugnard et al. are subscribed to prior to service invocation and may also be altered at runtime, thus extending the use of contracts to Systems of Systems [START_REF] Maier | Architecting Principles for Systems of Systems[END_REF]. So far contracts consisting of pre/postconditions naturally fit imperative sequential programming. In situations where programs may operate concurrently, interference on shared variables can occur. Rely/Guarantee rules [START_REF] Jones | Specification and design of (parallel) programs[END_REF] were thus added to interface contracts. Rely conditions state assumptions about any interference on shared variables during the execution of operations by the system's environment. Guarantee conditions state obligations of the operation regarding shared variables.

The concepts of interface and contract were subsequently further developed in the Model Driven Engineering (MDE) [START_REF] Karsai | Modelintegrated development of embedded software[END_REF], [START_REF] Schmidt | Model-driven engineering[END_REF], [START_REF] Ledeczi | Composing domain-specific design environments[END_REF]. In this context, interfaces are described as part of the system architecture and comprise typed ports, parameters and attributes. Contracts on interfaces are typically formulated in terms of constraints on the entities of components, using the Object Constraint Language (OCL) [150], [START_REF] Warmer | The Object Constraint Language: Getting Your Models Ready for MDA[END_REF]. Roughly speaking, an OCL statement refers to a context for the considered statement, and expresses properties to be satisfied by this context (e.g., if the context is a class, a property might be an attribute). Arithmetic or settheoretic operations can be used in expressing these properties. This method, however, does not account for functional and extra-functional properties of interfaces, i.e., for behavior and performance. To account for behavior, the classical approach in MDE consists in enriching components with methods that can be invoked from outside, and/or state machines. Likewise, attributes on port methods have been used to represent nonfunctional requirements or provisions of a component [START_REF] Cancila | Toward correctness in the specification and handling of non-functional attributes of high-integrity real-time embedded systems[END_REF]. The effect of a method is made precise by the actual code that is executed when calling this method. The state machine description and the methods together provide directly an implementation for the component -actually, several MDE related tools, such as GME and Rational Rose, automatically generate executable code from this specification [START_REF] Balasubramanian | Developing applications using model-driven design environments[END_REF], [START_REF] Ledeczi | The generic modeling environment[END_REF], [START_REF] Quatrani | Visual modeling with Rational Rose 2000 and UML[END_REF]. The notion of refinement is replaced by the concept of class inheritance. From a contract theory point of view, this approach has several limitations. Inheritance, for instance, is unable to cover aspects related to behavior refinement. Nor is it made precise what it means to take the conjunction of interfaces, which can only be approximated by multiple inheritance, or to compose them.

In a continuing effort since his joint work with W. Damm on Life Sequence Charts (LSC) in 2000 [START_REF] Damm | LSCs: Breathing life into message sequence charts[END_REF] with its Play-Engine implementation [START_REF] Harel | Come, Let's Play: Scenario-Based Programming Using LSCs and the Play-Engine[END_REF], David Harel has developed the concept of behavioral programming [START_REF] Harel | Behavioral programming[END_REF], [START_REF] Harel | Modelchecking behavioral programs[END_REF], [START_REF] Harel | Behavioral programming, decentralized control, and multiple time scales[END_REF], which puts in the forefront scenarios as a program development paradigm-not just a specification formalism. In behavioral programming, b-threads generate a flow of events via an enhanced publish/subscribe protocol. Each b-thread is a procedure that runs in parallel to the other b-threads. When a b-thread reaches a point that requires synchronization, it waits until all other b-threads reach synchronization points in their own flow. At synchronization points, each b-thread specifies three sets of events: requested events: the thread proposes that these be considered for triggering, and asks to be notified when any of them occurs; waited-for events: the thread does not request these, but asks to be notified when any of them is triggered; and blocked events: the thread currently forbids triggering any of these events. When all b-threads are at a synchronization point, an event is chosen (according to some policy), that is requested by at least one b-thread and is not blocked by any b-thread. The selected event is then triggered by resuming all the b-threads that either requested it or are waiting for it. This mechanism was implemented on top of Java and LSCs. The execution engine uses planning and model checking techniques to prevent the system from falling into deadlock, where all requested events are blocked. Behavioral programming is incremental in that new threads can be added to an existing program without the need for making any change to this original program: new deadlocks that are created by doing so are pruned away by the execution engine. While behavioral programming cannot be seen as a paradigm of contracts, it shares with contracts the objectives of incremental design and declarative style of specification.

Our focus-contracts for systems and CPS: The frameworks of contracts developed in the area of Software Engineering have established as useful paradigms for component based software system development. In this paper, we target the wider area of computer controlled systems, more recently referred to as Cyber-Physical systems, where reactive systems [START_REF] Harel | Statecharts: A visual formalism for complex systems[END_REF], [START_REF] Harel | On the development of reactive systems[END_REF], [START_REF] Halbwachs | Synchronous programming of reactive systems[END_REF], [START_REF] Manna | Temporal verification of reactive systems: Safety[END_REF] are encountered, that is systems that continuously interact with some environment, as opposed to transformational systems [START_REF] Halbwachs | Synchronous programming of reactive systems[END_REF], considered in Object-Oriented programming. For reactive systems, modelbased development (MBD) is generally accepted as a key enabler due to its capabilities to support early validation and virtual system integration. MBD-inspired design languages and tools include SysML [START_REF]System modeling language specification v1[END_REF] or AADL [START_REF] Hudak | The Architecture Analysis and Design Language (AADL): An Introduction[END_REF] for system level modeling, Modelica [START_REF] Fritzson | Principles of Object-Oriented Modeling and Simulation with Modelica 2[END_REF] for physical system modeling, Matlab-Simulink [START_REF] Karris | Introduction to Simulink with Engineering Applications[END_REF] for control-law design, and Scade [START_REF] Halbwachs | The synchronous data flow programming language Lustre[END_REF], [START_REF] Berry | The effectiveness of synchronous languages for the development of safety-critical systems[END_REF] and TargetLink for detailed software design. UML-related standardisation efforts in this area also include the MARTE UML 32 profile for real-time systems. Contract theories for model based development were considered in the community of formal verification. They were initially developed as specification formalisms able to refuse certain inputs from the environment. Dill proposed asynchronous 32 www.omgmarte.org trace structures with failure behaviors [START_REF] David | Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits[END_REF]. A trace structure is a representation of a component or interface with two sets of behaviors. The set of successes are those behaviors which are acceptable and guaranteed by the component. Conversely, the set of failures are behaviors which drive the component into unacceptable states, and are therefore refused. This work focuses primarily on the problem of checking refinement, and does not explore further the potentials of the formalism from a methodological point of view. The work by Dill was later extended by Wolf in the direction of synchronous systems. Negulescu later generalizes the algebra to Process Spaces which abstract away the specifics of the behaviors, and derives new composition operators [START_REF] Negulescu | Process Spaces and the Formal Verification of Asynchronous Circuits[END_REF]. This particular abstraction technique was earlier introduced by Burch with Trace Algebras to construct conservative approximations [START_REF] Burch | Trace Algebra for Automatic Verification of Real-Time Concurrent Systems[END_REF], and later generalized by Passerone and Burch [START_REF] Passerone | Refinement preserving approximations for the design and verification of heterogeneous systems[END_REF] to study generic trace structures with failure behaviors and to formalize the problem of computing the quotient (there called mirror) [START_REF] Passerone | Semantic Foundations for Heterogeneous Systems[END_REF]. This paper aims at proposing, for model based design of systems and CPS, a new vista on contracts. In the next section, we propose an all encompassing meta theory of contracts.

V. A MATHEMATICAL META-THEORY OF CONTRACTS

In software engineering, meta-models are "models of models", i.e., formal ways of specifying a certain family of models. Similarly, we call here meta-theory a way to specify a particular family of theories. In this section we propose a meta-theory of contracts. This meta-theory is summarized in Table IV. It comes as a few primitive concepts, on top of which derived concepts can be built. A number of key properties can be proved about the resulting framework. These properties demonstrate that contracts are a convenient paradigm to support incremental development and independent implementability in system design. The meta-theory will serve as a benchmark for our subsequent review of concrete contract theories.

The meta-theory we develop here is novel. There are very few attempts of that kind. In fact, the only ones we are aware of are the recent works by Bauer et al. [START_REF] Bauer | Moving from specifications to contracts in component-based design[END_REF] and Chen et al. [START_REF] Chen | A compositional specification theory for component behaviours[END_REF], which follow a different (and complementary) approach. The discussion of this work is deferred to the bibliographical section V-H.

A. Components and their composition

To introduce our meta-theory, we start from a universe M of possible components, each denoted by the symbol M or E, and a universe of their abstractions, or contracts, each denoted by the symbol C. Our meta-theory does not presume any particular modeling style, neither for components nor for contracts-we have seen in Section IV an example of a (very simple) framework for static systems. More generally, some frameworks may represent components and contracts with sets of discrete time or even continuous time traces, other theories use logics, or state-based models of various kinds, and so on.

We assume a composition M 1 × M 2 acting on pairs of components. Component composition × is partially, not to- Table IV Summary of the meta-theory of contracts. We first list primitive concepts and then derived concepts introduced by the meta-theory. tally, defined. Two components that can be composed are called composable. Composability of components is meant to be a typing property. In order to guarantee that different composable components may be assembled together in any order, it is required that component composition × is associative and commutative. Components that exhibit no means for interacting with the outside world are called closed; other components are open. An environment for a component M is another component E composable with M and such that M × E is closed.

C 1 ⊗C 2 is defined if M 1 |= M C 1 M 2 |= M C 2 ⇒ (M 1 , M 2 ) composable C 1 ⊗C 2 =    C M 1 |= M C 1 and M 2 |= M C 2 and E |= E C ⇓ M 1 × M 2 |= M C and E×M 2 |= E C 1 and E×M 1 |= E C 2    Assumption

B. Contracts

In our primer of Section IV, we have highlighted the importance of the legal environments associated with contracts, for which an implementation will operate satisfactorily. At the abstract level of the meta-theory, we make this explicit next:

Definition 1: A contract is a pair C = (E C , M C ), where: • M C ⊆ M is the set of implementations of C, and • E C ⊆ M is the set of environments of C.
For any pair (E, M ) ∈ E C × M C , E is an environment for M . Hence, M ×E must be well defined and closed. A contract possessing no implementation is called inconsistent.

A contract possessing no environment is called incompatible. Write M |= M C and E |= E C to express that M ∈ M C and E ∈ E C , respectively.
In concrete theories of contracts, both components and contracts are described in some finite (preferably concise) way.

In turn, it is not true that every set M ⊆ M of components can be represented as M = M C for some contract C and similarly for sets of environments. To highlight this, we assume a family C of expressible contracts.

(

) 5
Only contracts belonging to this family can be considered. This is made explicit in Table IV.

C. Refinement and conjunction

To support independent implementability, the concept of contract refinement must ensure the following: if contract C refines contract C, then any implementation of C should 1) implement C and 2) be able to operate in any environment for C. Hence the following definition for refinement preorder between contracts: C refines C, written C C, if and only if M C ⊆ M C and E C ⊇ E C . As a direct consequence, the following property holds, which justifies the use of the term "refinement" for this relation:

Property 1 (refinement):

1) Any implementation of C is an implementation of C: M |= M C ⇒ M |= M C, and
2) Any environment of C is an environment of C : E |= E C ⇒ E |= E C .
The conjunction of contracts C 1 and C 2 , written C 1 ∧ C 2 , is the greatest lower bound (GLB) of these two contracts with respect to refinement order-we assume such a GLB exists.

The intent is to define this conjunction as the intersection of sets of implementations and the union of sets of environments. However, due to [START_REF] Luca | Interface-based design[END_REF], not every set of components is the characteristic set of a contract. The best approximation consists in taking the greatest lower bound for the refinement relation.

The following immediate properties hold: Property 2 (shared refinement):

1) Any contract that refines C 1 ∧ C 2 also refines C 1 and C 2 . Any implementation of C 1 ∧ C 2 is a shared implementa- tion of C 1 and C 2 . Any environment of C 1 or C 2 is an environment of C 1 ∧ C 2 . 2) For C ⊆ C a subset of contracts, C is compatible if
and only if there exists a compatible C ∈ C.

The conjunction operation formalizes the intuitive notion of a "set of contracts" or a "set of requirements".

D. Contract composition

The objective of contract composition is to ensure that: 1) composing respective implementations of each contract yields an implementation for the composition, and, 2) composing an environment for the resulting composition with an implementation for C 2 yields an environment for C 1 and vice-versa. These two properties are essential in supporting top-down design by successive decompositions and refinements of contracts. Contract composition C 1 ⊗ C 2 is thus defined on top of component composition as indicated in Table IV, with the following assumption in force throughout this meta-theory:

Assumption 1: The following condition holds: The following lemma will be instrumental:

C 1 ⊗ C 2 ∈ C C1⊗C2 (Note
Lemma 1: Let four contracts be such that C 1 C 1 , C 2 C 2 , and C 1 ⊗ C 2 is well defined. Then, so is C 1 ⊗ C 2 and C C 1 ⊗C 2 ⊇ C C1⊗C2 . Proof: Since C 1 ⊗ C 2 is
well defined, it follows that every pair (M 1 , M 2 ) of respective implementations of these contracts is a composable pair of components. Hence, C 1 ⊗C 2 is well defined according to the formula of Table IV

. Next, since C 1 C 1 and C 2 C 2 and using Assumption 1, M 1 |= M C 1 and M 2 |= M C 2 implies M 1 |= M C 1 and M 2 |= M C 2 ; similarly E × M 2 |= E C 1 and E ×M 1 |= E C 2 implies E ×M 2 |= E C 1 and E ×M 1 |= E C 2 .
Therefore, replacing, in the big brackets defining the contract composition, C 1 by C 1 and C 2 by C 2 can only increase the set C C1⊗C2 .

2

To conform to the usage, we say that C 1 and C 2 are compatible contracts if their composition C 1 ⊗ C 2 is defined and compatible in the sense of Table IV. The following properties are a direct corollary of Lemma 1:

Property 3 (independent implementability): For all con- tracts C 1 , C 2 , C 1 and C 2 , if 1) C 1 is compatible with C 2 , 2) C 1 C 1 and C 2 C 2 hold, then C 1 is compatible with C 2 and C 1 ⊗ C 2 C 1 ⊗ C 2 .
Thus, compatible contracts can be independently refined. This property holds in particular if C 1 and C 2 are singletons:

Corollary 1: Compatible contracts can be independently implemented.

Property 3 is fundamental, particularly in top-down design. Top-down incremental design consists in iteratively decomposing a system-level contract C into sub-system contracts C i , i ∈ I for further independent development. To ensure that independent development will not lead to integration problems, it is enough to verify that i∈I C i C. We insist that, since contracts are purposely abstract and subsystems are not many, the composition of contracts C i will not typically result in state explosion. 33The following property is essential as it states that contract composition can be performed in any order and changes in architecture (captured by changes in parenthesizing) are allowed:

Property 4 (associativity and commutativity): For all contracts C 1 , C 2 , C 3 and C 4 , if C 1 and C 2 are compatible, C 3 and C 4 are compatible and C 1 ⊗C 2 is compatible with

C 3 ⊗C 4 , then C 1 is compatible with C 3 , C 2 is compatible with C 4 , C 1 ⊗ C 3 is compatible with C 2 ⊗ C 4 ,

and

(C 1 ⊗ C 2 ) ⊗ (C 3 ⊗ C 4 ) = (C 1 ⊗ C 3 ) ⊗ (C 2 ⊗ C 4 ) (6)
Proof: To shorten notations, write C 12 instead of C 1 ⊗ C 2 and similarly for any subset of {1, 2, 3, 4}. By Assumption 1 and the associativity and commutativity of component composition, C 1234 is characterized by the following two properties, where index i ranges over the set 1. . .4:

M i |= M C i ⇒ M 1 × . . . ×M 4 |= M C 1234 E |= E C 1234 ⇒ E× (× j =i M j ) |= E C i (7)
Observe that ( 7) is fully symmetric, which proves [START_REF] Alur | A theory of timed automata[END_REF]. Next, using the assumptions regarding compatibility, we derive the existence of at least one environment E satisfying the premise of the second implication of [START_REF] Alur | A determinizable class of timed automata[END_REF]. Since ( 7) is fully symmetric, this proves the conclusions of Property 4 regarding compatibility. 2

Property 5 (distributivity): If the following contract compositions are all well defined, then the following holds:

[(C 11 ∧ C 21 ) ⊗ (C 12 ∧ C 22 )] [(C 11 ⊗ C 12 ) ∧ (C 21 ⊗ C 22 )] (8) Proof: By Lemma 1, C (C11∧C21)⊗(C12∧C22) ⊇ C C11⊗C12 .
Taking the GLB of these two sets thus yields

[(C 11 ∧ C 21 ) ⊗ (C 12 ∧ C 22 )] (C 11 ⊗ C 12 )
and similarly for (C 21 ⊗ C 22 ). Thus, (8) follows.

2

The use of distributivity is best illustrated in the following context. Suppose the system under design decomposes into two sub-systems labeled 1 and 2, and each subsystem has two viewpoints associated with it, labeled by another index with values 1 or 2. Contract (C 11 ∧ C 21 ) is then the contract associated with sub-system 1 and similarly for sub-system 2. Thus, the left hand side of (8) specifies the set of implementations obtained by, first, implementing each sub-system independently, and then, composing these implementations. Property 5 states that, by doing so, we obtain an implementation of the overall contract obtained by, first, getting the two global viewpoints (C 11 ⊗ C 12 ) and (C 21 ⊗ C 22 ), and, then, taking their conjunction. This property supports independent implementation for specifications involving multiple viewpoints. Observe that only refinement, not equality, holds in [START_REF] Alur | Event-clock automata: A determinizable class of timed automata[END_REF].

E. Quotient

The quotient of two contracts is defined in Table IV. It is the adjoint of the product operation ⊗ in that C 1 /C 2 is the most general context C in which C 2 refines C 1 . It formalizes the practice of "patching" a component to make it behaving according to another specification. From its definition in Table IV, we deduce the following property: Property 6 (quotient): The following holds:

C C 1 /C 2 ⇔ C ⊗ C 2 C 1
Proof: Immediate, from the definition. 2

F. Discussion

By inspecting Table IV, the different notions can be classified into the following two categories:

• Primitive notions that are assumed by the meta-theory.

This category comprises: components, component composability and composition. • Derived notions comprise: contract; refinement, conjunction, composition, and quotient; consistency and compatibility for contracts. The derived notions follow from the primitive ones through set theoretic, non effective, definitions. The meta-theory offers by itself a number of fundamental properties that underpin incremental development and independent implementability. Concrete theories will offer definitions for the primitive notions as well as effective means to implement (or sometimes approximate) the derived notions. Observers and then abstract interpretation we develop next provide generic approaches to recover effectiveness.

G. Observers

Notion Observer

C = (E C , M C ) b E C , b M C C = C 1 ∧C 2 b E C = b E C 1 ∨ b E C 2 , b M C = b M C 1 ∧ b M C 2 C = C 1 ∨C 2 b E C = b E C 1 ∧ b E C 2 , b M C = b M C 1 ∨ b M C 2 C = C 1 ⊗C 2 b E C (E) =    b M C 1 (M 1 ) ∧ b M C 2 (M 2 ) ⇓ b E C 2 (E×M 1 ) ∧ b E C 1 (E×M 2 ) b M C (M 1 × M 2 ) = b M C 1 (M 1 ) ∧ b M C 2 (M 2 )

Table V Mirroring the algebra of contracts with observers.

A typical obstacle in getting finite (or, more generally, effective) representations of contracts is the occurrence of infinite data types and functions having infinite domains. These can be dealt with by using observers, which originate from the basic notion of test for programs:

Definition 2: Let C be a contract. An observer for C is a pair (b E C , b M C ) of non-deterministic boolean functions M → {F, T} called verdicts, such that: b E C (M ) outputs F =⇒ M ∈ E C b M C (M ) outputs F =⇒ M ∈ M C (9)
The functions M → b E C (M ) and M → b M C (M ) being both non-deterministic accounts for the fact that the outcome of a test depends on the stimuli from the environment and possibly results from internal non-determinism of the tested component itself. Note the single-sided implication in [START_REF] Alur | Alternatingtime temporal logic[END_REF], which reflects that tests only provide semi-decisions.

Relations and operations of the meta-theory can be mirrored by relations and operations on observers as explained in Table V-we omit the formulas for the quotient as semieffectiveness of testing makes it useless. Despite GLB and LUB can be mirrored using the formulas of the table, nothing can be said about the relationship of observers for contracts based on the fact that they are in a refinement ordering. Dually nothing can be inferred in terms of their refinement from such a relationship between the observers. Still, the following weaker result holds, which justifies how GLB and LUB are represented using observers in Table V:

Lemma 2: Let (b E C , b M C ) be an observer for C and let C C. Then, any pair (b E , b M ) satisfying b E ≥ b E C and b M ≤ b M C is an observer for C .
The following immediate results hold, regarding consistency and compatibility:

Lemma 3:

1) If b E C (E) outputs F for all tested environment E, then C is incompatible; 2) If b M C (M ) outputs F for all tested component M , then C is inconsistent.
To summarize, Definition 2 provides semi-decision procedures to check whether a component or an environment are valid for a contract. Lemma 3 provides semi-decision procedures for checking consistency and compatibility. Finally, Table V indicates how operations from the contract algebra can be reflected into operations on observers.

Due to the need for exercising all components or environments, using observers for checking consistency or compatibility is still non-effective. For concrete theories exhibiting some notion of "strongest" environment or component for the considered contract, a reinforcement of Lemma 3 will ensure effectiveness.

In Section VI where concrete theories are reviewed, we indicate, for each theory, how observers can be constructed and how Lemma 3 specializes.

H. Bibliographical note

Abstract contract theories and features of our presentation: Our presentation here is new. There is only a small literature providing an abstract formalization of the notion of contracts. The only attempts we are aware of are the recent works by Bauer et al. [START_REF] Bauer | Moving from specifications to contracts in component-based design[END_REF] and Chen et al. [START_REF] Chen | A compositional specification theory for component behaviours[END_REF], albeit with deeply different and complementary approaches.

The publication [START_REF] Bauer | Moving from specifications to contracts in component-based design[END_REF] develops an axiomatization of the notion of specification, from which contracts can be derived in a second step. More precisely, specifications are abstract entities that obey the following list of axioms: it possesses a refinement relation that is a preorder, which induces a notion of equivalence of specifications, and a parallel composition that is associative, commutative (modulo equivalence), and monotonic with respect to refinement. It is assumed that, if two specifications possess a common lower bound, then they possess a greatest lower bound. A quotient is also assumed, which is the residuation of the parallel composition. From specifications, contracts are introduced as pairs of specifications, very much like Assume/Guarantee contracts we develop in Section VII are pairs of assertions. Sets of legal environments and sets of implementations are associated to contracts. Finally modal contracts are defined by borrowing ideas from modal specifications we discuss in Section VIII. This abstract theory nicely complements the one we develop here in that it shows that both specifications and contracts can be defined as primitive entities and be used to build more concrete theories.

The work [START_REF] Chen | A compositional specification theory for component behaviours[END_REF] develops the concept of declarative specification, which consists of a tuple P = (Σ in , Σ out , T Σ , F Σ ), where Σ in and Σ out are input and output alphabets of actions, Σ = Σ in Σ out , and T Σ , F Σ ⊆ Σ * such that F Σ ⊆ T Σ are sets of permissible and inconsistent traces, respectivelythis approach find its origins in earlier work by Dill [START_REF] David | Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits[END_REF] and Negulescu [START_REF] Negulescu | Process Spaces and the Formal Verification of Asynchronous Circuits[END_REF]. Outputs are under the control of the component, whereas inputs are issued by the environment. Thus, after any successful interaction between the component and the environment, the environment can issue any input α, even if it will be refused by the component. If α is refused by the component after the trace t ∈ T Σ , t.α ∈ F Σ is an inconsistent trace, capturing that a communication mismatch has occurred. An environment is called safe if it can prevent a component from performing an inconsistent trace. For Q to be used in place of P it is required that Q must exist safely in any environment that P can exist in safely; this is the basis on which refinement is defined. Alphabet extension is used, by which input actions outside the considered alphabet are followed by an arbitrary behavior for the declarative specification. A conjunction is proposed that is the GLB for refinement order. A parallel composition is proposed, which is monotonic with respect to refinement. A quotient is also proposed, which is the residuation of parallel composition.

Observers: Observers, being related to the wide area of software and system testing, have been widely studied.

A number of existing technologies support the design of observers and we review some of them now.

Synchronous languages [START_REF] Benveniste | The synchronous approach to reactive and real-time systems[END_REF], [START_REF] Halbwachs | Synchronous programming of reactive systems[END_REF], [START_REF] Benveniste | The Synchronous Languages 12 years later[END_REF] are a formalism of choice in dealing with observers. The family of Synchronous Languages comprises mainly the imperative language Esterel [START_REF] Boussinot | The Esterel language[END_REF], [START_REF] Potop | Compiling Esterel[END_REF] and the dataflow languages Lustre [START_REF] Halbwachs | The synchronous data flow programming language Lustre[END_REF] and Signal [START_REF] Le | Programming real-time applications with Signal[END_REF]. The family has grown with several children offering statecharts-like interfaces and blending dataflow and statechart-based styles of programming, such as in Scade V6 34 . Synchronous languages support only systems governed by discrete time, not systems with continuous time dynamics (ODEs). They benefit from a solid mathematical semantics. As a consequence, executing a given program always yields the same results (results do not depend on the type of simulator). The simulated or analysed program is identical to the code for embedding. Thanks to these unique features, specifications can easily be enhanced with timing and/or safety viewpoints. The RT-Builder 35 tool on top of Signal is an example of framework supporting the combination of functional and timing viewpoints while analyzing an application deployed over a virtual architecture (see Section IV-D4). The widely used Simulink/Stateflow 36 tool by The Mathworks offers similar features. One slight drawback is that its mathematical seman-tics is less firmly defined (indeed, results of executions may differ depending on the code executed: simulation or generated C code). On the other hand, Simulink supports continuous time dynamics in the form of systems of interconnected ODEs (Ordinary Differential Equations), thus supporting the modeling of the physical part of the system. Using Simulink, possibly enhanced with SimScape, 37 allows for including physical system models in observers, e.g., as part of the system environment. The same comment holds regarding Modelica. 38 Actually, observers have been proposed and advocated in the context of Lustre and Scade [START_REF] Halbwachs | Programming and Verifying Real-Time Systems by Means of the Synchronous Data-Flow Language Lustre[END_REF], [START_REF] Halbwachs | Synchronous observers and the verification of reactive systems[END_REF], [START_REF] Halbwachs | Validation of synchronous reactive systems: From formal verification to automatic testing[END_REF], Esterel [START_REF] Bouali | XEVE, an Esterel Verification Environment[END_REF], and Signal [START_REF] Marchand | Synthesis of Discrete-Event Controllers Based on the Signal Environment[END_REF], [START_REF] Marchand | Incremental Design of a Power Transformer Station Controller Using a Controller Synthesis Methodology[END_REF]. More precisely, Scade advocates expressing tests using Scade itself. Tests can then easily be evaluated at run time while executing a Scade program. To conclude, observe that synchronous languages and formalisms discussed in this section are commercially available and widely used.

Another good candidate for expressing observers is the Property Specification Language (PSL). PSL is an industrial standard [START_REF]IEEE Standard for Property Specification Language (PSL)[END_REF], [START_REF] Eisner | Formal Syntax and Semantics of PSL -Appendix B of Accellera LRM January 2003[END_REF], [START_REF] Eisner | PSL for Runtime Verification: Theory and Practice[END_REF] for expressing functional (or behavioral) properties targeted mainly to digital hardware design. We believe that PSL is indeed very close to several, less established but more versatile formalisms based on restricted English language that are used in industrial sectors other than digital hardware, e.g., in aeronautics, automobile, or automation. Consider the following property:

" For every sequence that starts with an a immediately followed by three occurrences of b and ends with a single occurrence of c, d holds continuously from the next step after the end of the sequence until the subsequent occurrence of e. " This property is translated into its PSL version

{ [ * ];a;b[ * 3];c } |=> (d until! e)
PSL is a well-suited specification language for expressing functional requirements involving sequential causality of actions and events. Although we are not aware of the usage of PSL in the particular context of contract-based design, we mention the tool FoCS [START_REF] Abarbanel | FoCs -Automatic Generation of Simulation Checkers from Formal Specifications[END_REF] that translates PSL into checkers that are attached to designs. The resulting checker takes the form of an observer, if the PSL specification is properly partitioned into assumption and guarantee properties. More recently, PSL was also used for the generation of transactors that may adapt high-level requirements expressed as transactionlevel modules to the corresponding register-transfer implementation [START_REF] Balarin | Specification, synthesis and simulation of transactor processes[END_REF], [START_REF] Balarin | Functional verification methodology based on formal interface specification and transactor generation[END_REF]. It follows that the existing tool support for PSL makes this specification language suitable in the contractbased design using observers. We note that the availability of formal analysis tools allows the design to be checked exhaustively-this is, of course, at the price of restrictions on data types. Another benefit in using PSL as an observerbased interface formalism is an existing methodology for userguided automated property exploration built around this lan-37 http://www.mathworks.com/products/simscape/ 38 https://www.modelica.org/ guage [START_REF] Pill | Property simulation[END_REF], [START_REF] Bloem | Manual for property-based synthesis tool[END_REF], that is supported by the tool RATSY [START_REF] Bloem | RATSY -A New Requirements Analysis Tool with Synthesis[END_REF]. As previously stated, PSL is built on top of LTL and regular expressions. One can thus express liveness properties in PSL, which are not suitable for online monitoring. There are two orthogonal ways to avoid this potential issue: (1) restricting the PSL syntax to its safety fragment; or (2) adapting the PSL semantics to be interpreted over finite traces [START_REF] Eisner | Reasoning with temporal logic on truncated paths[END_REF]. A survey of using PSL in runtime verification can be found in [START_REF] Eisner | PSL for Runtime Verification: Theory and Practice[END_REF].

Another relevant formalism for building observers consists of the Live Sequence Charts (LSC) [START_REF] Damm | LSCs: Breathing life into message sequence charts[END_REF], [START_REF] Harel | Come, Let's Play: Scenario-Based Programming Using LSCs and the Play-Engine[END_REF], [START_REF] Harel | Accelerating smart play-out[END_REF]. LSC are a graphical specification language based on scenarios that is an extension of Message Sequence Charts (MSC) 39 . A typical LSC consists of a prechart and a main chart. The semantics is that whenever the prechart is satisfied in a run of the system, eventually the main chart must also be satisfied. Precharts should not be confused with assumptions, however, they are rather sort of "prerequisites". LSCs are multi-modal in that any construct in the language can be either cold or hot, with a semantics of "may happen" or "must happen", respectively. If a cold element is violated (say a condition that is not true when reached), this is considered a legal behavior and some appropriate action is taken. Violation of a hot element, however, is considered a violation of the specification and is not allowed to happen in an execution. LSC are executable. The execution of a set of LSCs is called play out by the authors [START_REF] Harel | Come, Let's Play: Scenario-Based Programming Using LSCs and the Play-Engine[END_REF]. Play out is useful for checking an LSC specification against a property [START_REF] Damm | Live and let die: LSC based verification of UML models[END_REF]. LSC can be used as (expressive) tests to monitor the execution of a design over non-terminating runs. While doing so, the same rules as above are applied, except that the design controls the emission of events and the LSC specification is used to react in case of violation of the specification. This is manifested by the absence of rules explaining the occurrence of some event at run-time. This procedure is called play in by the authors. To conclude, LSCs are well suited to express observers.

VI. PANORAMA OF CONCRETE THEORIES

For the coming series of sections where concrete contract theories are reviewed, the reader is referred to Table IV of Section V, where the meta-theory of contracts is developed. We will illustrate how various concrete contract theories can be developed by specializing the meta-theory. VII. PANORAMA: ASSUME/GUARANTEE CONTRACTS Our static example of Section IV provided an example of contract specified using Assumptions and Guarantees. Assume/Guarantee contracts (A/G-contracts), Assumptions characterize the valid environments for the considered component, whereas the Guarantees specify the commitments of the component itself, when put in interaction with a valid environment. Various kinds of A/G-contract theories can be obtained by specializing the meta-theory in different ways. Variations concern how the composition of components is defined. We will review some of these specialization and relate them to the existing literature.

In general, A/G contract theories build on top of component models that are assertions, i.e., sets of behaviors or traces assigning successive values to variables. As we shall see, different kinds of frameworks for assertions can be considered, including asynchronous frameworks of Kahn Process Networks (KPN) [START_REF] Kahn | The Semantics of Simple Language for Parallel Programming[END_REF] and synchronous frameworks in which behaviors are sequences of successive reactions assigning values to the set of variables of the considered system. We first develop the theory for the simplest case of a fixed alphabet. Then, we develop the other cases.

A. Dataflow A/G contracts

For this simplest variant, all components and contracts involve a same alphabet Σ of variables, possessing identical 40domain D.

With this simplification, a component M identifies with an assertion

P ⊆ Σ → D * ∪ D ω (10)
i.e., a subset of the set of all finite or infinite behaviors over alphabet Σ; such a behavior associates, to each symbol x ∈ Σ, a finite or infinite flow of values. The flows are not mutually synchronized and there is no global clock or logical step. We discuss in Section VII-D variants of this framework with more synchronous models of behaviors. For convenience, we feel free to use both set theoretic and boolean notations for the relations and operations on assertions. Two components are always composable and we define component composition by the intersection of their respective assertions:

P 1 ×P 2 = P 1 ∧P 2 (11)
Formulas ( 10) and ( 11) define a framework of asynchronous components, with no global clock and no notion of reaction. Instead, a component specifies a relation between the histories of its different flows. When input and output ports are considered as in Section VII-B and components are input/output functions, we obtain the model of Kahn Process Networks [START_REF] Kahn | The Semantics of Simple Language for Parallel Programming[END_REF] widely used for the mapping of synchronous programs over distributed architectures [START_REF] Potop-Butucaru | Concurrency in synchronous systems[END_REF], [START_REF] Potop-Butucaru | Necessary and sufficient conditions for deterministic desynchronization[END_REF]. Next, for C and C two saturated contracts with identical input and output alphabets,

refinement C C holds iff A ≥ A G ≤ G (12)
Conjunction follows from the refinement relation: for C 1 and C 2 two saturated contracts with identical input and output alphabets:

C 1 ∧ C 2 = (A 1 ∨A 2 , G 1 ∧G 2 ).
Focus now on contract composition C = C 1 ⊗ C 2 , for two saturated contracts-this is no loss of generality, as we have seen. Contract composition instantiates through the following formulas, cf. [START_REF] Abadi | Conjoining specifications[END_REF] in Section IV:

G = G 1 ∧G 2 A = max    A A∧G 2 ⇒A 1 and A∧G 1 ⇒A 2    (13)
which satisfies Assumption 1 of the meta-theory. If, furthermore, contracts are saturated, then [START_REF]Road vehicles -functional safety[END_REF] reformulates as the formulas originally proposed in [START_REF] Benveniste | Multiple viewpoint contract-based specification and design[END_REF]:

G = G 1 ∧ G 2 A = (A 1 ∧ A 2 ) ∨ ¬(G 1 ∧ G 2 ) (14)
Observe that the so obtained contract (A, G) is saturated:

G ∨ A = (G 1 ∧ G 2 ) ∨ (A 1 ∧ A 2 ) ∨ ¬(G 1 ∧ G 2 ) = T.
No quotient operation is known for Assume/Guarantee contracts.

We finish this section by observing that the two contracts C 1 and C 1 of Section IV-A1 satisfy C 1 C 1 according to the theory of this section: guarantees are identical but assumptions are relaxed.

B. Capturing exceptions

Referring to the primer of Section IV-A1 and its static system example, dividing by zero may raise an exception. For instance, a careless designer may consider, instead of M 1 , a slight variation M 1 of it where the behaviors are only partially defined:

M 1 : behaviors (y = 0 → z = x/y)
leaving what happens if a value 0 is submitted for y unspecified. In practice, y = 0 would raise an exception, leading to an unpredictable outcome and possibly a crash unless exception handling is offered as a rescue by the execution platform.

In this section, we show how a mild adjustment of our theory of A/G contracts can capture exceptions and their handling. To simplify, we develop this again for the case of a fixed alphabet Σ. We only present the add-ons with respect to the previous theories, the parts that remain unchanged are not repeated.

Since exceptions are undesirable events caused by the component itself and not by its inputs-for our simple example, the exception is the improper handling of the division by zero-we need to include inputs and outputs as part of our framework for components.

A component is thus a tuple M = (Σ in , Σ out , P ), where Σ = Σ in ∪ Σ out is the decomposition of alphabet Σ into its inputs and outputs, and P ⊆ (Σ → (D * ∪ D ω )) is an assertion. Whenever convenient, we shall denote by Σ in M , Q M , P M , etc., the items defining component

M . Components M 1 and M 2 are composable if Σ out 1 ∩ Σ out 2 = ∅. If so, then M 1 ×M 2 = (Σ in , Σ out , P ) is well defined, with Σ out = Σ out 1 ∪ Σ out 2 , Σ in = Σ -Σ out
, and P = P 1 ∩ P 2 . Let us now focus on exceptions. To capture improper response (leading to a "crash"), we distinguish a special element fail ∈ D. We assume that crash is not revertible, i.e., in any behavior of the component, any variable remains at fail when it reaches that value. Referring to the static example of Section IV, we would then set x/0 := fail for any x. We are now ready to formalize what it means, for a component, to be free of exception:

Definition 4: A component M is free of exception if:
1) It accepts all inputs:

pr Σ in M (P M ) = Σ in M → (D * ∪D ω )
2) It does not cause by itself the occurrence of fail in its behaviors: for any behavior σ ∈ P M , if the projection pr Σ in M (σ) of σ to the input alphabet Σ in M does not involve fail , then neither does σ.

Exception freeness defined in this way is such that, if M 1 and M 2 are both composable and free of exception, then M 1 ×M 2 is also free of exception. Hence, we are free to restrict our universe of components to exception free components-thus, Definition 4 defines our family of components. A/G contracts are re-defined accordingly: Definition 5: A contract is a tuple C = (Σ in , Σ out , A, G), where Σ in and Σ out are the input and output alphabets and A and G are assertions over Σ, called the assumptions and the guarantees. The set E C of the legal environments for C are all free of exception components E such that

Σ in E = Σ out C , Σ out E = Σ in C , and P E ⊆ A. The set M C of all components implementing C is defined by: M is free of exception, Σ in M = Σ in C and Σ out M = Σ out C
and P E×M ⊆ G for every environment E of C. Focus now on the issue of consistency and compatibility, for contracts. The following holds:

Property 7: Let C = (Σ in , Σ out , A, G) be a contract satisfying the following conditions:

pr Σ in C (G) = Σ in M → (D * ∪D ω ) ( 15
)
pr Σ out C (A) = Σ out M → (D * ∪D ω ) (16) fail does not occur in G ∧ A (17)
Then, C is consistent and compatible. Proof: By condition [START_REF] Balarin | Constraints specification at higher levels of abstraction[END_REF], the component M = (Σ in , Σ out , G) satisfies condition 4 of Definition 4. It may not satisfy condition 2, however. To achieve this we must modify, in M , the behaviors not belonging to A to avoid fail to occur. Preserving M on A will ensure that implementation of C is preserved.

To get M , replace any behavior σ ∈ G ∧ ¬A by a behavior σ such that pr Σ in C (σ ) = pr Σ in C (σ) and pr Σ out C (σ ) fail . Component M obtained in this way is free of exception and implements C, showing that C is consistent. Consider next the component E = (Σ out , Σ in , A). If E is free of exception, then it is an environment for C. If this is not the case, then we can modify E on A ∧ ¬G as we did for obtaining M . This yields an environment E for C, showing that C is compatible. 2

Conditions ( 15) and ( 16) express that assumptions and guarantees are both input enabled. Condition ( 17) is the key one. Observe that, now, contract C 1 of Section IV-A1 is inconsistent since it has no implementation-implementations must be free of exception. In turn, contract C 1 is consistent. This is in contrast to the theory of Section VII-A, where both contracts were considered consistent (crashes were not ruled out). Indeed, contract C 1 of Section IV-A1 satisfies the conditions of Property 7, whereas C 1 does not. Addressing exceptions matters.

C. Dealing with variable alphabets

Since contracts aim at capturing incomplete designs, we cannot restrict ourselves to a fixed alphabet-it is not known in advance what the actual alphabet of the complete design will be. Thus the simple variants of Sections VII-A and VII-B have no practical relevance and we must extend them to dealing with variable alphabets. In particular, components will now be pairs M = (Σ M , P M ), where Σ M is the alphabet of M and P M is an assertion over Σ M . Similarly, contracts are triples C = (Σ C , A C , G C ), where assumptions A C and guarantees G C are assertions over alphabet Σ C .

Key to dealing with variable alphabet this is the operation of alphabet equalization that we introduce next. For P an assertion over alphabet Σ and Σ ⊆ Σ, we consider its projection pr Σ (P ) over Σ , which is simply the set of all restrictions, to Σ , of all behaviors belonging to P . We will also need the inverse projection pr -1 Σ (P ), for Σ ⊇ Σ, which is the set of all behaviors over Σ projecting, to Σ, as behaviors of P . For (Σ i , P i ), i = 1, 2, we call alphabet equalization of (Σ 1 , P 1 ) and (Σ 2 , P 2 ) the two assertions (Σ, pr -1

Σ (P i )), i = 1, 2 where Σ = Σ 1 ∪ Σ 2 .
We also need to define alphabet equalization when the alphabet Σ decomposes as Σ = Σ in Σ out . Equalizing the above decomposition to a larger alphabet Σ ⊇ Σ yields Σ out = Σ out , whence Σ in = Σ \ Σ out follows.

Alphabet equalization serves as a preparation step to reuse the framework of Section VII-A when alphabets are variable.

This being defined, all operations and relations introduced in Section VII-A are extended to the case of variable alphabets by 1) applying alphabet equalization to the involved assertions, and, 2) reusing the operation or relation as introduced in Section VII-A.

As pointed out in [START_REF] Benveniste | Multiple viewpoint contract-based specification and design[END_REF], this generalization yields a contract theory that is a valid instantiation of the meta-theory (up to the missing quotient). It is not satisfactory from the practical standpoint, however. The reason is that the conjunction of two contracts with disjoint alphabets yields a trivial assumption T, which is very demanding-any environment must be accommodated-and does not reflect the intuition (more on this will be discussed in Section VIII-D.

To summarize, Sections VII-A, VII-B, and VII-C, together define a framework for asynchronous Assume/Guarantee contracts where components are of Kahn Process Network type.

D. Synchronous A/G contracts

We obtain variants of this framework of Assume/Guarantee contracts by changing the concrete definition of what an assertion is, and possibly revisiting what the component composition is. We can redefine assertions as

P ⊆ (Σ → D) * ∪ (Σ → D) ω . ( 18
)
Compare ( 18) with [START_REF] Alur | Alternating refinement relations[END_REF]. In both cases, assertions are sets of behaviors. With reference to [START_REF] Alur | Alternating refinement relations[END_REF], behaviors were tuples of finite or infinite flows, one for each symbol of the alphabet. In contrast, in [START_REF] Balarin | Specification, synthesis and simulation of transactor processes[END_REF], behaviors are finite or infinite sequences of reactions, which are the assignment of a value to each symbol of the alphabet. By having a distinguished symbol ⊥ ∈ D to model the absence of an actual data, we get the multiple-clocked synchronous model used by synchronous languages [START_REF] Benveniste | The Synchronous Languages 12 years later[END_REF]. Definition [START_REF] Balarin | Specification, synthesis and simulation of transactor processes[END_REF] for assertions correspond to the synchronous model of computation, whereas [START_REF] Alur | Alternating refinement relations[END_REF] corresponds to the Kahn Process Network type of model [START_REF] Kahn | The Semantics of Simple Language for Parallel Programming[END_REF], [START_REF] Walid | Advances in the dataflow computational model[END_REF]. The material of Sections VII-A, VII-B, and VII-C, can be adapted to this new model of component composition, thus yielding a framework of synchronous Assume/Guarantee contracts.

E. Observers

The construction of observers for this case is immediate. We develop it for the most interesting case in which exceptions are handled, see Sections VII-A and VII-B. Let P be an assertion according to [START_REF] Alur | Alternating refinement relations[END_REF]. P defines a verdict b P by setting b P (σ) = T if and only if σ ∈ P

Observers must return their verdict in some finite amount of time. Hence, on-line interpretation based on Definition 3 is appropriate. With this interpretation, for C = (Σ in , Σ out , A, G) a contract, its associated observer is obtained as follows, with reference to Definition 2:

• b E C (E) is performed by drawing non-deterministically a behavior σ of E and then evaluating b A (σ). Lemma 3 for generic observers specializes to the following, effective, semi-decision procedure:

Lemma 4:

1) If b A outputs F, then C is incompatible; 2) If b A ⇒ b G outputs F, then C is inconsistent.

F. Discussion

Assume/Guarantee contracts are a family of instantiations of our meta-theory. This family is flexible in that it can accommodate different models of communication and different models of exceptions. Assume/Guarantee contracts are an adequate framework for use in requirements capture. Indeed, requirements are naturally seen as assertions. When categorizing requirements into assumptions (specifying the context of use of the system under development) and guarantees (that the system offers), formalizing the resulting set of requirements as an A/G contract seems very natural.

Regarding exceptions, the special value fail that we introduced to capture exceptions is not something that is given in practice. Value fail may subsume various run time errors. Alternatively, for the synchronous Assume/Guarantee contracts, fail can capture the failure of a component to be input enabled (able, in each reaction, to accept any tuple of inputs).

In its present form, the framework of Assume/Guarantee contracts (synchronous or asynchronous), suffers from the need to manipulate negations of assertions, an operation that is generally not effective, except if the framework is restricted to finite state automata and finite alphabets of actions. For general frameworks, using observers or abstract interpretation can mitigate this in part.

G. Bibliographical note

By explicitly relying on the notions of Assumptions and Guarantees, A/G-contracts are intuitive, which makes them appealing for the engineer. In A/G-contracts, Assumptions and Guarantees are just properties. The typical case is when these properties are languages or sets of traces, which includes the class of safety properties [START_REF] Lamport | Proving the correctness of multiprocess programs[END_REF], [START_REF] Chang | Characterization of temporal property classes[END_REF], [START_REF] Manna | Temporal verification of reactive systems: Safety[END_REF], [START_REF] Baier | Principles of Model Checking[END_REF], [START_REF] Clarke | Model Checking[END_REF]. A/Gcontracts were advocated by the SPEEDS project [START_REF] Benveniste | Multiple viewpoint contract-based specification and design[END_REF]. They were further experimented in the framework of the CESAR project [START_REF] Damm | Using Contract-Based Component Specifications for Virtual Integration and Architecture Design[END_REF], with the additional consideration of weak and strong assumptions. The theory developed in [START_REF] Benveniste | Multiple viewpoint contract-based specification and design[END_REF] turns out to be closest to this presentation; still, exceptions were not handled in [START_REF] Benveniste | Multiple viewpoint contract-based specification and design[END_REF]. The presentation developed in this paper clarifies the design choices in A/G-contract theories.

Inspired by [START_REF] Kim Guldstrand Larsen | Interface Input/Output Automata[END_REF], another form for A/G-contract was proposed by [START_REF] Graf | Contracts for BIP: Hierarchical Interaction Models for Compositional Verification[END_REF], [START_REF] Ben Hafaiedh | Reasoning about Safety and Progress Using Contracts[END_REF] when designs are expressed using the BIP programming language [START_REF] Bliudze | The Algebra of Connectors -Structuring Interaction in BIP[END_REF], [START_REF] Sifakis | Component-Based Construction of Heterogeneous Real-Time Systems in Bip[END_REF]. To achieve separate development of components, and to overcome the problems that certain models have with the effective computation of the operators, the authors avoid using parallel composition ⊗ of contracts. Instead, they replace it with the concept of circular reasoning, which states as follows in its simplest form: if design M satisfies property G under assumption A and if design N satisfies assumption A, then M × N satisfies G. When circular reasoning is sound, it is possible to check relations between composite contracts based on their components only, without taking expensive compositions. In order for circular reasoning to hold, the authors devise restricted notions of refinement under context and show how to implement the relations in the contract theory for the BIP RR n°8147 framework. Compatibility is not addressed and this proposal does not consider conjunction.

Regarding extensions, a notion of contract for real-time interfaces is proposed in [START_REF] Bhaduri | A proposal for real-time interfaces in speeds[END_REF]. Sets of tasks are associated to components which are individually schedulable on a processor. An interface for a component is an ω-language containing all legal schedules. Schedulability of a set of components on a single processor then corresponds to checking the emptiness of their intersection. The interface language considered is expressive enough to specify a variety of requirements like periodicity, the absence or the presence of a jitter, etc. An assume/guarantee contract theory for interfaces is then developed where both assumptions and guarantees talk about bounds on the frequency of task arrivals and time to completions. Dependencies between tasks can also be captured. Refinement and parallel product of contracts are then defined exactly as in the SPEEDS generic approach.

In [START_REF] Nuzzo | Methodology for the design of analog integrated interfaces using contracts[END_REF], a platform-based design methodology that uses A/G analog contracts is proposed to develop reliable abstractions and design-independent interfaces for analog and mixed-signal integrated circuit design. Horizontal and vertical contracts are formulated to produce implementations by composition and refinement that are correct by construction. The effectiveness of the methodology is demonstrated on the design of an ultra-wide band receiver used in an intelligent tire system, an on-vehicle wireless sensor network for active safety applications.

A/G-contracts have been extended to a stochastic setting by Delahaye et al. [START_REF] Delahaye | Modular Specification and Compositional Analysis of Stochastic Systems[END_REF], [START_REF] Delahaye | Probabilistic Contracts : A Compositional Reasoning Methodology for the Design of Stochastic Systems[END_REF], [START_REF] Delahaye | Probabilistic contracts : A compositional reasoning methodology for the design of systems with stochastic and/or non-deterministic aspects[END_REF]. In this work, the implementation relation becomes quantitative. More precisely, implementation is measured in two ways: reliability and availability. Availability is a measure of the time during which a system satisfies a given property, for all possible runs of the system. In contrast, reliability is a measure of the set of runs of a system that satisfy a given property. Following the lines of the contract theories presented earlier, satisfaction is assumption-dependent in the sense that runs that do not satisfy the assumptions are considered to be "correct"; the theory supports refinement, structural composition and logical conjunction of contracts; and compositional reasoning methods have been proposed, where the stochastic or non-stochastic satisfaction levels can be budgeted across the architecture: For instance, assume that implementation M i satisfies contract C i with probability α i , for i = 1, 2, then the composition of the two implementations M 1 ×M 2 satisfies the composition of the two contracts C 1 ⊗C 2 with probability at least α 1 + α 2 -1.

Features of our presentation: This presentation of A/Gcontracts is new in may respects. For the first time, it is cast into the meta-theory of contracts, with the advantage of clarifying the definition of refinement and parallel composition of contracts-this involved some hand waving in the original work [START_REF] Benveniste | Multiple viewpoint contract-based specification and design[END_REF]. Also, this allowed us to handle exceptions properly.

VIII. PANORAMA: INTERFACE THEORIES

Interface theories are an interesting alternative to Assume/Guarantee contracts. They aim at providing a merged specification of the implementations and environments associated to a contract via the description of a single entity, called an interface. We review some typical instances of interface theories, with emphasis on interface automata and modal interfaces. Interface theories generally use (a mild variation of) Lynch Input/Output Automata [START_REF] Lynch | A proof of the kahn principle for input/output automata[END_REF], [START_REF] Lynch | Input/output automata: Basic, timed, hybrid, probabilistic, dynamic[END_REF] as their framework for components and environments. As a prerequisite, we thus recall the background on Input/Output Automata, i/o-automata for short.

A. Components as i/o-automata

An i/o-automaton is a tuple M = (Σ in , Σ out , Q, q 0 , →), where

• Σ in and Σ out are disjoint finite input and output alphabets; set Σ = Σ in ∪ Σ out ; • Q is a finite set of states and q 0 ∈Q is the initial state;

• → ⊆ Q × Σ × Q is the transition relation; as usual, we write q α -→ q to mean (q, α, q ) ∈ → and q α -→ to indicate the existence of a q such that q α -→ q . By concatenation, transition relation → extends to a relation → * on Q × Σ * × Q, where Σ * is the set of all finite words over Σ. Say that a state q is reachable from q if there exists some word m such that q m -→ * q . To considerably simplify the development of the theory, we restrict ourselves to deterministic i/o-automata, i.e., such that:

q α -→ q 1 and q α -→ q 2 implies q 2 = q 1 . ( 20
)
Two i/o-automata M 1 and M 2 having identical alphabet Σ are composable if the usual input/output matching condition holds:

Σ out 1 ∩ Σ out 2 = ∅ and their composition M = M 1 × M 2 is given by Σ in = Σ in 1 ∩ Σ in 2 Σ out = Σ out 1 ∪ Σ out 2 Q = Q 1 × Q 2 and q 0 = (q 1,0 , q 2,0 ),
and the transition relation → is given by

(q 1 , q 2 ) α -→ (q 1 , q 2 ) iff q i α -→ i q i , i = 1, 2
An i/o-automaton is said closed whenever Σ in = ∅ and open otherwise. For M i , i = 1, 2 two i/o-automata and two states q i ∈ Q i , say that q 1 simulates q 2 , written q 2 ≤q 1 if

∀α, q 2 such that q 2 α -→ 2 q 2 ⇒ q 1 α -→ 1 q 1 and q 2 ≤q 1 (21)
Say that

M 1 simulates M 2 , written M 2 ≤M 1 , if q 2,0 ≤q 1,0 . (22)
Observe that simulation relation [START_REF] Balasubramanian | Developing applications using model-driven design environments[END_REF][START_REF] Bauer | Moving from specifications to contracts in component-based design[END_REF] does not distinguish inputs from outputs neither it distinguishes the component from its environment. It is the classical simulation relation meant for closed systems. Due to condition (20) of determinism, simulation coincides with language inclusion. Variable alphabet is again dealt with using the mechanism of alphabet equalization. For M = (Σ in , Σ out , Q, q 0 , →) an i/o-automaton and Σ ⊃ Σ, we define

M ↑Σ = Σ in ∪ (Σ \ Σ), Σ out , Q, q 0 , → RR n°8147
where → is obtained by adding, to →, for each state and each added action, a self-loop at this state labeled with this action.

Components-and consequently environments-for use in interface theories will be receptive i/o-automata (also termed input enabled), i.e., they should react by proper response to any input stimulus in any state:41

M is receptive iff ∀q ∈ Q, ∀α ∈ Σ in : q α -→ (23)
Receptiveness is stable under parallel composition.

B. Interface Automata with fixed alphabet

For reasons that will become clear later, we restrict the presentation of interface automata to the case of a fixed alphabet Σ. We begin with the definition of Interface Automata which are possibly non-receptive i/o-automata. Moreover we give their interpretation as contracts according to the metatheory.

Definition 6: An Interface Automaton is a tuple C = (Σ in , Σ out , Q, q 0 , →) where Σ in , Σ out , Q, → are as in i/o-automata.

The initial state q 0 , however, may not satisfy q 0 ∈Q. If q 0 ∈Q holds, Interface Automaton C defines a contract by fixing a pair (E C , M C ) as follows:

• The set E C of the legal environments for C collects all components E such that: 1) Σ in E = Σ out and Σ out E = Σ in . Thus, E and C, seen as i/o-automata, are composable and E × C is closed; 2) For any output action α ∈ Σ in of environment E such that q E α -→ E and any reachable state (q E , q) of E × C, then (q E , q) α -→ E×C holds. There exists a unique maximal environment E C ∈ E C , in that E C × C simulates E × C in the sense of [START_REF] Bauer | Moving from specifications to contracts in component-based design[END_REF] for any

E ∈ E C ; E C = (Σ out , Σ in , Q ∪ { }, q 0 , → E C ), where: (a) the restriction, to Q × Σ × Q, of transition relation → E C , coincides with → ; (b) ∀q ∈ Q: q α -→ E C holds if and only if ¬[q α -→ ] and α ∈ Σ out ; (c) α -→ E C
holds for any α ∈ Σ.

• The set M C of the implementations of C collects all components M such that i/o-automaton C simulates E C ×M in the sense of ( 22).

Condition 2) means that environment E is only willing to emit an output if it is accepted as an input by C in the composition E × C. Regarding the existence and uniqueness of E C , observe first that conditions (a) and (b) together imply that E C is receptive. Also, by (a) and (b), E C × C is strictly identical with (∅, Σ, Q, q 0 , →), i.e., it is obtained from C, seen as an i/o-automaton, by simply turning inputs to outputs. Consequently, Condition 2) holds and, thus, E C ∈ E C . By (b) and (c), E C is maximal. The above definition of Interface Automata is heterodox, compare with the original references [START_REF] De Alfaro | Interface automata[END_REF], [START_REF] Luca | Interface-based design[END_REF]. Definition 6 introduces the two sets E C and M C , whereas no notion of implementation or environment is formally associated to an Interface Automaton in the original definition. Also, the handling of the initial state is unusual. Failure of q 0 ∈Q to hold typically arises when the set of states Q is empty. Our Definition 6 allows to cast Interface Automata in the framework of the meta-theory of Table IV.

Corresponding relations and operations must be instantiated and we do this next. As a first, immediate, result:

Lemma 5: q 0 ∈ Q is the necessary and sufficient condition for C to be both consistent and compatible in the sense of the meta-theory, i.e., E C = ∅ and M C = ∅.

Refinement and conjunction: Contract refinement as defined in Table IV is equivalent to alternate simulation [START_REF] Alur | Alternating refinement relations[END_REF], defined as follows: for C i , i = 1, 2 two contracts, say that two respective states q i , i = 1, 2 are in alternate simulation, written

q 2 q 1 , if ∀α ∈ Σ out 2 , q 2 s.t. q 2 α -→ 2 q 2 ⇒      α ∈ Σ out 1 q 1 α -→ 1 q 1 q 2 q 1 ∀α ∈ Σ in 1 , q 1 s.t. q 1 α -→ 1 q 1 ⇒      α ∈ Σ in 2 q 2 α -→ 2 q 2 q 2 q 1 (24)
Say that C 2 refines C 1 , written C 2 C 1 , if q 2,0 q 1,0 . The first condition of (24) reflects the inclusion M C 2 ⊆ M C 1 , whereas the second condition of (24) reflects the opposite inclusion E C 2 ⊇ E C 1 . Alternate simulation can be effectively checked, see [START_REF] De | Game Models for Open Systems[END_REF] for issues of computational complexity. Unfortunately, no simple formula for the conjunction of contracts is known. See [START_REF] Doyen | Interface theories with component reuse[END_REF] for the best results in this direction.

Parallel composition and quotient: Contract composition C 2 ⊗C 1 , as defined in the meta-theory, is effectively computed as follows, for C i two Interface Automata satisfying the conditions of Lemma 5. Consider, as a first candidate for contract composition, the composition C 2 ×C 1 where C i , i = 1, 2 are seen as i/o-automata. This first guess does not work because of the condition involving environments in the contract composition of the meta-theory. More precisely, by the meta-theory we should have

E |= E C ⇒ [E×M 2 |= E C 1 and E×M 1 |= E C 2 ] which requires ∀α ∈ Σ out i : q i α -→ i ⇒ (q 1 , q 2 )
α -→ C2×C1 . Pairs (q 1 , q 2 ) not satisfying this are called illegal. In words, a pair of states (q 1 , q 2 ) is illegal when one Interface Automaton wants to submit an output whereas the other one refuses to accept it-referring to Assume/Guarantee contracts, one could interpret this as a mismatch of assumptions and guarantees in this pair of interfaces. Illegal pairs must then be pruned away. Pruning away illegal pairs from C 2 ×C 1 together with corresponding incoming transitions may cause other illegal pairs to occur. The latter must also be pruned away, until fixpoint occurs. The result is the contract composition C 2 ⊗C 1 .

As a result of this pruning, it may be the case that the resulting contract has empty set of states, which, by Lemma 5, expresses that the resulting composition of the two interfaces is inconsistent and incompatible-in the original literature on Interface Automata [START_REF] De Alfaro | Interface automata[END_REF], [START_REF] Luca | Interface-based design[END_REF] it is said that the two interfaces C 1 and C 2 are incompatible.

In [START_REF] Bhaduri | Interface synthesis and protocol conversion[END_REF], incremental design of deterministic Interface Automata is studied. Let C ↓ be the interface C with input and output actions interchanged. Given two Interface Automata C 1 and C 2 , the greatest interface compatible with C 2 such that their composition refines C 1 is given by (C 2 C 1 ↓ ) ↓ . Hence, the part regarding quotient in the meta-theory is correctly addressed for deterministic Interface Automata.

Dealing with variable alphabets: So far we have presented the framework of interface automata for the case of a fixed alphabet. The clever reader may expect that dealing with variable alphabets can be achieved by using the mechanism of alphabet equalization via inverse projections. 42 This is a correct guess for contract composition. It is however not clear if it is also adapted for conjunction for which no satisfactory construction exists as previously indicated.

In contrast, alphabet equalization and conjunction are elegantly addressed by the alternative framework of Modal Interfaces we develop now.

C. Modal Interfaces with fixed alphabet

Modal Interfaces inherit from both the Interface Automata and the originally unrelated notion of Modal Automaton (or Modal Transition System), see the bibliographical note VIII-G. As Interface Automata, Modal Interfaces use receptive i/o-automata as their components and environments. The presentation of Modal Interfaces we develop here is aligned with our meta-theory and, thus, differs from classical presentations. Again, we begin with the case of a fixed alphabet Σ.

Definition 7: We call Modal Interface a tuple of the form C = (Σ in , Σ out , Q, q 0 , →,

), where Σ in , Σ out , Q, q 0 are as in Interface Automata and →, ⊆ Q × Σ × Q are two transition relations, called must and may, respectively.

A Modal Interface C such that q 0 ∈Q induces two (possibly non receptive) i/o-automata and C must = (Σ in , Σ out , Q, q 0 , →) and C may = (Σ in , Σ out , Q, q 0 , ).

A Modal Interface is deterministic if C may is deterministic in the sense of 20. C defines a contract by fixing a pair (E C , M C ) as follows:

The set E C of the legal environments for C collects all components E such that:

1) Σ in E = Σ out and Σ out E = Σ in ; consequently, E and C must , seen as i/o-automata, are composable and E × C must is closed; the same holds with C may in lieu of C must ; 42 The inverse projection of an i/o-automaton is simply achieved by adding, in each state, a self-loop for each missing symbol.

2) For any α ∈ Σ in such that q E α -→ E and any reachable state (q E , q) of E × C may : (q E , q) α -→ E×C must .

There exists a unique maximal environment E C ∈ E C , in that E C × C may simulates E × C may in the sense of [START_REF] Bauer | Moving from specifications to contracts in component-based design[END_REF] for any

E ∈ E C ; E C = (Σ out , Σ in , Q ∪ { }, q 0 , → E C )
, where:

(a) the restriction, to Q×Σ in ×Q, of transition relation → E C , coincides with → ; the restriction, to

Q × Σ out × Q, of transition relation → E C , coincides with ; (b) for any q ∈ Q, q α -→ E C holds if and only if ¬[q α ] and α ∈ Σ out ; (c) α -→ E C
holds for any α ∈ Σ.

The set M C of the implementations of C collects all components M such that:

3) E C ×C may simulates E C ×M in the sense of ( 22); [only may transitions are allowed for E C ×M ;] 4) for any reachable state (q E , q M ) of E C ×M and (q E , q) of E C ×C may such that (q E , q M )≤(q E , q), and any ac-

tion α ∈ Σ out M such that q α → , then (q E , q M ) α -→ E C ×M [must transitions are mandatory in E C ×M .]
The first paragraph is a verbatim of the original definition of Modal Interfaces [START_REF] Raclet | A modal interface theory for component-based design[END_REF]. Definition 7 introduces the two sets E C and M C , whereas the classical theory of Modal Interfaces considers and develops a different notion of model (often also called "implementation", which is unfortunate). As for Interface Automata in Section VIII-B, the handling of initial state q 0 is heterodox. Our Definition 7 allows to cast Modal Interfaces in the framework of the meta-theory.

To justify the existence and uniqueness of E C , observe first that conditions (a) and (b) together imply that E C is receptive. Condition (2) follows from (a). Maximality in the sense of [START_REF] Bauer | Moving from specifications to contracts in component-based design[END_REF] follows from (b) and (c).

Consistency and Compatibility:

We begin with consistency. Say that state q ∈ Q of C is consistent if q α → implies q α , otherwise we say that it is inconsistent. Assume that C has some inconsistent state q ∈ Q, meaning that, for some action α, q α → holds but q α does not hold. By conditions 3) and 4) of Definition 7, for any environment E and any implementation M of C, no state (q E , q M ) of E×M satisfies (q E , q M )≤q. Hence, all may transitions leading to q can be deleted from C without changing M C . Performing this makes state q unreachable in C may , thus Condition 2 of Definition 7 is relaxed and the set of environments is possibly augmented. Since we have removed may transitions, some more states have possibly become inconsistent. So, we must repeat the same procedure. Since the number of states is finite, this procedure eventually reaches a fixpoint. At fixpoint, the set Q of states partition as Q = Q con Q incon , where Q incon collects all states that were or became inconsistent as a result of this procedure, and Q con only collects consistent states. In addition, since the fixpoint has been reached, Q incon is unreachable from Q con . As a final step, we delete Q incon and call [C] the so obtained contract. The following result holds:

Lemma 6: RR n°8147 1) Modal Interface [C] satisfies M [C] = M C and E [C] ⊇ E C (25)
where the inclusion is strict unless C possesses no inconsistent state. 2) [C] offers the smallest set of environments among the Modal Interfaces satisfying [START_REF] Benes | Checking Thorough Refinement on Modal Transition Systems Is EXPTIME-Complete[END_REF]. 3) C is consistent and compatible if and only if Q con q 0 . In the sequel, unless otherwise specified, we will only consider Modal Interfaces that are consistent and compatible.

Refinement and conjunction: Conjunction and refinement are instantiated in a very elegant way in the theory of Modal Interfaces. Contract refinement in the sense of the meta-theory is instantiated by the effective notion of Modal refinement we introduce now. Roughly speaking, modal refinement consists in enlarging the must relation (thus enlarging the set of legal environments) and restricting the may relation (thus restricting the set of implementations). The formalization requires the use of simulation relations.

For C a Modal Interface and q∈Q a state of it, introduce the following may and must sets:

may(q) = {α ∈ Σ | q α } must(q) = {α ∈ Σ | q α → }
Definition 8 (modal refinement): Let C i , i = 1, 2 be two Modal Interfaces and let q i be a state of C i , for i = 1, 2. Say that q 2 refines q 1 , written q 2 q 1 , if: may 2 (q 2 ) ⊆ may 1 (q 1 ) must 2 (q 2 ) ⊇ must 1 (q 1 ) and ∀α ∈ Σ :

q 1 α 1 q 1 q 2 α 2 q 2 =⇒ q 2 q 1 Say that C 2 C 1 if q 2,0 q 1,0 .
The following result relates modal refinement with contract refinement as defined in the meta-theory. It justifies the consideration of modal refinement. Its proof follows by direct use of Definition 7 and Lemma 6: Lemma 7: For C 1 and C 2 two Modal Interfaces, the following two properties are equivalent:

(i) M C 2 ⊆ M C 1 and E C 2 ⊇ E C 1 , meaning that contract C 2 refines contract C 1 following the meta-theory; (ii) [C 2 ] [C 1 ], i.e., [C 2 ] refines contract [C 1 ]
in the sense of modal refinement. The conjunction of two Modal Interfaces is thus the Greatest Lower Bound (GLB) with respect to refinement order. Its computation proceeds in two steps. In a first step, we wildly enforce the GLB and compute a pre-conjunction by taking union of must sets and intersection of may sets: Definition 9: The pre-conjunction 43

and is given by

Σ in = Σ in 1 , Σ out = Σ out 1 , Q = Q 1 ×Q 2 , q 0 = (q 1,
0 , q 2,0 ), and its two transition relations are given by: must(q 1 , q 2 ) = must 1 (q 1 ) ∪ must 2 (q 2 ) may(q 1 , q 2 ) = may 1 (q 1 ) ∩ may 2 (q 2 ) (

Due to [START_REF] Benes | On determinism in modal transition systems[END_REF], C 1 ∧C 2 may involve inconsistent states and, thus, in a second step, the pruning introduced in Lemma 6 must be applied:

C 1 ∧ C 2 = [C 1 ∧C 2 ] (27)
Say that the two Modal Interfaces C 1 and C 2 are consistent 44if C 1 ∧ C 2 is consistent in the sense of Lemma 6.

Parallel composition and quotient: For Modal Interfaces, we are able to define both parallel composition and quotient in the sense of the meta-theory. As it was the case for Interface Automata, parallel composition for Modal Interfaces raises compatibility issues and, thus, a two-step procedure is again followed for its computation.

Definition 10: The pre-composition

C 1 ⊗C 2 of two Modal Interfaces is only defined if Σ out 1 ∩ Σ out 2
= ∅ and is given by:

Σ out = Σ out 1 ∪ Σ out 2 , Q = Q 1 ×Q 2 , q 0 = (q 1,
0 , q 2,0 ), and its two transition relations are given by: must(q 1 , q 2 ) = must 1 (q 1 ) ∩ must 2 (q 2 ) may(q 1 , q 2 ) = may 1 (q 1 ) ∩ may 2 (q 2 ) (

Say that a state (q 1 , q 2 ) of C 1 ⊗C 2 is illegal if

may 1 (q 1 ) ∩ Σ in 2 ⊆ must 2 (q 2 ) or may 2 (q 2 ) ∩ Σ in 1 ⊆ must 1 (q 1 )
Illegal states are pruned away from C 1 ⊗C 2 as follows. Remove, from C may 1 × C may 2 , all transitions leading to (q 1 , q 2 ). As performing this may create new illegal states, the same is repeated until fixpoint is reached. As a final step we delete the states that are not may-reachable. This finally yields C 1 ⊗C 2 , which no more possesses illegal states.

The above construction is justified by the following result:

Lemma 8: C 1 ⊗C 2 as defined in Definition 10 instantiates the contract composition from the meta-theory. Proof: (sketch) E is an environment for C iff for any reachable state

(q E , q 1 , q 2 ) of E × C may 1 × C may 2 , we have rs(q E ) ⊆ must 1 (q 1 ) ∩ must 2 (q 2 ), (29)
where rs(q), the ready set of state q, is the subset of actions α such that q α -→ holds. Let M 1 be any implementation of C 1 and consider E×M 1 . We need to prove that E×M 1 is an environment for C 2 , i.e., satisfies Condition 2 of Definition 7 (we must also prove the symmetric property). Let (q E , q 1 , q 2 ) be a reachable state of E×M 1 ×C may 2 . We must prove

rs(q E ) ∩ rs M1 (q 1 ) ∩ Σ in 2 ⊆ must 2 (q 2 )
By ( 29) it suffices that the following property holds:

rs M1 (q 1 ) ∩ Σ in 2 ⊆ must 2 (q 2 ) (30)
However, we only know that rs M1 (q 1 ) ⊆ may 1 (q 1 ). Hence, to guarantee [START_REF] Benveniste | The Synchronous Languages 12 years later[END_REF] we must prune away illegal pairs of states.

To this end, we use the same procedure as before: we make state (q 1 , q 2 ) unreachable in C may 1 ×C may 2 by removing all may transitions leading to that state. We complete the reasoning as we did for the study of consistency.

2

Definition 11: The quotient C 1 /C 2 of two modal interfaces C 1 and C 2 is only defined if Σ in 1 ∩ Σ out 2 =
∅ and is defined according to the following two steps procedure. First, define C as follows:

Σ out = Σ out 1 \ Σ out 2 , Q = Q 1 × Q 2 , q 0 = (q 1,
0 , q 2,0 ), and its two transition relations are given by:

must(q 1 , q 2 ) = must 1 (q 1 ) may(q 1 , q 2 ) = ¬ [may 1 (q 1 ) ∩ ¬must 1 (q 1 )] ∪ ¬ [must 1 (q 1 ) ∩ must 2 (q 2 )] ∪ ¬ [may 1 (q 1 ) ∪ may 2 (q 2 )]
These formulas may give raise to inconsistent states, and, thus, in a second step, we set

C 1 /C 2 = [C].
This definition is justified by the following result [START_REF] Raclet | A modal interface theory for component-based design[END_REF], showing that Definition 11 instantiates the meta-theory:

Lemma 9: C 1 ⊗ C 2 C if and only if C 2 C/C 1 .
Now, it may be that (C 1 /C 2 )⊗C 2 possess illegal pairs of states (Definition 10), whence the following improvement, where Σ out and Σ in are as in Definition 11 and may / and must / refer to the quotient C 1 /C 2 : Definition 12: Let C be the interface defined on the same state structure as C 1 /C 2 , with however the following modalities: may (q 1 , q 2 ) = may / (q 1 , q 2 ) ∩ may 2 (q 2 ) ∪ Σ in must (q 1 , q 2 ) = must / (q 1 , q 2 ) ∪ (Σ out 1 ∩ Σ out 2 ∩ may 2 (q 2 )) define the compatible quotient, written C 1 / /C 2 , to be the reduction of

C : C 1 / /C 2 = [C ] .
This construction is justified by the following result: Lemma 10: The compatible quotient C 1 / /C 2 solves the following problem:

max    C C has no inconsistent state C ⊗ C 2 has no illegal pair of states C ⊗ C 2 C 1    Proof: Denote C = C 1 / /C 2
the compatible quotient defined above. The proof is threefold: (i) C is proved to be a solution of the inequality C ⊗C 2 C 1 , (ii) C is proved to be compatible with C 2 , and (iii) every C satisfying the two conditions above is proved to be a refinement of C.

Remark that reachable states in (C 1 / /C 2 )⊗C 2 are of the form (q 1 , q 2 , q 2 ) and that for every reachable state pair (q 1 , q 2 ) in

C 1 / /C 2 , state (q 1 , q 2 , q 2 ) is reachable in (C 1 / /C 2 ) ⊗ C 2 .
(i) Remark that may ⊆ may / and must ⊇ must / . Hence,

C 1 / /C 2 C 1 /C 2 . Since the parallel composition is monotonic, (C 1 / /C 2 ) ⊗ C 2 (C 1 /C 2 ) ⊗ C 2 C 1 .
(ii) For every state (q 1 , q 2 , q 2 ), reachable in (C 1 / /C 2 ) ⊗ C 2 , one among the following three cases occurs:

• Assume e ∈ Σ in 1 , meaning that e is an input for both C 2 and C 1 / /C 2 . Hence state (q 1 , q 2 , q 2 ) is not illegal because of e.

• Assume e ∈ Σ out 1 ∩ Σ out 2 , Therefore e is an input of the compatible quotient. Remark must (q 1 , q 2 ) ⊆ may 2 (q 2 ). Hence, state (q 1 , q 2 , q 2 ) is not illegal because of e • Assume e ∈ Σ out 1 ∩Σ in 2 , meaning that e is an output of the compatible quotient. Remark may (q 1 , q 2 ) ⊆ must 2 (q 2 ). Therefore state (q 1 , q 2 , q 2 ) is not illegal because of e.

(iii) Let C be a modal interface such that C 1 / /C 2 C C 1 /C 2 . We shall prove that either C C 1 / /C 2 or that C is not compatible with C 2 . Remark that every reachable state (q 1 , q 2 ) of C 1 / /C 2 is related to exactly one state q of C by the two modal refinement relations. Assume that C is not a refinement of C 1 / /C 2 , meaning that there exists related states (q 1 , q 2 ) and q such that may (q 1 , q 2 ) ⊆ may (q ) ⊆ may / (q 1 , q 2 ) and must (q 1 , q 2 ) ⊇ must (q ) ⊇ must / (q 1 , q 2 ) and either may (q 1 , q 2 ) may (q ) or must (q 1 , q 2 ) must (q ). Remark e ∈ Σ in 1 implies that e ∈ may (q 1 , q 2 ) iff e ∈ may / (q 1 , q 2 ) and that e ∈ must (q 1 , q 2 ) iff e ∈ must / (q 1 , q 2 ). Therefore the case e ∈ Σ in 1 does not have to be considered.

1) Assume there exists e such that e ∈ may (q ) \ may (q 1 , q 2 ). Remark this implies e ∈ Σ out 1 ∩ Σ in 2 , meaning that e is an output of the compatible quotient. Remark also that e ∈ must 2 (q 2 ). Therefore state (q , q 2 ) is illegal in C ⊗ C 2 .

2) Assume there exists e such that e ∈ must (q 1 , q 2 ) \ must (q ). Remark this implies e ∈ Σ out 1 ∩ Σ out 2 , meaning that e is an input of the compatible quotient. Remark also that e ∈ may 2 (q 2 ). Therefore state (q , q 2 ) is illegal in C ⊗ C 2 .

D. Modal Interfaces with variable alphabet

As a general principle, every relation or operator introduced in Section VIII-C (for Modal Interfaces with a fixed alphabet Σ) is extended to the case of variable alphabets by 1) extending and equalizing alphabets, and then 2) applying the relations or operators of Section VIII-C to the resulting Modal Interfaces. For all frameworks we studied so far, alphabet extension was performed using inverse projections, see Section VII-C. For instance, this is the procedure used in defining the composition of i/o-automata: extending alphabets in i/o-automata is by adding, at each state and for each added action, a selfloop labeled with this action. The very reason for using this mechanism is that it is neutral for the composition in the following sense: it leaves the companion i/o-automaton free to perform any wanted local action.

So, for Modal Interfaces, what would be a neutral procedure for extending alphabets? Indeed, considering ( 26) or [START_REF] Benveniste | The synchronous approach to reactive and real-time systems[END_REF] RR n°8147 yields two different answers, namely: for (26) :   α ∈ may 1 (q 1 ) and α ∈ whatever 2 (q 2 ) ⇓ α ∈ whatever (q 1 , q 2 )   for (28) :   α ∈ must 1 (q 1 ) and α ∈ whatever 2 (q 2 ) ⇓ α ∈ whatever (q 1 , q 2 )   where "whatever" denotes either may or must. Consequently, neutral alphabet extension is by adding

• may self-loops for the conjunction, and • must self-loops for the composition.

The bottom line is that we need different extension procedures. These observations explain why alphabet extension is properly handled neither by Interface Automata (see the last paragraph of Section VIII-B) nor by A/G-contracts (see the end of Section VII-C). These theories do not offer enough flexibility for ensuring neutral extension for all relations or operators.

We now list how alphabet extension must be performed for each relation or operator, for two Modal Interfaces C 1 and C 2 (the reader is referred to [START_REF] Raclet | A modal interface theory for component-based design[END_REF] for justifications). Alphabets are extended as follows, where Σ ⊇ Σ. Define the strong extension of C to Σ , written C ↑Σ , as follows:

C ↑Σ :                        (Σ in ) ↑Σ = Σ in ∪ (Σ \ Σ) (Σ out ) ↑Σ = Σ out Q ↑Σ = Q q ↑Σ 0 = q 0 may ↑Σ = may ∪ (Σ \ Σ) must ↑Σ = must ∪ (Σ \ Σ) (31)
In [START_REF] Benvenuti | A contract-based formalism for the specification of heterogeneous systems[END_REF], the added may and must transitions are all self-loops. The weak extension of C, written C ⇑Σ , is defined using the same formulas, with the only following modification:

C ⇑Σ : . . . = . . . must ⇑Σ = must (32)
Observe that the strong extension uses the classical inverse projection everywhere. The weak extension, however, proceeds differently with the must transitions in that it forbids the legal environments to submit additional actions as its outputs.

Using weak and strong alphabet equalization, the relations and operations introduced in Section VIII-C extend to variable alphabets as indicated now. In the following formulas, (Σ, Σ ) is a pair such that Σ ⊆ Σ , and (Σ 1 , Σ 2 , Σ) denotes a triple such that Σ = Σ 1 ∪ Σ 2 and satisfying the typing constraints

Σ in i = Σ in ∩ Σ i and Σ out i = Σ out ∩ Σ i for i = 1, 2.
It is understood that contract C has alphabet Σ, and so on.

Theorem 1: The following relations and operators

M |= M C ::= M |= M C ⇑Σ E |= E C ::= E |= E C ↑Σ C 1 C 2 ::= C 1 C ⇑Σ 2 C 1 ∧ C 2 ::= C ⇑Σ 1 ∧ C ⇑Σ 2 C 1 ⊗ C 2 ::= C ↑Σ 1 ⊗ C ↑Σ 2 C 1 /C 2 ::= C ⇑Σ 1 /C ↑Σ 2 ( 33
)
instantiate the meta-theory.

Proof: The first two formulas just provide definitions, so no proof is needed for them. Their purpose is to characterize the weakly and strongly extended Modal Interfaces in terms of their sets of environments and implementations. For both extensions, allowed output actions of the implementations are augmented whereas mandatory actions are not. For the weak extension, legal environments are not modified in that no additional output action is allowed for them. In contrast, for the strong extension, legal environments are allowed to submit any additional output action. These observations justify the other formulas. 2

E. Projecting and Restricting

A difficult step in the management of contracts was illustrated in Figure 4 of Section IV-D. It consists in decomposing a contract C into a composition of sub-contracts

i∈I C i C (34)
where sub-contract C i has alphabet

Σ i = Σ in i Σ out i .
As a prerequisite to [START_REF] Bertrand | Modal event-clock specifications for timed component-based design[END_REF], the designer has to guess some topological architecture by decomposing the alphabet of actions of C as

Σ = i∈I Σ i , Σ i = Σ in i Σ out i ( 35
)
such that composability conditions regarding inputs and outputs hold. Guessing architectural decomposition [START_REF] Bertrand | Modal event-clock specifications for timed component-based design[END_REF] relies on the designer's understanding of the system and how it should naturally decompose-this typically is the world of SysML. Finding decomposition ( 34) is, however, technically difficult in that it involves behaviors. It is particularly difficult if C is itself a conjunction of viewpoints or requirements, which typically occurs in requirements engineering, see Section XI:

C = k∈K C k ( 36
)
The algorithmic means we develop in the remaining part of this section will be instrumental in solving [START_REF] Bertrand | Modal event-clock specifications for timed component-based design[END_REF]. They will be used in the Parking Garage example of Section XI.

Projecting over a subalphabet: Projecting a contract over a sub-alphabet is the first natural tool for consideration. It is the dual operation with respect to alphabet extension that was developed in Section VIII-D. Two projections can be defined, which can be seen as under-and over-approximations, respectively, by referring to the refinement order.

Let C be a Modal Interface with alphabet Σ = Σ in ∪ Σ out and let Σ ⊂ Σ be a sub-alphabet. Define respectively the abstracted projection and refined projection

C ↓Σ = min {C | Σ C = Σ and C C} C ⇓Σ = max {C | Σ C = Σ and C C} ( 37
)
where "min" and "max" refer to refinement order for Modal Interfaces with different alphabets, see [START_REF] Bertrand | A compositional approach on modal specifications for timed systems[END_REF]. The projection C ⇓Σ (respectively C ↓Σ ) is computed via the following onthe-fly algorithm: 1) Perform ε-closure on the set of states by considering unobservable the actions not belonging to Σ , and then, 2) Perform determinization by giving priority to must over may (respectively to may over must), see Table VI for details.

Step 2) of the procedure for computing C ⇓Σ is a possible source of inconsistencies.

The abstracted projection C ↓Σ provides a projected view of a system-level contract over a small subset of actions. The abstracted projection is thus a useful tool for contract exploration and debug. It is not a synthesis tool, however. This is in contrast to the refined projection C ⇓Σ , which satisfies the following result. For any finite set {C i | i ∈ I} of Modal Interfaces with respective alphabets Σ i , we have, assuming that the left and right hand sides are properly defined-a typing property on input and output alphabets:

i∈I C i ∧ k∈K C ⇓Σi k k∈K C k (38)
To show this, by symmetry, it is enough to show [START_REF] Beyer | Web service interfaces[END_REF] with the conjunction on the right hand side replaced by any single C k for k selected from finite set K. For any i ∈ I, we have C ⇓Σi k C k , and thus

C i = def C i ∧ k∈K C ⇓Σi k C k (39)
holds for every i, from which [START_REF] Beyer | Web service interfaces[END_REF] follows. Unfortunately, the refined projection quite often gives raise to inconsistencies. In addition, the contract composition arising in left hand side of ( 38) is subject to incompatibilities. Informally said, this technique works if the sub-systems are only "loosely coupled" so that neither inconsistencies nor incompatibilities occur. To mitigate this problem we propose an alternative technique for turning a conjunction into a composition.

Restricting to a sub-alphabet: Let C be a Modal Interface with alphabet Σ = Σ in ∪ Σ out and let (Σ in , Σ out ) be two input and output sub-alphabets such that Σ out ⊆ Σ out . Set Σ = Σ in Σ out and define the restriction of C to Σ , denoted by C ↓Σ via the procedure shown in see [START_REF] Beugnard | Making components contract aware[END_REF].

Y = ε-closure(Σ -Σ , next(α, X)) 2.2 let m = Op{m C (q, α) | q ∈ X} 2.3 add to C a transition (X, α, Y ) with modality m 2.4 proj(Op, Y ) done let project(Op, C) = 1. let X 0 = ε-closure(Σ -Σ , q 0 ) 2. set initial state of C to X 0 3. proj(Op, X 0 ) 4. reduce C 5. return C let order ({cannot, may, must}, ≤) = must ≤ may cannot ≤ may in C ↓Σ = project(∨, C) C ⇓Σ = project(∧, C)
input: C, Σ in , Σ out , Σ in , Σ out ; output: C let order({cannot, may, must}, ≤ in ) = cannot ≤ in may ≤ in must order({cannot, may, must}, ≤ out ) = must ≤ may cannot ≤ may in let rest(X) = if X has not been visited, then 1. mark X visited 2. for every α ∈ Σ do 2.1 let Y = ε-closure(Σ -Σ , next(α, X)) 2.2 let m = Op{m C (q, α) | q ∈ X} where Op = if α ∈ Σ in then ∨ in else ∧ out 2.3 add to C a transition (X, α, Y ) with modality m 2.4 rest(Op, Y ) done let restrict(C) = 1. let X 0 = ε-closure(Σ -Σ , q 0 ) 2. set initial state of C to X 0 3. rest(Op, X 0 ) 4. reduce C 5. return C Table VII ALGORITHM FOR COMPUTING THE RESTRICTION C ↓Σ .
exists an action e and a state pair (q, R) in C/ /C ↓Σ , such that e has modality must in q and does not have modality must in R. We prove by contradiction that no such reachable state pair (q, R) and action e exist. Remark that by definition of the restriction, q ∈ R. The restriction is assumed to be in reduced form, meaning that it does not contain inconsistent states. Two cases have to be considered: 1) Action e has modality cannot in R. Several sub-cases have to be considered, depending on the I/O status of e and on the fact that the reduction of the restriction has turned a may modality for e into a cannot. In all cases, action e has modality cannot or may in q, which contradicts the assumption. 2) Action e has modality may in R. This implies that e also has modality may in q, which contradicts the assumption. This finishes the proof of the lemma.

2

The following holds by Lemma 10:

C ↓Σ ⊗ (C/ /C ↓Σ ) C C/ /C ↓Σ has no inconsistent state (C ↓Σ , C/ /C ↓Σ )
has no incompatible pair of states [START_REF] Bhaduri | A proposal for real-time interfaces in speeds[END_REF] By Lemma 11, the only property for checking is the consistency of C ↓Σ . This is a significant improvement compared to the issues raised by the refined projection, as explained in the paragraph following [START_REF] Bhaduri | Interface synthesis and protocol conversion[END_REF]. Decomposition [START_REF] Bhaduri | A proposal for real-time interfaces in speeds[END_REF] can be used while sub-contracting through the following algorithm:

Algorithm 1: We are given some system-level contract C. The top-level designer guesses some topological architecture according to [START_REF] Bertrand | Modal event-clock specifications for timed component-based design[END_REF]. Then, she recursively decomposes:

C = C 0 C 0↓Σ 1 ⊗ C 1 C 0↓Σ 1 ⊗ C 1↓Σ 2 ⊗ C 2 . . . C 0↓Σ 1 ⊗ . . . ⊗ C n-1 ↓Σn = def C(Σ 1 ) ⊗ . . . ⊗ C(Σ n ) (41)
which ultimately yields a refinement of C by a compatible composition of local sub-contracts. 2

Discussion: The operations of projection and restriction that we introduced here can probably be made be generic, at the level of the meta-theory. Observe, however, that such operations explicitly refer to the notion of sub-alphabet, which does not exist at the level of the meta-theory. In addition, Modal Interfaces are the only concrete theory in which variable alphabets are properly supported. For these two reasons, we preferred to develop these operations for Modal Interfaces only.

F. Observers

Here we develop observers for a Modal Interface C = (Σ in , Σ out , Q, q 0 , →,

) having no inconsistent state, meaning that →⊆ . With this consistency assumption in force, observers are then obtained as follows, with reference to Definition 2:

• Condition 2 of Definition 7 boils down to requiring that E × C must simulates E. Simulation testing can thus be used to check this; call b E C (E) the corresponding verdict. • To test for implementations, we first construct the maximal environment E C and apply testing to check simulation of E C × M by C may , call b M C,1 the corresponding verdict. Performing this requires maintaining pairs of states ((q E , q M ), (q E , q)) in simulation relation: (q E , q M )≤(q E , q). For any such pair of states, let b M C,2 denote the verdict answering whether (q E , q M ) α -→ E C ×M holds each time q α -→ holds, for any α ∈ Σ out . The overall verdict for implementation testing is then

b M C,1 (E C × M ) ∧ b M C,2 (E C × M )
Lemma 3 for generic observers specializes to the following, effective, semi-decision procedure:

Lemma 12: 1) If b E C outputs F, then C is incompatible; 2) If b M C,1 ∧ b M C,2 outputs F, then C is inconsistent. G. Bibliographical note
As explained in [START_REF] De Alfaro | Interface automata[END_REF], [START_REF] Chakrabarti | Synchronous and Bidirectional Component Interfaces[END_REF], [START_REF] Kim Guldstrand Larsen | Modal I/O Automata for Interface and Product Line Theories[END_REF], [START_REF] Doyen | Interface theories with component reuse[END_REF], [START_REF] Raclet | Modal interfaces: Unifying interface automata and modal specifications[END_REF], [START_REF] Raclet | A modal interface theory for component-based design[END_REF], Interface Theories make no explicit distinction between assumptions and guarantees.

Interface Automata, variants and extensions: Interface Automata were proposed by de Alfaro and Henzinger [START_REF] De Alfaro | Interface automata[END_REF], [START_REF] De | Game Models for Open Systems[END_REF], [START_REF] Luca | Interface-based design[END_REF], [START_REF] Chakrabarti | A Framework for Compositional Design and Analysis of Systems[END_REF] as a candidate theory of interfaces. In these references, Interface Automata focused primarily on parallel composition and compatibility. Quoting [START_REF] De Alfaro | Interface automata[END_REF]:

"Two interfaces can be composed and are compatible if there is at least one environment where they can work together". The idea is that the resulting composition exposes as an interface the needed information to ensure that incompatible pairs of states cannot be reached. This can be achieved by using the possibility, for a component, to refuse selected inputs from the environment at a given state [START_REF] De Alfaro | Interface automata[END_REF], [START_REF] Chakrabarti | Synchronous and Bidirectional Component Interfaces[END_REF]. In contrast to our development in Section VIII-B, no sets of environments and implementations are formally associated to an Interface Automaton in the original developments of the concept. A refinement relation for Interface Automata was defined in [START_REF] De Alfaro | Interface automata[END_REF]-with the same definition as ours-it could not, however, be expressed in terms of sets of implementations. Properties of interfaces are described in game-based logics, e.g., ATL [START_REF] Alur | Alternatingtime temporal logic[END_REF], with a theoretical high-cost complexity. The original semantics of an Interface Automaton was given by a two-player game between: an input player that represents the environment (the moves are the input actions), and an output player that represents the component itself (the moves are the output actions). Despite the availability of partial results [START_REF] Doyen | Interface theories with component reuse[END_REF], the framework of Interface Automata lacks support for the conjunction of interfaces in a general setting, and does not offer the flexibility of modalities. Sociable Interfaces [START_REF] Luca De Alfaro | Sociable Interfaces[END_REF] combine the approach presented in the previous paragraph with interface automata [START_REF] De Alfaro | Interface automata[END_REF], [START_REF] De Alfaro | Interface theories for component-based design[END_REF] by enabling communication via shared variables and actions 45 . First, the same action can appear as a label of both input and output transitions. Secondly, global variables do not belong to any specific interface and can thus be updated by multiple interfaces. Consequently, communication and synchronization can be one-toone, one-to-many, many-to-one, and many-to-many. Symbolic algorithms for checking the compatibility and refinement of sociable interfaces have been implemented in TICC [START_REF] Adler | Ticc: A Tool for Interface Compatibility and Composition[END_REF]. Software Interfaces were proposed in [START_REF] Chakrabarti | Interface compatibility checking for software modules[END_REF], as a pushdown extension of interface automata (which are finite state). Pushdown interfaces are needed to model call-return stacks of possibly recursive software components. This paper contains also a comprehensive interface description of Tiny OS, 46 an operating system for sensor networks. Moore machines and related reactive synchronous formalisms are very well suited to embedded systems modeling. Extending interface theories to a reactive synchronous semantics is therefore meaningful. Several contributions have been made in this direction, starting with Moore and Bidirectional Interfaces [START_REF] Chakrabarti | Synchronous and Bidirectional Component Interfaces[END_REF]. In Moore Interfaces, each variable is either an input or an output, and this status does not change in time. Bidirectional Interfaces offer added flexibility by allowing variables to change I/O status, depending on the local state of the interface. Communication by shared variable is thus supported and, for instance, allows distributed protocols or shared buses to be modeled. In both formalisms, two interfaces are deemed compatible whenever no variable is an output of both interfaces at the same time, and every legal valuation of the output variables of one interface satisfies the input predicate of the other. The main result of the paper is that parallel composition of compatible interfaces is monotonic with respect to refinement. Note that Moore and Bidirectional Interfaces force a delay of at least one transition between causally dependent input and output variables, exactly like Moore machines. In [START_REF] Doyen | Interface theories with component reuse[END_REF], the framework of Synchronous Interfaces is enriched with a notion of conjunction (called shared refinement). This development was further elaborated in [START_REF] Delahaye | Synchronous interface theories and time triggered scheduling[END_REF]. In Moore interfaces, legal values of the input variables and consequent legal values of the output variables are not causally related. Synchronous Relational Interfaces [START_REF] Tripakis | On relational interfaces[END_REF], [START_REF] Tripakis | A theory of synchronous relational interfaces[END_REF] have been proposed to capture functional relations between the inputs and the outputs associated to a component. More precisely, input/output relations between variables are expressed as first-order logic formulas over the input and output variables. Two types of composition are then considered, connection and feedback. Given two relational interfaces C 1 and C 2 , the first one consists in connecting some of the output variables of C 1 to some of the input variables of C 2 whereas feedback composition allows one to connect an output variable of an interface to one of its own inputs. The developed theory supports refinement, compatibility and also conjunction. The recent work [START_REF] Henzinger | Independent implementability of viewpoints[END_REF] studies conditions that need to be imposed on interface models in order to enforce independent implementability with respect to conjunction. Finally, [START_REF] Cerný | Interface simulation distances[END_REF] develops the concept of simulation distances for interfaces, thereby taking robustness issues into account by tolerating errors. Finally, Web services Interfaces were proposed in [START_REF] Beyer | Web service interfaces[END_REF].

The discussion of variants and extensions related to time, resources, and probability, is deferred to corresponding sections.

Modal Interfaces, variants and extensions: Properties expressed as sets of traces can only specify what is forbidden.

Unless time is explicitly invoked in such properties, it is not possible to express mandatory behaviors for designs. Modalities were proposed by Kim Larsen [START_REF] Guldstrand | A Modal Process Logic[END_REF], [START_REF] Antonik | 20 Years of Modal and Mixed Specifications[END_REF], [START_REF] Boudol | Graphical versus logical specifications[END_REF] as a simple and elegant framework to express both allowed and 46 http://www.tinyos.net/ mandatory properties. Modal Specifications basically consist in assigning a modality may or must to each possible transition of a system. They have been first studied in a process-algebraic context [START_REF] Guldstrand | A Modal Process Logic[END_REF], [START_REF] Guldstrand | Modal specifications[END_REF] in order to allow for loose specifications of systems. Since then, they have been considered for automata [START_REF] Kim Guldstrand Larsen | On Modal Refinement and Consistency[END_REF] and formal languages [START_REF] Raclet | Quotient de spécifications pour la réutilisation de composants[END_REF], [START_REF] Raclet | Residual for Component Specifications[END_REF] and applied to a wide range of application domains (see [START_REF] Antonik | 20 Years of Modal and Mixed Specifications[END_REF] for a complete survey). Informally, a must transition is available in every component that realizes the modal specification, while a may transition needs not be. A modal specification thus represents a set of models-unfortunately, models of modal transition systems are often call "implementations" in the literature, which is unfortunate in our context. We prefer keeping the term "model" and reserve the term "implementation" for the entities introduced in Sections VIII-B and VIII-C. Modal Specifications offer built-in conjunction of specifications [START_REF] Kim Guldstrand Larsen | A constraint oriented proof methodology based on modal transition systems[END_REF], [START_REF] Raclet | Why are modalities good for interface theories?[END_REF]. The expressiveness of Modal Specifications has been characterized as a strict fragment of the Hennessy-Milner logic in [START_REF] Boudol | Graphical versus logical specifications[END_REF] and also as a strict fragment of the mu-calculus in [START_REF] Feuillade | Modal specifications are a syntactic fragment of the Mucalculus[END_REF]. The formalism is rich enough to specify safety properties as well as restricted forms of liveness properties. Modal Interfaces with the right notion of compatibility were introduced in [START_REF] Raclet | Modal interfaces: Unifying interface automata and modal specifications[END_REF], [START_REF] Raclet | A modal interface theory for component-based design[END_REF] and the problem of alphabet equalization with weak and strong alphabet extensions was first correctly addressed in the same references. In [START_REF] Bauer | On Weak Modal Compatibility, Refinement, and the MIO Workbench[END_REF], compatibility notions for Modal Interfaces with the passing of internal actions are defined. Contrary to the approach reviewed before, a pessimistic view of compatibility is followed in [START_REF] Bauer | On Weak Modal Compatibility, Refinement, and the MIO Workbench[END_REF], i.e., two Modal Interfaces are only compatible if incompatibility between two interfaces can occur in any environment. A verification tool called MIO Workbench is available. The quotient of Modal Specifications was studied in [START_REF] Kim | Equation solving using modal transition systems[END_REF], [START_REF] Raclet | Residual for Component Specifications[END_REF]. Determinism plays a role in the modal theory. Non-deterministic Modal Interfaces have possibly non-deterministic i/o-automata as class of components. They are much more difficult to study than deterministic ones and corresponding computational procedures are of higher complexity. A Modal Interface is said to be deterministic if its may-transition relation is deterministic. For nondeterministic Modal Interfaces, modal refinement is incomplete [START_REF] Kim Guldstrand Larsen | On Modal Refinement and Consistency[END_REF]: there are nondeterministic Modal Interfaces C 1 and C 2 for which the set of implementations of C 1 is included in that of C 2 without C 1 being a modal refinement of C 2 . Hence refinement according to the meta-theory is not exactly instantiated but only approximated in a sound way. A decision procedure for implementation inclusion of nondeterministic Modal Interfaces does exist but turns out to be EXPTIME-complete [START_REF] Antonik | Complexity of Decision Problems for Mixed and Modal Specifications[END_REF], [START_REF] Benes | Checking Thorough Refinement on Modal Transition Systems Is EXPTIME-Complete[END_REF] whereas the problem is PTIME-complete if determinism is assumed [START_REF] Raclet | Why are modalities good for interface theories?[END_REF], [START_REF] Benes | On determinism in modal transition systems[END_REF]. The benefits of the determinism assumption in terms of complexity for various decision problems on modal specifications is underlined in [START_REF] Benes | On determinism in modal transition systems[END_REF]. The "merge" of non-deterministic Modal Specifications regarded as partial models has been considered in [START_REF] Uchitel | Merging partial behavioural models[END_REF]. This operation consists in looking for common refinements of initial specifications and is thus similar to the conjunction operation presented here. In [START_REF] Uchitel | Merging partial behavioural models[END_REF], [START_REF] Fischbein | On correct and complete strong merging of partial behaviour models[END_REF], algorithms to compute the maximal common refinements (which are not unique when non-determinism is allowed) are proposed. They are implemented in the tool MTSA [START_REF] Nicolás | MTSA: The Modal Transition System Analyser[END_REF]. Assume/guarantee contracts viewed as pairs of Modal Specifications were proposed in [START_REF] Gössler | Modal Contracts for Component-based Design[END_REF]. It thus combines the flexibility offered by the clean separation between assumptions and guarantees and the benefits of a modal framework. Several operations are then studied: refinement, parallel composition, conjunction and priority of aspects. This last operation composes aspects in a hierarchical order, such that in case of inconsistency, an aspects of higher priority overrides a lower-priority contract. The synthesis of Modal Interfaces from higher-level specifications has been studied for the case of scenarios. In [START_REF] Sibay | Existential Live Sequence Charts Revisited[END_REF], Existential Live Sequence Charts are translated into Modal Specifications, hence providing a mean to specify modal contracts. Regarding extensions, Acceptance Interfaces were proposed by J-B. Raclet [START_REF] Raclet | Quotient de spécifications pour la réutilisation de composants[END_REF], [START_REF] Raclet | Residual for Component Specifications[END_REF]. Informally, an Acceptance Interface consists of a set of states, with, for each state, a set of ready sets, where a ready set is a set of possible outgoing transitions from that state. In intuitive terms, an Acceptance Interface explicitly specifies its set of possible models. Acceptance Interfaces are more expressive than Modal Interfaces but at the price of a prohibitive complexity for the various relations and operators of the theory. Modal Interfaces have been enhanced with marked states by Caillaud and Raclet [START_REF] Caillaud | Ensuring Reachability by Design[END_REF]. Having marked states significantly improves expressiveness. It is possible to specify that some state must be reachable in any implementation while leaving the particular path for reaching it unspecified. As an example of use, Modal Interfaces with marked states have been applied in [START_REF] Benveniste | Application of Interface Theories to the Separate Compilation of Synchronous Programs[END_REF] to the separate compilation of multiple clocked synchronous programs.

The discussion of variants and extensions related to time, resources, and probability, is deferred to corresponding sections.

Features of our presentation: The presentation of interface theories in this paper is new in many aspects. For the first time, all interface theories are clearly cast in the abstract framework of contracts following our meta-theory. In particular, the association, to an interface C, of the two sets E C and M C is new. It clarifies a number of concepts. In particular, the interface theories inherit from the properties of the metatheory without the need for specific proofs. The projection and restriction operators for Modal Interfaces are new. Casting interface theories into the meta-theory was developed for the basic interface theories only. It would be useful to extend this to the different variants and see what the benefit would be. Benoît Caillaud has developed the MICA tool [START_REF] Caillaud | Mica: A Modal Interface Compositional Analysis Library[END_REF], which implements Modal Interfaces with all the operations and services discussed in this section.

IX. PANORAMA: TIMED INTERFACE THEORIES

In this section we develop an instance of an interface theory for timed systems. This section is meant to be illustrative of our approach to concrete instances of contract theories. It does not claim to expose the good instance. Our presentation builds on top of [START_REF] Bertrand | Modal event-clock specifications for timed component-based design[END_REF]. To simplify the exposure, we restrict ourselves to the case of a fixed alphabet Σ. As usual now, we begin with the component model.

A. Components as Event-Clock Automata

Timed Automata [START_REF] Alur | A theory of timed automata[END_REF] constitute the basic model for systems dealing with time and built on top of automata. In words, timed automata are automata enhanced with clocks. Predicates on clocks guard both the states (also called "locations") and the transitions. Actions are attached to transitions that result in the resetting of some of the clocks.

Event-Clock Automata [START_REF] Alur | A determinizable class of timed automata[END_REF], [START_REF] Alur | Event-clock automata: A determinizable class of timed automata[END_REF], [START_REF] Bertrand | Modal event-clock specifications for timed component-based design[END_REF] form a subclass of timed automata where clock resets are not arbitrary: each action α comes with a clock h α which is reset exactly when action α occurs. The interest of this subclass is that event-clock automata are determinizable, which facilitates the development of a (modal) theory of contracts. The definition of event-clock automata requires some prerequisites.

We are given an underlying finite set H of clocks. A clock valuation is a map ν : H → R + , where R + denotes the set of nonnegative reals. The set of all clock valuations is denoted by V. We denote by 0 the clock valuation assigning 0 to all clocks and by ν + t the clock obtained by augmenting ν with the constant t. For ν a valuation, the valuation ν[0/h α ] assigns 0 to h α and keeps the valuation of other clocks unchanged.

Clocks can be used to define guards. The class of guards considered by [START_REF] Bertrand | Modal event-clock specifications for timed component-based design[END_REF] consists of finite conjunctions of expressions of the form h ∼ n where h is a clock, n is an integer, and ∼ is one of the following relations: <, ≤, =, ≥, >. For g a guard, write ν |= g to mean that valuation ν satisfies guard g. For N an integer, G(H, N ) denotes the set of all guards over H involving only integers n < N + 1 and we write G(H) = G(H, ∞).

Definition 13: An event-clock automaton over alphabet Σ is a tuple M = (Σ in , Σ out , Q, q 0 , N, →), where:

• Σ in , Σ out , Q, q 0 are as for i/o-automata; elements of Q are called locations;

• H Σ = {h α | α ∈ Σ} is the set of clocks; • N is a finite integer and →⊆ Q × G(H Σ , N ) × Σ × Q is the transition relation; write q g,α
-→ q to mean that (q, g, α, q ) ∈→.

The semantics of M is a timed transition system with infinite state space Q × V, defined as follows: transition q g,α -→ q can fire from state (q, ν) ∈ Q × V iff ν |= g; as a result of this firing, the clock h α is reset to zero, thus resulting in the new state (q , ν[0/h α ]) ∈ Q × V. In our Timed Interface theory, components are event-clock automata that are:

1) deterministic in the following sense:

∀(q, α, ν) ∈ Q × Σ × V, there is at most one transition q g,α -→ q such that ν |= g. ( 42
)
2) receptive, meaning that

∀q ∈ Q, ∀α ∈ Σ in : q T,α -→
holds, where T denotes the trivial guard "true".

RR n°8147

Instead of further developing our theory we will show how to take advantage of previously developed theories by showing that event-clock automata are finitely encoded by means of region automata that we introduce next. Fix bound N . A region is an equivalence class ϑ of clock valuations ν satisfying the same set of guards from G(H, N ). Denote by Θ the set of all such regions (bound N is understood). For ϑ ∈ Θ, consider

τ (ϑ) = {ϑ | ∃ν ∈ ϑ , ∃ν ∈ ϑ, ∃t ≥ 0 s.t. ν = ν + t}
which is the set of all regions that can be obtained from ϑ by letting time elapse. Finally, for ϑ a region and α an action, ϑ ↓α is the region obtained from ϑ by resetting clock h α . Using these notations, we associate, to each event-clock automaton M = (Σ in , Σ out , Q, q 0 , N, →), a Region Automaton, which is the following finite state automaton:

R [M ] = Σ in × Θ, Σ out × Θ, Q × Θ, (q 0 , 0), ⇒ (43)
where the transition relation ⇒ is given by:

(q, ϑ) ϑ",α ===⇒ (q , ϑ ) iff    q g,α → q , with ϑ" ⊆ τ (ϑ) ∩ g and ϑ = ϑ" ↓α (44)
Vice-versa, any Region Automaton R defines a unique event-clock automaton M [R] by deducing, from [START_REF] Booch | Unified Modeling Language User Guide, The (2nd Edition)[END_REF], the minimal guards associated to its transitions. Starting from an event-clock automaton

M , M [R [M ]
] is related to M by a strengthening of its guards. However, it holds that 47

R [M [R [M ]]] = R [M ] (45)
Under the above correspondence, components in the event-clock automaton domain are mapped to components in the i/o-automaton domain.

B. Modal Event-Clock Specifications

In this section we develop the framework of contracts on top of our component model of deterministic event-clock automata. To simplify, we only develop the case of a fixed alphabet Σ.

Definition 14: A Modal Event-Clock Specification (MECS) is a tuple C = (Σ in , Σ out , Q, q 0 , →,
), where Σ in , Σ out , Q, q 0 are as in Interface Automata and

→ ⊆ ⊆ Q × G(H Σ ) × Σ × Q
Using the same construction as above, MECS C induces a Region Modal Event-Clock Specification (RMECS) denoted by R [C], which is a Modal Interface according to Definition 7.

Accordingly, R [C] defines a pair (E R[C] , M R[C]
) of sets of i/o-automata and we finally define

(E C , M C ) = def M E R[C] , M M R[C]
The map

C → R [C] satisfies: 48 R [M [R [C]]] = R [C] ( 46
)
47 It is shown in [START_REF] Bertrand | Modal event-clock specifications for timed component-based design[END_REF] that M → R [M ] forms a Galois connection. 48 Again, it is a Galois connection [START_REF] Bertrand | Modal event-clock specifications for timed component-based design[END_REF].

This allows us to lift the contract theory of RMECS (which are Modal Interfaces) to a contract theory of MECS. While this is conceptually elegant, it is not efficient since moving from MECS to RMECS (from timed models to region models) is ExpTime, which is costly. To cope with this difficulty, the authors of [START_REF] Bertrand | Modal event-clock specifications for timed component-based design[END_REF] have provided direct cheap formulas, expressed in the MECS domain. These formulas provide a partial answer to the issue of complexity. In particular, the following lemma holds that was stated and proved in [START_REF] Bertrand | Modal event-clock specifications for timed component-based design[END_REF]:

Lemma 13: For C 1 and C 2 two MECS having identical input and output alphabets, define C 1 ∧C 2 symbolically with rules of the following form:

Glb may : q 1 g1,α q 1 and q 2 g2,α q 2 (q 1 , q 2 ) g1∧g2.α (q 1 , q 2 )
Glb must,left :

q 1 g1,α
→ q 1 and q 2 g2,α q 2 (q 1 , q 2 ) g1∧g2.α

→ (q 1 , q 2 )
where denotes ad libitum → or and with Glb must,right defined symmetrically (see [START_REF] Bertrand | Modal event-clock specifications for timed component-based design[END_REF] for the complete set of rules). Then, we have

R [C 1 ∧ C 2 ] = R [C 1 ] ∧ R [C 2 ] (47)
Inconsistent states for both sides of (47) correspond. A similar lemma holds for contract quotient C 1 /C 2 . Unfortunately, the pruning of inconsistent states cannot be performed directly in the MECS domain and mapping to regions is mandatory. Nevertheless, dedicated rules to handle directly inconsistent states exist in the symbolic versions of the different relations and operations on MECS. As a result, the computation of the regions is only mandatory when the designer aims at cleaning its contract by pruning the inconsistencies. A similar lemma holds for contract composition C 1 ⊗ C 2 . Again, pruning incompatible pairs of states cannot be performed directly in the MECS domain and mapping to regions is mandatory. 49

C. Bibliographical note

This note focuses on interface types of framework. The reader is referrect to the bibliographical note of Section VII-G for extensions of A/G-contracts addressing time.

A first interface theory able to capture the timing aspects of components is Timed Interfaces [START_REF] Luca De Alfaro | Timed Interfaces[END_REF]. Timed Interfaces allows specifying both the timing of the inputs a component expects from its environment and the timing of the outputs it can produce. Compatibility of two timed interfaces is then defined and refers to the existence of an environment such that timing expectations can be met. The Timed Interface theory proposed in [START_REF] David | Timed I/O automata : A complete specification theory for real-time systems[END_REF] fills a gap in the work introduced in [START_REF] Luca De Alfaro | Timed Interfaces[END_REF] by defining a refinement operation. In particular, it is shown that compatibility is preserved by refinement. This theory also proposes a conjunction and a quotient operation and is implemented in the tool ECDAR [START_REF] David | ECDAR: An Environment for Compositional Design and Analysis of Real Time Systems[END_REF]. Timed Specification Theories are revisited from a linear-time perspective in [START_REF] Chilton | Revisiting timed specification theories: A linear-time perspective[END_REF].

The first timed extension of modal transition systems was published in [START_REF] Cerans | Timed Modal Specification -Theory and Tools[END_REF]. It is essentially a timed (and modal) version of the Calculus of Communicating Systems (by Milner). Based on regions tool support for refinement checking were implemented and made available in the tool EPSILON [START_REF] Chr | Automatic verification of real-time systems using Epsilon[END_REF]. Another timed extension of Modal Specifications was proposed in [START_REF] Bertrand | Refinement and consistency of timed modal specifications[END_REF]. In this formalism, transitions are equipped with a modality and a guard on the component clocks, very much like in timed automata. For the subclass of modal event-clock automata, an entire algebra with refinement, conjunction, product, and quotient has been developed in [START_REF] Bertrand | A compositional approach on modal specifications for timed systems[END_REF], [START_REF] Bertrand | Modal event-clock specifications for timed component-based design[END_REF].

Resources other than time were also considered-with energy as the main target. Resource Interfaces [START_REF] Chakrabarti | Resource Interfaces[END_REF] can be used to enrich a variety of interface formalisms (Interface Automata [START_REF] De Alfaro | Interface automata[END_REF], Assume/Guarantee Interfaces [START_REF] De Alfaro | Interface theories for component-based design[END_REF], etc.) with a resource consumption aspect. Based on a two player gametheoretic presentation of interfaces, Resource Interfaces allow for the quantitative specification of resource consumption. With this formalism, it is possible to decide whether compositions of interfaces exceed a given resource usage threshold, while providing a service expressed either with Büchi conditions or thanks to quantitative rewards. Because resource usage and rewards are explicit rather then being defined implicitly as solutions of numerical constraints, this formalism does not allow one to reason about the variability of resource consumption across a set of logically correct models.

X. PANORAMA: PROBABILISTIC INTERFACE THEORIES

Probabilistic systems are non-deterministic systems in which choice is controlled by random trial. Such systems are useful for many purposes, ranging from physical or biological systems, to security protocols, intrusion detection, and up to safety and reliability analyses in system design. In this section, as another illustration of our meta-theory, we develop a simple instance of a probabilistic interface theory. Again, to simplify the exposure, we restrict ourselves to the case of a fixed alphabet Σ.

A. Components as Probabilistic Automata

We first introduce Probabilistic Automata with inputs and outputs, also called Input/Output Markov Decision Processes, and then we motivate their use in safety analysis. Definition 15: A Probabilistic Automaton with inputs and outputs (i/o-PA) is a tuple M = (Σ in , Σ out , Q, q 0 , Π, →), where

• Σ in and Σ out are disjoint finite input and output alphabets such that Σ in ∪ Σ out = Σ; • Q is a finite set of states and q 0 ∈Q is the initial state;

we denote by Π(Q) the finite set of all probabilities over Q, also called the probabilistic states;

• → ⊆ Q × Σ × Π(Q) is the transition relation; we write q α -→ π to mean (q, α, π) ∈ →, and q α -→ if q α
-→ π holds for some π;

• In addition, we require M to be deterministic in the following sense: for any pair (q, α)

∈ Q × Σ, q α -→ π and q α -→ π implies π = π .
A run σ of M starts from initial state q 0 and then progresses by a sequence of steps of the form q α -→ π → q , where supplementary transitions π → q are drawn at random by selecting a successor state q ∈ Q according to probability π. A strategy consists in fixing a function ϕ : Q → Σ and using it to select the next action. Once a strategy has been fixed, jumping from a probabilistic state to the next one gives raise to a time-invariant Markov Chain, whose invariant probability can be computed or statistically estimated. When all probabilistic states are Dirac measures δ q selecting q as a next state with probability one, i/o-PA M boils down to an i/o-automaton. Thus, i/o-PA subsume i/o-automata.

Two i/o-PA M 1 and M 2 are composable if Σ out 1 ∩ Σ out 2 = ∅. Two composable i/o-PA M 1 and M 2 compose into M = M 1 × M 2 as follows: (q 1 , q 2 ) α -→ M π 1 ⊗ π 2 iff q 1 α -→ M1 π 1 and q 2 α -→ M2 π 2 (48)
where ⊗ denotes the product of two probabilities, thus making the two components independent. Parallel composition defined in this way has all the desired properties.

Similarly, the concept of simulation relation is easily derived from that of i/o-automata by preserving probabilities: for M i , i = 1, 2 two i/o-PA and two states q i ∈ Q i , say that q 1 simulates q 2 , written q 2 ≤ q 1 if there exists a surjective map f :

Q 1 → Q 2 such that: ∀α s.t. q 2 α -→ 2 π 2 , ∃π 1 ∈ Π(Q 1 ) ⇓ (49)    q 1 α -→ 1 π 1 π 2 (q 2 ) = f (q 1 )=q 2 π 1 (q 1 ) π 1 (q 1 ) > 0 ⇒ f (q 1 ) ≤ q 1   
Observe that, since we consider only deterministic i/o-PA, there exists at most one π 2 such that q 2 α -→ 2 π 2 , hence there is no need to quantify over π 2 in the precondition of [START_REF] Caillaud | Mica: A Modal Interface Compositional Analysis Library[END_REF]. In probability theory, relation

π 2 (q 2 ) = f (q 1 )=q 2 π 1 (q 1 ) writes π 2 = f (π 1 ). Say that M 1 simulates M 2 , written M 2 ≤M 1 , if q 2,0 ≤q 1,0 . Simulation relation is preserved by composition. If M 2 ≤M 1 , then every strategy ϕ 2 : Q 2 → Σ 2 defined over M 2 has its counterpart into a matching strategy ϕ 1 : Q 1 → Σ 1 over M 1 by setting ϕ 1 (q 1 ) = ϕ 2 (f (q 1 )). For i = 1, 2, let Ω i = Q N
i be the set of all sequences of states of Q i , and let (Ω i , P i ), i = 1, 2 be the two resulting probability spaces when matching strategies are used for M 1 and M 2 . Then, the map f induces a measurable map ψ = (f, f, . . . ) : Ω 1 → Ω 2 such that Z(ω 2 )dP 2 (ω 2 ) = Z(ψ(ω 1 ))dP 1 (ω 1 ). In particular, the probability distributions with respect to P 1 and P 2 , of any measurable function depending only on the successive actions performed, are identical.

The natural use of i/o-PAs for safety/reliability analysis is to capture faulty situations through states. Component states are partitioned into safe states and faulty states that can be equipped with different fault labels (names of states can do this, no semantic adaptation is needed). The probabilistic part of i/o-PAs naturally captures the spontaneous occurrence of faults. When in a faulty state, a component outputs actions that can either be used to model fault propagation, or may be alarms for use in system supervision. Input actions in a faulty state can be used to either model denial of service from other components (thus resulting in a risk of moving to a faulty state), or may be reconfiguration actions. Thus, spontaneous occurrence of failures with fault propagation is captured by this framework. To summarize, i/o-PAs offer a natural framework in which to combine functional and safety viewpoints.

B. Simple Modal Probabilistic Interfaces

By following the same steps as for Modal Interfaces, see Definition 7, we can define Simple Modal Probabilistic Interfaces as pairs C = (C may , C must ) of i/o-PAs. There is no new difficulty in doing this. Expressiveness of this framework, however, is modest; whence the attribute "simple". When used in the context of safety/reliability analysis, Simple Modal Probabilistic Interfaces support the specification of fault accommodation in systems. For example, one can specify about a component:

• that it does not accommodate denial of service: inputs representing fault propagation are disallowed ("must not occur"); • that it must be prepared to possible denial of service: inputs representing fault propagation are allowed ("must be accepted"); • that it never generates spontaneous failures: actions leading to a probabilistic state from which a faulty state can be immediately reached are disallowed ("must not occur"); • that spontaneous failures are unavoidable: actions leading to a probabilistic state from which a faulty state can be immediately reached are allowed ("must be accepted"). One could argue that i/o-PA by themselves offer a similar expressiveness by playing with probabilities. Simple Modal Probabilistic Interfaces, however, offer the full algebra of contracts, which i/o-PA don't.

C. Bibliographical note

This note focuses on interface types of framework. The reader is referred to the bibliographical note of Section VII-G for extensions of A/G-contracts addressing probability.

Exactly like the Interval Markov Chain (IMC) formalism [START_REF] Jonsson | Specification and refinement of probabilistic processes[END_REF] they generalize, Constraint Markov Chains (CMC) [START_REF] Caillaud | Compositional design methodology with constraint Markov chains[END_REF] are abstractions of a (possibly infinite) sets of Discrete Time Markov Chains. Instead of assigning a fixed probability to each transition, transition probabilities are kept symbolic and defined as solutions of a set of first order formulas. Variability across implementations is made possible not only with symbolic transition probabilities, but also thanks to the labelling of each state by a set of valuations or sets of atomic propositions. This allows CMCs to be composed thanks to a conjunction and a product operators. While the existence of a residuation operator remains an open problem, CMCs form an interface theory in which satisfaction and refinement are decidable, and compositions can be computed using quantifier elimination algorithms. In particular, CMCs with polynomial constraints form the least class of CMCs closed under all composition operators. Abstract Probabilistic Automata (APA) [START_REF] Delahaye | Abstract Probabilistic Automata[END_REF] is another specification algebra with satisfaction and refinement relations, product and conjunction composition operators. Despite the fact that APAs generalize CMCs by introducing a labeled modal transition relation, deterministic APAs and CMCs coincide, under the mild assumption that states are labeled by a single valuation. For both formalisms, parallel composition is restricted to noninteracting components, since alphabets of actions must be disjoint.

Our formalism of Simple Modal Probabilistic Interfaces exhibits the whole contract algebra. Regarding limitations, unlike IMC, CMC, and APA, this model does not allow for specifying families of transition probabilities and, hence, it cannot help for quantitative reasoning about reliability analysis.

XI. THE PARKING GARAGE, AN EXAMPLE IN REQUIREMENTS ENGINEERING

In this section we develop the parking garage example introduced in Section IV-C. Some of the material is repeated for better readability. Despite being simple and small, this example quickly becomes complex for reasons that are intrinsic to the formal management of requirements. The MICA tool developed by Benoît Caillaud was used to develop it [START_REF] Caillaud | Mica: A Modal Interface Compositional Analysis Library[END_REF].

Requirements are written in constrained English language and then translated into Modal Interfaces-while the presented translation is manual, automatic translation can be envisioned. 50 Once this is completed, contracts are formally defined and the apparatus of contracts can be used. In particular, important properties regarding certification can be formally defined and checked, e.g., consistency, compatibility, correctness, and completeness. In addition, support is provided for turning top-level requirements into an architecture of subsystems, each one equipped with its own requirements. The latter can then be submitted to independent suppliers for further development.

A. The contract framework

We shall use Modal Interfaces (with variable alphabet) as developed in Sections VIII-C and subsequent ones. There are three main reasons for this choice:

1) By offering the may and must modalities, Modal Interfaces are well suited to express mandatory and optional behaviors in the specification, which we consider important for requirements engineering.

2) Being large sets of requirements structured into chapters, requirements documents are a very fragmented style of specification. Only Modal Interfaces offer the needed support for an accurate translation of concepts such as "set of requirements", "set of chapters", together with a qualification of who is responsible for each requirement (the considered component or sub-system versus its environment). 3) As we shall see, at the top-level, conjunction prevails.

However, as soon as the designer refines the top-level requirements into an architecture of sub-systems, composition enters the game. Turning a conjunction of toplevel requirements into a composition of sub-systems specifications thus becomes a central task. Only Modal Interfaces provide significant assistance for this. Overall, the problem considered in claim 3) can be stated as follows. The designer begins with some system-level contract C, which is typically specified as a conjunction of viewpoints and/or requirements. The designer guesses some topological architecture by decomposing the alphabet of actions of C as

Σ = i∈I Σ i , Σ i = Σ in i Σ out i (50)
such that composability conditions regarding inputs and outputs hold. Once this is done, we expect our contract framework to provide help in generating a decomposition of C as

i∈I C i C (51)
where sub-contract C i has alphabet

Σ i = Σ in i Σ out i .
Guessing architectural decomposition (50) relies on the designer's understanding of the system and how it should naturally decompose-this typically is the world of SysML. Finding decomposition (51) is, however, technically difficult in that it involves behaviors. The algorithmic means that were presented in Section VIII-E provide the due answer. In this Parking Garage example, we will use both the abstracted projection and the restriction that were developed in that section.

B. Top level requirements

In this section, we begin with the top-level requirements. The system under specification is a parking garage subject to payment by the user. At its most abstract level, the requirements document comprises the different chapters gate, payment, and supervisor, see Table VIII. The gate chapter will collect the generic requirements regarding entry and exit gates. These generic requirements will then be specialized for entry and exit gates, respectively. Focus on the "gate" chapter. It consists of the three requirements shown on Table VIII. Requirement R g.1 is best described by means of an i/o-automaton, shown in Figure 7we provide an informal textual explanation for it, between quotes. 51 The other two requirements are written using constrained natural language, which can be seen as a boilerplate style of specification. Prefix "?" indicates an input and prefix "!" indicates an output.

0

The first two requirements are not under the responsibility of the system, since they rather concern the car driver. Thus it does not make sense to include them as part of the guarantees offered by the system. Should we remove them? This would be problematic. If drivers behave the wrong way unexpected things can occur for sure. The conclusion is that 1) we should keep requirements R g.1 and R g.2 , and 2) we should handle them differently than R g.3 , which is a guarantee offered by the system. Indeed, R g.1 and R g.2 are assumptions under which the gate operates as guaranteed. In the sequel, assumptions are written in italics.

So far we have specified gate as a list of requirements. Requirement R g.1 specified as an i/o-automaton can be considered formal. Requirements R g.2 and R g.3 are formulated in constrained natural language and are ready for subsequent formalization, e.g., as i/o-automata. Are we done? Not yet! We need to give a formal meaning to what it means to have a collection of requirements, and what it means to distinguish assumptions from guarantees. The contract framework we develop next will provide support for this.

C. Formalizing requirements as contracts

We shall use Modal Interfaces (with variable alphabet) as developed in Sections VIII-C and subsequent ones. Thus, we first need to explain how the specification of "gate" in Table VIII translates into Modal Interfaces.

We first observe that each requirement R g.j of Table VIII is a sentence that can be formalized as an i/o-automaton, see Figure 7 for such a formalization of requirement R g.1 . Accordingly, each chapter D = gate/payment/supervisor of Table VIII is structured as a pair

D = ((A 1 , . . . , A m ), (G 1 , . . . , G n )) (52)
where the A i s (the assumptions) and the G j s (the guarantees) are i/o-automata in which all involved actions possess the same status (input or output) throughout all A i s and G j s. The translation of a specification of the form (52) into a Modal Interface is performed by applying the following two series of rules:

Rules 1: We adopt the following rules for the translation of guarantees (in the form of i/o-automata) into Modal Interfaces: R G 1 : Unless otherwise explicitly stated, transitions labeled by an output action of the considered system are given a may modality; the rationale for doing this is that the default semantics for guarantees is "best effort". A must modality is assigned if the requirement specifies it-e.g., by having a "must" in the sentence. R G 2 : Transitions labeled by an input action of the considered system are given a must modality; the rationale for doing this is that, as part of its guarantees, the component must not refuse an input that is "legally" submitted by the environment. R G 3 : Guarantees in a same requirements chapter D combine by conjunction. Applying Rules 1 to the set of guarantees of D yields the contract encoding these guarantees, denoted by G D .

2

Performing this for the single guarantee R g.3 of gate yields the Modal Interface shown in Figure 8. Rules 2: We adopt the following rules for the translation of assumptions (in the form of i/o-automata) into Modal Interfaces: R A 1 : We exchange the status input/output in every assumption, thus taking the point of view of the environment. R A 2 : Having done this, we apply Rules 1 to the assumptions. So far this yields a draft Modal Interface A that must be satisfied by every environment. R A 3 : This is not enough, however, as we really want environments that submit all legal stimuli. To ensure this, we simply turn, in A, all may transitions to must transitions, which yields A.

0 1 !gate_open !gate_close 0 1 !gate_open !gate_close
Applying Rules 2 to the set of assumptions of D yields the Modal Interface A D encoding these assumptions. 2

Performing this for the assumptions R g.1 and R g.2 of gate yields the Modal Interface shown in Figure 9. So far we have represented any chapter D of the requirements document as a pair of Modal Interfaces (A D , G D ) with mirroring input/output statuses for their actions-every input of A D is an output of G D and vice-versa. It is the merit of Modal Interfaces to allow for a direct representation of this pair of assumption and guarantee in the form of a single Modal Interface, by using the following formula, for A and G two Modal Interfaces with mirroring input/output statuses for their actions:

(A, G) is represented by the quotient (A ⊗ G)/A , (53)
which is the contract characterizing the components that implement G in the context of A, see Section V-E. Performing this for the whole chapter gate yields the Modal Interface shown in Figure 10. Some comments are in order regarding this Modal Interface:

• Regarding the guarantees offered by the component: Allowed outputs possess a may modality, which reflects that Guarantees specify what the component may deliver.

Other actions are forbidden. the component should not refuse legal stimuli from its environment. Violation of the contract by its environment occurs when an illegal input is submitted by the environment (vehicle_through when exiting state 0 or state 3). As a consequence, the whole contract gets relaxed, which is reflected by the move to the special state "2", from which any action is allowed-such a state is often called a "top" state. Note that this top state resulted from computing the quotient.

The same procedure applies to all chapters gate, payment, and supervisor, of the top-level textual specification, shown in Table IX (it is an expansion of Table VIII). In particular, the Modal Interfaces encoding chapters payment and supervisor of the top-level are displayed in Figures 11 to 13. Figure 13 showing the contract associated to the supervisor is unreadable and the reader may wonder why we decided to put it here. We indeed wanted to show that, when contract design is performed formally and carefully, top-level contracts rapidly become complex, even for modest sets of requirements. So the formal management of requirements and their translation into formal contracts must be tool-assisted.

Finally, the whole top-level contract C is the conjunction of the contracts representing chapters gate, payment, and supervisor, of the top-level requirements document:

C = C gate ∧ C payment ∧ C supervisor (54)
Owing to the complexity of C supervisor shown in Figure 13, we do not show the Modal Interface C formalizing the full document. Nevertheless, the latter was generated and can then be exploited as we develop next. The above specification only covers the functional viewpoint of the system. Other viewpoints might be of interest as well, e.g., regarding timing behavior and energy consumption. They would be developed with the same method and combined to the above contract C using conjunction.

D. Sub-contracting to suppliers

In this section, we apply the technique developed in Section VIII-E for generating an architecture of sub-systems with their associated sets of requirements. Each sub-system can then be submitted for independent development to a different supplier.

The duty of the designer is to specify an architecture "à la SysML", as shown on Figure 14. Some comments are in order regarding this architecture. The considered instance of a parking garage consists of one entry gate, one exit gate, and one payment machine. Compare with the top-level specification of Table IX. The latter comprises a generic gate, a payment machine, and a supervisor, each one with its set of requirements. In contrast, the architecture of Figure 14 involves no supervisor. The supervisor is meant to be distributed among the two gates. The architecture of Figure 14 seems to be very loosely coupled. First, the PaymentMachine seems to be totally independent. In fact, the ticket that is inserted in the exit gate must coincide with the one issued by the PaymentMachine. It turns out that this reflects a missing assumption regarding the environment of the system (namely the user of the parking). Then, the two gates seem to have the RR n°8147 shared input "?vehicle exit" as their only interaction. But this shared input is involved in requirement R s.3 , which forbids the entry if the parking is full.

In Figure 15 we show the result of applying, to the architecture of Figure 14, the Algorithm 1 developed in Section VIII-E, which yields by construction a refinement of the top-level contract C by a decomposition into local contracts:

C C(Σ EntryGate ) ⊗ C(Σ ExitGate ) ⊗ C(Σ PaymentMachine ) (55)
Local contract C(Σ EntryGate ) is the more complex one because it involves counting-we have assumed a capacity of two to keep it simple. Remarkably enough, the decomposition (55) involves small sub-systems compared to C supervisor (Fig. 13) and the global contract C; the restriction operation is to be acknowledged for this strong reduction in size.

E. The four "C"

Requirements capture and management are important matters for discussion with certification bodies. These bodies would typically assess a number of quality criteria from, e.g., the following list elaborated by INCOSE [START_REF]Incose systems engineering handbook[END_REF] Conciseness, Conformance, Consistency, Correctness, Criticality, Level, Orthogonality, Priority, Risk, Unambiguousness, and Verifiability. In this section we focus on four quality criteria that are considered central by certification authorities and are relevant to contracts, namely: Completeness, Correctness, Consistency, and Compatibility.

1) Consistency & Compatibility: Consistency and compatibility have been formally defined in the meta-theory, see Section V and Table IV therein. In particular, those formal definitions can be formally checked. Thus, the question arises whether these formal definitions suitably reflect the common sense meaning of these terms.

According to the common meaning, a set of requirements is consistent if it is not self-contradicting. The intent is that there is no point in trying to implement an inconsistent set of requirements, as no such implementation is going to exist.

RR n°8147

It turns out that the existence of implementations is the formal definition of consistency according to the meta-theory. Clearly, the formal definition of consistency meets its common sense interpretation. We illustrate consistency on the top-level specification of Table IX. Referring to this table, we have strengthened R s.6 and R s.7 in some way. Lack of consistency is revealed by checking the mutual consistency of these two requirements with the requirement R g.3 applied to the exit gate. After the following scenario: exit_ticket_insert exit_gate_open exit_ticket_insert event exit_gate_open has modality must in left-hand interface and modality cannot in right-hand interface.

According to the common meaning, an architecture of subsystems, as characterized by their respective specifications, is compatible if these sub-systems "match together", in that they can be composed and the resulting system can interact with the environment as expected-use cases can be operated as wished. As explained in Table IV of Section V, this is the formal definition of compatibility in the meta-theory. Again, the formal definition of compatibility meets its common sense interpretation.

2) Correctness: Correctness can only be defined with reference to another specification. We propose to translate "correctness" by one of the following properties, depending on the case (see Table IV for the notations):

• "is a correct implementation of", written |= M ;

• "is a correct environment of", written |= E ;

• "refines", written .

3) Completeness: Completeness raises a difficulty. Although the term "completeness" speaks for itself, it cannot be formally defined what it means to be complete, for a toplevel specification in the form of a set of requirements. The reason is that we lack a reference against which completeness could be checked. Hence, the only way to inspect a toplevel specification for completeness is to explore it manually. The best help for doing this is to execute the specification. Thus, specifications must be executable. Fortunately, Modal Interfaces are executable and, this way, undesirable behaviors can be revealed. We illustrate this on the top-level specification of Table IX, where R s.6 is changed into "exit gate must open after an exit ticket is inserted" (by omitting "and only then"). Lack of completeness is revealed by simulation. The following scenario can occur: exit_ticket_insert exit_gate_open vehicle_exit exit_gate_close exit_gate_open which allows vehicles to exit without having inserted an exit ticket, an unwanted behavior. This reveals that the specification was not tight enough, i.e., incomplete. So far for completeness of the top-level specification.

In contrast, completeness can be formally defined when a reference C is available. We propose to say that C is incomplete with reference to C, if 1) C does not refine C, but 2) there exists C C such that C is consistent and compatible, and refines C. The rationale for this definition is that C is not precise enough but can be made so by adding some more requirements. Note that C is incomplete with reference to C if and only if C ∧ C is consistent and compatible. This criterion is of particular relevance when C = i∈I C i is an architecture of sub-contracts, where C i is to be submitted to supplier i for independent development.

F. Discussion

Requirements engineering is considered very difficult. Requirements are typically numerous and very difficult to structure. Requirements concern all aspects of the system: function, performance, energy, reliability/safety. Hence, systems engineers generally use several frameworks when expressing requirements. The framework of contracts expressed as Modal Interfaces that we have proposed here improves the situation in a number of aspects:

• It encompasses a large part of the requirements. 52 • It can accommodate different concrete formalisms. In our example, we have blend textual requirements with requirements specified as state machines. Richer formalisms such as Stateflow diagrams can be accommodated in combination with abstract interpretation techniques-this is not developed here. • We have shown how to offer formal support to important properties such as the four C's during the process of certification.

• We have proposed a correct-by-construction approach to the difficult step of moving from the top-level specification in the form of a requirements document, to an architecture of sub-contracts for the suppliers. 53

XII. CONTRACTS IN THE CONTEXT OF AUTOSAR

In this section, we use AUTOSAR as an industrial example of how to leverage contracts within an existing standard to extend it.

A. The AUTOSAR context

AUTOSAR 54 is a world-wide development partnership including almost all players in the automotive domain electronics 52 According to figures that were given to us by industrials, 70-80% of the requirements can be expressed using the style we have developed here. Other requirements typically involve physical characteristics of the system or define the range for some parameters. 53 The framework of Assume/Guarantee contracts that is used in Section XII does not offer this, for two reasons. First, it lacks the quotient and, second, local alphabets are not properly handled. In contrast, Assume/Guarantee contracts are very permissive in how they can be expressed. In particular, dataflow diagrams (Simulink) can be used to express assumptions and guarantees. 54 http://www.autosar.org/ supply chain. It has been created with the purpose of developing an open industry standard for automotive software architectures. To achieve the technical goals of modularity, scalability, transferability and reusability of functions, AU-TOSAR provides a common software infrastructure based on standardized interfaces for the different layers. The AUTOSAR project has focused on the objectives of location independence, standardization of interfaces and portability of code. While these goals are undoubtedly of paramount importance, their achievement may not be sufficient for improving the quality of software systems. As for most other embedded system, car electronics is characterized by functional as well as non functional properties, assumptions and constraints [START_REF] Heinecke | Software Components for Reliable Automotive Systems[END_REF]. Therefore, an AUTOSAR based development process benefits from adding contracts, as the this section will demonstrate.

B. The contract framework

Extensive use of Simulink/Stateflow modeling is performed for system design in the automobile sector. It is thus natural to try reusing this modeling style for defining contracts. Since A/G contracts of Section VII simply rely on specifying assertions regardless of how they are actually described, we use A/G contracts for this AUTOSAR case study. Since Simulink/Stateflow diagrams are very flexible, contracts can be expressed for all viewpoints (function, timing, safety). In turn, reasoning on such contracts is beyond the capability of automatic tools. Consequently, checking for implementation and refinement relations will be performed manually on small models. In contrast, the powerful contract algebra developed in the meta-theory is fully generic and does not depend on the nature and complexity of the considered models. The modularity it offers will thus be the main help offered by contract based design in this case study. As another feature of this this study, the distinction between "horizontal" and "vertical" contracts is used, see Section IV-D4. Finally, the following variation of A/G contracts is used.

Assertions consist of a timed extension of the "weakly synchronous" model [START_REF] Balarin | Specification, synthesis and simulation of transactor processes[END_REF], namely:

P ⊆ ((Σ → D) ∪ R + ) * ∪ ((Σ → D) ∪ R + ) ω (56)
meaning that the assertion proceeds by a succession of steps consisting of either assignment of values to variables (including the special status "absent" for multiple-clocked assertions), or time progress. Composition is by intersection: P 1 ×P 2 = def P 1 ∧ P 2 , with alphabet equalization by inverse projection as in see Section VII-C. Following Section VII-B, components are tuples M = (Σ in , Σ out , P ), where Σ = Σ in ∪ Σ out is the decomposition of alphabet Σ into its inputs and outputs, and P is an assertion following [START_REF] Chakrabarti | Synchronous and Bidirectional Component Interfaces[END_REF]. Components must be free of exception in the sense of Definition 4.

A contract is a tuple C = (Σ in , Σ out ; A s , A w ; G), where Σ = Σ in ∪ Σ out is the decomposition of alphabet Σ into its inputs and outputs. A s and A w , the strong and weak assumptions, and G, the guarantees, are assertions over Σ.

The set E C of the legal environments for C collects all components E such that E ⊆ A. The set M C of all components implementing C is defined by (A s ∧ A w ) × M ⊆ G, meaning that implementations guarantee G under the condition that the environment satisfies the stronger condition A s ∧ A w . In other words, in this framework, legal environments are constrained by strong assumptions only, whereas the conjunction of strong and weak assumptions is required to guarantee G. Weak assumptions are useful for design iterations in case strict obligations for the context of use may not be realizable.

To conclude on this framework, its difference is only methodological since any contract with strong and weak assumptions, C = (Σ in , Σ out ; A s , A w ; G), is equivalent to an ordinary A/G contract (Σ in , Σ out ; A s ; G ∨ ¬A w ). Thus, the reader is referred to Section VII. Adding time to the paradigm does not change anything to the relations or operators defined in that section.

However, adding time results in decidability and complexity issues. The latter problem can be fixed in part by using observers, see Sections V-G and VII. Other proofs can be carried on manually-this is feasible for undecidable properties when the needed reasoning only involves a small part of the analyzed system involving few locally interacting components. The added value of our contract framework is to support the combination of proofs into a validation for the overall system taking into account detailed design decisions captured in system and ECU configurations.

C. Exterior Light Management System

To illustrate the benefits of contract-based systems engineering in AUTOSAR, we consider as an example an excerpt of an Exterior Light Management for an automobile. 55 We focus on the parts responsible for sensing driver inputs and actuating the rear direction indicator lights and brake lights. With this example we show how requirements can be refined to contracts and discuss the added value of contracts for negotiations between OEM and suppliers. We will also illustrate the use of vertical contracts, e.g., to specify the expected latency of the communication solution and computations from the timing viewpoint, and a failure hypothesis in terms of reliability.

1) Function and timing:

We begin our study by showing how AUTOSAR models can be enhanced with contracts. The Virtual Functional Bus model: Figure 16 shows the Virtual Functional Bus (VFB) model encompassing the exterior lights management. This software composition specifies the interfaces exposed by the component to the sensors delivering driver inputs (brake pedal, warn light button, turn signal lever) and to the actuators controlling the lights. Ports with arrowheads denote an asynchronous data flow interface, which is a SenderReceiverInterface. Here it is a special kind called ServiceInterface, which means the data is provided by some local service located in the BasicSoftware stack of an ECU (Electronic Computing Unit). The requirements document of the system contains one timing-related requirement:

• R 1 : If the driver presses the brake pedal, the brake lights must light not later than 25ms. We formalize in Table X this requirement as a contract by using a pattern-based contract specification language (terms in bold-face are keywords). Decomposed VFB Software composition: Figure 17 shows the decomposed VFB model. AssemblySwConnectors link the ports of parts of the composition and are subject to communication refinement. The components used in the composition and their functions are as follows:

• BrakePedalSensor receives the position of the brake pedal (ext_pedal) and distributes it to other components.

• PedalToLamp reads the brake pedal position (pos_pedal) and calculates requested brightness of the brake indicator lights (lamp_intensity). • BrakeLampActuator reads the requested brightness of the brake indicator lights (lamp_intensity) and actuates the brake lamps accordingly (ext_lamp). • TurnSwitchSensor reads the position of the lever and forwards it (tss). • WarnLightsSensor reads status of the warn blink button and forwards it (wls). • Indicator reads the status of the warn blink button, the lever position and cyclically toggles the left and right signals (rla_signal, rra_signal). • Rear(Left|Right)Actuator reads its input signal ((rla|rra)_signal) and actuates the bulb (ext_(rla|rra)). provided that the pedal is not "multiply pressed", then the pos_pedal message traverses the BrakePedalSensor, and then the wire following it, with some unspecified delay. In particular, no message is lost due to a miss by this block. Similar contracts are stated for all blocks of the VFB model, thus resulting in a set C f IO of contracts. For all AssemblySwConnectors of the composition, horizontal contracts are specified that are similar to that of C f SIGNALBPS , resulting in a set C f SIGNAL of contracts. This contract scheme guarantees a reliable data transport by each wire of the VFB model, no matter how the communication is refined. So far we have stated contracts for each block and each wire of the VFB model. Compose the above contracts using contract composition [START_REF] Baier | Principles of Model Checking[END_REF], i.e., compute

C f VFB = {C | C ∈ C f IO } {C | C ∈ C f SIGNAL } (57)
RR n°8147

The guarantee offered by overall contract C f VFB is the conjunction of the guarantees of the constitutive contracts. Hence, contract C f VFB guarantees that messages reliably traverse the VFB model with, however, an unspecified delay. On the other hand, contract composition [START_REF] Baier | Principles of Model Checking[END_REF] assumes the conjunction of all assumptions stated for each block-the guarantee offered by C f VFB and the strong assumption of C R1 discharge all of these assumptions.

At this point, we observe that contract C f VFB involves no timing characteristics and, thus, functional contract C f VFB does not refine the initial contract C R1 . To overcome this, timing contracts are added in the next step, that will complement this functional contract with timing viewpoint based on expected performance characteristics of the computing platform.

Budgeting time using contracts: We now state additional contracts such as the ones shown in Table XII. Observe that, for those contracts weak assumptions are used, see Section XII-B regarding the motivations for doing this. Observe also that we repeated the functional strong assumption. 56 Again, stating similar contracts for each block and wire of the

= ( {C | C ∈ C t IO }) ( {C | C ∈ C t SIGNAL }) (58)
The next step is to combine, for each component (block or wire) of the VFB model, the two functional and timing viewpoints using conjunction, i.e., to compute

C VFB = C f ∧ C t | (C f , C t ) ∈ C IO C f ∧ C t | (C f , C t ) ∈ C SIGNAL (59)
where C IO collects, for each block, the pair of functional and timing contracts associated with it, and similarly for C SIGNAL . 56 If we do not do this, then, when taking the conjunction of functional and timing contracts, the functional strong assumption gets absorbed by the strong assumption of the timing contract, since the latter is equal to T. See the discussion regarding Assume/Guarantee contracts with variable alphabets at the end of Section VII-C.

At this point, we observe that the architecture of the VFB model is a directed acyclic graph.

Consider the conjunction C = C f ∧ C t = (A, G) for each block or wire. As an example, focus on block IO BPS , which is the first block of VFB, seen as a directed acyclic graph. Regarding the combination of strong and weak assumptions, we have A = A f s ∧ A t w , which is weaker than A s , the assumption of C R1 in Table X. Regarding guarantees, we have G = G f ∧ G t , which ensures that messages traverse the component without duplication or loss and with a delay less than the "minperiod" of the input signal (15ms). Also, guarantee G offered by this block is strong enough to discharge the assumption of the next wire when performing contract composition. Reproducing the same reasoning, inductively, along all blocks and wires of the VFB model seen as an acyclic graph, shows that

C VFB C R1 (60)
Consequently, submitting the pairs of contracts (C f , C t ) associated to each component for separate development, possibly by different suppliers, will ensure correct integration (provided implementations by the suppliers are correct with respect to their contracts). In particular, the component BrakePedalSensor belongs to the chassis domain and is implemented by a different supplier than the other components.

Discussion: The above step of our contract based design methodology leads to the following important notices:

1) So far our proof steps were all manual. Our contract based reasoning, however, was instrumental in ensuring that elementary proof steps were combined correctly. Reasoning based on intuition when component composition and viewpoint combination both occur is very likely to lead to wrong conclusions. There is a strong added value in contract based reasoning even if elementary proof steps are manual.

2) Manual reasoning can be complemented by the use of observers. Again, it is important that the use of observers when component composition and viewpoint combination both occur is performed correctly. Our development in Section V-G provides the formal support for this. For the pattern based language used here, a framework for checking refinement of contracts using an observer based strategy is described in [START_REF] Gezgin | A Refinement Checking Technique for Contract-Based Architecture Designs[END_REF].

3) The responsibility of establishing the sub-contracts submitted to the different suppliers is assigned to the OEM, in accordance with his role as integrator. Components belonging to different domains of a car (engine, chassis, etc.) are likely to originate from different vendors/suppliers. By using our above reasoning, the OEM can decompose its contract specifications, passing them to supplier(s). For example, the component BrakePedalSensor is the only one in the VFB model that belongs to the chassis domain and other components are developed by one or more different suppliers. Thus, in decomposition ( 59), the two sets of contracts C IO and C SIGNAL are partitioned, e.g., for subcontracting to two different suppliers:

C supplier 1 VFB = C f ∧ C t | (C f , C t ) ∈ C 1 IO C f ∧ C t | (C f , C t ) ∈ C 1 SIGNAL C supplier 2 VFB = C f ∧ C t | (C f , C t ) ∈ C 2 IO C f ∧ C t | (C f , C t ) ∈ C 2

SIGNAL

Each supplier can then safely develop its own sub-system, independently. We develop this in the next sub-section. Implementation of software components and vertical assumptions: Each of the software components being part of the software system composition (cf. Figure 17) is a Compo-sitionSoftwareComponents, as this allows the supplier to reuse already designed components. We thus consider one such component with its contract C = C f ∧ C t consisting of the functional contract C f , in conjunction with the timing contract C t . The supplier can then follow two different approaches for developing this component.

In a first approach, the supplier reuses a composition

C = i∈I C i (61)
of off-the-shelf components available from a library. Two situations can then occur:

• The easy case is when refinement holds: C C. This means that, for C = ( A s , A w , G), guarantees are strong enough and assumptions are weak enough to imply refinement with respect to the contract C specified by the OEM.

• A more realistic (but also more delicate) case is when the following weaker relations are satisfied:

C C f (62) G ⊆ G (63) A s ∧ A w ⊇ A f s ∧ A f w (64)
but the conditions requested on timing assumptions for refinement C C to hold are not satisfied:

A s ∧ A w ⊇ A t s ∧ A t w (65)
Under [START_REF] Damm | Boosting reuse of embedded automotive applications through rich components[END_REF], composition from library C cannot be used as such. It can, however, still be used as a valid implementation provided that some additional missing vertical assumption regarding timing is stated, such that:

A s ∧ A w ⊇ A t s ∧ A t w ∧ A t w for negotiation (66)
(66) requires a negotiation in which additional vertical assumption A t w is returned back to the OEM as an additional performance requirement for the ECU platform. If this is accepted by the OEM, then development by the supplier using off-the-shelf components from the library (61) can proceed. The alternative approach is to implement the component. Eventually, this results in a composition of AtomicSoftwareComponents. This component type has an internal behavior specification comprising so called Runnables, which are the smallest executable entities known to AUTOSAR. For each runnable, activation conditions are defined by means of RTEEvents controlled by the RuntimeEnvironment on the corresponding ECU, and data accesses referring ports of the owning component. An RTEEvent can be configured to occur either cyclically (timetriggered) or by the data arrival on some input port of the owning component (event-triggered).

Figure 18 depicts the internal behavior of component

BrakePedalSensor. [START_REF] Clarke | Compositional model checking[END_REF][START_REF] Damm | Using Contract-Based Component Specifications for Virtual Integration and Architecture Design[END_REF][START_REF] Damm | LSCs: Breathing life into message sequence charts[END_REF][START_REF] Damm | Boosting reuse of embedded automotive applications through rich components[END_REF] hold. However, strengthening an assumption is not a refinement. Therefore, applying this modification cannot be performed by the supplier on its own but rather requires negotiation with the OEM. If the OEM is willing to accept the stronger assumption A t w , the component from the libary can be used and the modified contract of the supplier is refined: C C supplier 1 VFB . The next process steps in the AUTOSAR methodology, called System configuration and ECU configuration define the target architecture (ECUs and communication network) as well as the deployment of the application software components on that distributed architecture. Thus, satisfaction of the contracts specified for the application needs to be verified for the given architecture and deployment (cf. IV-D4). We develop this in the next two sub-sections.

This component consists of a single

ECU configuration and vertical contracts: During the following discussion we assume that for each component implementation a contract similar to C has been specified and possibly an associated A t w has been negotiated. Observe, that A t w may invalidate refinement of system requirements by the VFB contract. Consider the example above. A t w assumes an activation of BPSRunnable each 10ms and a worst case response time less than 5ms. This additional weak assumption is now part of C supplier 1 VFB . However, it is neither discharged by any guarantee of C VFB , nor by the strong assumption of C R1 . Thus, we need to verify that 1/ all vertical assumptions collected during previous steps are discharged during systemand ECU configuration and 2/ all guarantees are met by software components and connectors. For both tasks state-ofthe-art verification techniques can be used.

As an example, focus on the vertical assumption A t w of the BrakePedalSensor-component and consider the ECU configuration depicted in Figure 19. The ECU hosts the two components BrakePedalSensor and PedalToLamp of the VFB model 57 . These components are integrated with a layered basic software stack on an ECU. That stack consists of multiple BasicSoftwareModules (BSWM). Each of these modules has a set of standardized interfaces and is implemented by a set 57 To simplify, we omit port emcyBrake of BswModuleEntities. These are analogous to the Runnables of application software components and are either executed by a dedicated OS task or interrupt service routine. Therefore, we expect BasicSoftwareModules to be characterized by contracts in a way similar to the internal behavior of application components (cf. contracts in Table XIII). In case a BSWM has a BswModuleEntity that is not mapped to some task or interrupt service routine, that entity is an "ordinary" function called within the context of another BswModuleEntity or Runnable. In the example ECU configuration two BSWMs are shown:

• A ComplexDeviceDriver, which has direct access to the sensor of the ECU that detects position of the brake pedal. • An AUTOSAR COM module and a CAN interface (not shown here).

The components and BSWMs own a single runnable each, bsw entity respectively. The ECU configuration maps BP-SRunnable to task t1 of the operating system (OS) and PTL-Runnable to task t2. The BswModuleEntity of the ComplexDe-viceDriver is mapped to an interrupt service routine, while the entity of the COM module is simply a function for sending a signal. That function is used by the AUTOSAR runtime environment (RTE) to realize the communication specified on VFB-level by means of the connectors. For each task of the OS the ECU configuration specifies at least its priority and wether it is preemptable. The activation of a task is specified by linking an alarm of the OS to that task. Those alarms can also be configured to occur cyclically. For each cyclic alarm we generate a contract P ALARMi , with trivial strong and weak assumptions and as guarantee the cycle time of the alarm. The example ECU configuration contains a single alarm, whose contract is listed in we can extract from the AUTOSAR model of the component implementation a set of execution time specifications for each Runnable owned by the component. Again, the same applies to BswModuleEntities. With this information we can create a task network and obtain response times for each Runnable and BswModuleEntity (if executed by some task or interrupt service routine) using tools like SymTA/S 58 or chronVAL 59 . Afterwards, we generate for each Runnable and BswModuleEntity (if executed by task or ISR) a contract P Runnablei , with stong and weak assumption T and as guarantee the reponse time interval determined by analysis. For the ECU configuration sketched in Figure 19, BPSRunnable has a response time that lies in the interval [1ms, 4ms], resulting in the contract shown in Table XIV, bottom. Similar contracts are stated for all tasks and alarms extracted from the ECU configurations. We then compose these contracts and the contracts of the BSWMs, which yields the contract P characterizing the execution platform. Following the approach outlined in Section IV-D4 we compose the VFB contract with the platform contract and check for refinement, i.e.

C VFB ⊗ P C VFB (67)
The vertical assumption A t w is discharged in the composition of the VFB and platform contracts and refinement holds. Furthermore, with A t w being discharged refinement of the system requirement holds again:

C VFB ⊗ P C R1 (68)
The approach outlined here to analyze the mapping of application software components and their associated contracts on an ECU network by creating contracts from ECU configurations and results of response time analysis, has been implemented in a framework. That framework includes a meta-model supporting contract-based design and enables to 1/ specify contracts for components in foreign models and 2/ check for refinement between contracts belonging to different models [START_REF] Baumgart | Architecture Modeling[END_REF].

Inter-ECU communication: During system configuration the leaves of the hierarchical software composition called AtomicSoftwareComponents are mapped to ECUs of the target architecture. Thus, we know for each connector of the VFB model, whether it must be implemented by the communication network interconnecting the ECUs.

For both, intra-and inter-ECU communication the design must be verified against the corresponding contracts of the VFB model, i.e. the set of contracts

C f ∧ C t (C f , C t ) ∈ C SIGNAL (69)
Again, available analysis techniques can be used. Suppose, a signal from the VFB model is mapped to a frame transmitted on a CAN bus. The OEM can then for each such contract use the combination of strong and weak assumptions A = A f s ∧ A t w as specification of the minimal inter-arrival times of subsequent occurrences of the signal. Taking into account 58 http://www.symtavision.com/symtas.html 59 http://www.inchron.com/chronval.html the priority of each CAN frame given by its identifier, the response time of each signal can be computed and compared against the guarantee G = G f ∧ G t .

If the communication network, whose configuration is part of the AUTOSAR system configuration, is successfully verified against the contracts defined in [START_REF] David | ECDAR: An Environment for Compositional Design and Analysis of Real Time Systems[END_REF], deployment of the VFB model on the target architecture is correct with regard to the VFB contract and the design fulfills the initial system requirement C R1 . Discussion: The above development highlights the methodological value of contracts for system design in AU-TOSAR context at later design stages. First, both contract conjunction and composition are used. Then, modifications that are not refinements are pinpointed, which forces the supplier to engage on a negotiation with the OEM regarding system specifications. Without the solid support of contracts and its rules, such kind of reasoning would be error prone.

2) Safety: The virtual function bus (VFB) concept was intended to enable a distributed development of software components independently from the underlying hardware architecture. The specification of the interfaces in the 3.x releases did not support the kind of non functional property necessary to develop safety aspects of critical systems. This fact lead to the development of the previously mentioned Timing Extension and Safety Extension to Methodology and Templates. The safety extension directly addresses the use of contracts for the specification of safety relevant properties driven by the need for compliance to the upcoming ISO26262 standard. The ISO26262 not only requires comprehensive checking of requirements but also states explicitly the need for using assumptions on the environment to develop a safety relevant element on the supplier side ("safety element out of context"). In particular the standard distinguishes between:

• A functional safety concept comprising the functional safety requirements, their allocation to architectural elements, and their interaction necessary to achieve the safety goals. This is used to demonstrate that the risks related to an item of a vehicle are addressed by an adequate functional architecture. • A technical safety concept used to demonstrate that the functional safety concept is addressed by an adequate technical solution. As a simple example for this approach we take the functional architecture of Figure 20 showing the decomposition of the SafeBrakeIndication function into the "normal" BrakeIndication function and the SignalingFailureDetection safety function in case the BrakeIndication fails. The corresponding safety goal requires that a loss of the braking indication function shall be detected. This is formalized as contract C S0 , shown in Table XV. This contract states that under a given failure hypothesis ("no double failure") either the brake lamp is activated or the driver is warned by the SignalingFailureDetection function. This contract is attached to the function SafeBrakeIndication.

For the subfunction BrakeIndication we show in

Table XVIII HORIZONTAL CONTRACT FOR SAFETY FUNCTION FOR BRAKING LAMP

The nominal behavior is again given by the contract with an assumption about the absence of the communication failure, see Table XIX.

Similarly, the error state of the BreakLampActuator is caused by a failure on the second communication link (fail(lamp_intensity)) or by a failure propagated from the PedalTo-Lamp component, see

Table XXI CONTRACT STATING THE TECHNICAL SAFETY REQUIREMENT

Contract C S8 is directly related to the functional safety goal and includes the allocation to a technical safety concept. This way a consistency between the functional and the technical safety concept has been established. Furthermore, thanks to the formal pattern-based specification language, the refinement relations ensure that the concepts themselves are correct.

To conclude, let us mention other safety related use-cases which benefit from contract based specification such as the automatic generation of fault-trees or FMEA tables as well as the safe-state management.

D. Integrating Contracts in AUTOSAR

An important challenge is to smoothly integrate the use of contracts as part of AUTOSAR methodology. We advocate a migration in two steps.

Today-Offering a Smooth Integration of Contract-Based System Engineering with AUTOSAR: The metamodel underlying the CESAR reference technology platform has been carefully designed to support a seamless design flow from the derivation of high-level requirements of new automotive functions to the level of detailed application design defined as the entry point in the AUTOSAR design methodology. The key for this smooth integration has been laid by AUTOSAR itself, by enforcing a clean separation between application development on the one side, and deployment to distributed target architectures on the other side. Regarding layered design, the joint scope of CESAR and AUTOSAR ranges from systemsof-systems levels for Car2X applications, to the introduction of new automotive functions, and down to the detailed design level. As illustrated in the previous section, such phases would build on established design processes and currently used design tools, where contracts and viewpoints are conservatively added as additional flavor to existing design methodologies. Full hand-over to AUTOSAR takes place at the detailed design stage, where component contracts get implemented using the AUTOSAR component model, thus providing the entry point for the AUTOSAR design methodology.

Following the AUTOSAR flow, system configurations and ECU configurations describe the detailed target hardware. We can then automatically extract from system and ECU configurations all information for performing real-time analysis. Vertical assumptions on the component level can be derived by back-annotation from the underlying target hardware. Alternatively, vertical assumptions can be seen as constraining the target architecture (regarding its timing characteristics) and can thus be used to constrain the design space for possible target architectures. Finally, when deploying components to ECUs, communications of the virtual functional bus are mapped to the inter-component communications on the physical architecture.

The Future-Integrating Contracts in AUTOSAR: The current AUTOSAR release is expressive enough to represent realtime contracts. Using the concept of timing chains, both endto-end deadlines as well as assumed response times for component execution and communication can be expressed. However, the current release was not designed for extensibility: there is no established notion of viewpoints and, hence, no anchor to easily migrate from the current setting to one supporting multiple viewpoints. As pointed out before, the decision as to which viewpoints should or should not be anchored is a business decision. However, given that ISO 26262 has become binding, we see the need for a systematic integration of the safety viewpoint.

In fact, a safety extension has already been proposed for inclusion in AUTOSAR. It allows to use contracts for the encapsulation of Basic SoftWare (BSW) modules, application software components, entities of the hardware architecture (like ECUs and buses) and the characterization of communication services. Such encapsulation would, for instance, distinguish between BSW modules that (1) contribute to safety ("safety mechanisms") and (2) those that could potentially impact system's safety (by providing their failure propagation behavior). A typical example for (1) would be the function inhibition manager that maintains function inhibitions whenever, for instance, implausible outputs are generated. A typical example for (2) would be an error that occurs in the communication services or an error that is generated in communication H/W that impacts communication services.

The objective of the extension is to provide an ISO 26262 compliant traceability. This allows, for instance, to deal with compliance between functional safety (where functions, hazards and safety functions are collected in the functional RR n°8147 model) and technical safety of the AUTOSAR architecture instance (guaranteeing that the AUTOSAR implementationusing given safety functions of the AUTOSAR architectureindeed implements the identified functional safety concept).

Since timing and safety viewpoints will be supported in AUTOSAR it is at least worthwhile to consider introducing the concepts of viewpoints systematically. Doing so will ease their activation at times when other market factors such as power-management mandate their introduction.

E. Summary and discussion

We have proposed a smooth path for integrating contracts in the context of AUTOSAR at the level of detailed design. We believe that the main aspects for consideration while introducing contracts are the handling of time budgets and the specification of failure modes and failure propagation, in combination with the functional aspect itself. Vertical contracts were instrumental in handling time budgets. Such contracts relate two different layers of the AUTOSAR framework.

XIII. CONCLUSION

This paper presented past and recent results as well as novel advances in the area of contracts and their theory. By encompassing (functional and non-functional) behaviors, the notion of contract we considered here represents a significant step beyond the one originally developed in the software engineering community.

A. What contracts can do for the designer

This paper demonstrates that contracts offer a number of advantages:

Contracts offer a technical support to legal customersupplier documents: Concurrent development-both within and across companies-calls for smooth coordination and integration of the different design activities. Properly defining and specifying the different concurrent design tasks is and remains a central difficulty. Obligations must therefore be agreed upon, together with suspensive conditions, seen as legal documents. By clearly establishing responsibilities, our formalization of contracts constitutes the technical counterpart of such legal documents. Contracts are an enabling technology for concurrent development.

Contracts offer support to certification: By providing formal arguments that can assess and guarantee the quality of a design throughout all design phases (including early requirements capture), contracts offer support for certification. By providing sophisticated tools in support of modularity, reuse in certification is made easier.

Contracts comply with formal and semi-formal approaches: The need for being "completely formal" has hampered for a long time formal verification in many industrial sectors, in which flexibility and intuitive expression in documentation, simulation and testing, were and remain preferred. As the AUTOSAR use case of Section XII demonstrated, using contracts makes semi-formal design safer. Small analysis steps are within the reach of human reasoning. A valid, system wide, analysis for both component-based and refinement-based designs is typically beyond the reach of human reasoning. Contract based design enables it.

Contracts improve requirement engineering: As illustrated in the Parking Garage example of Section XI, contracts are instrumental in decoupling top-level system architecture from the architecture used for sub-contracting to suppliers. Formal support is critical in choosing alternative solutions and migrating between different architectures with relatively small effort. Of course, contracts are not the only important technology for requirements engineering-traceability is essential and developing domain specific ontologies is also important.

Contracts can be used in any design process: Contracts offer a "orthogonal" support for all methodologies and can be used in any flow as a supporting technology in composing and refining designs.

B. Status of research

The area of contracts benefits from many advances in research that were not targeted to it. Interface theories were developed by the community of game theory-component and environment are seen as two players in a game. Modalities aimed to offer more expressive logics were born at the boundary between logics and formal verification. Contracts as a philosophy originated both from software engineering and formal verification communities, with the paradigms of Pre-condition/Post-condition or Assume/Guarantee. It is not until the 2000's that the concept of contracts presented here as a tool to support system design emerged. In this evolution, various formalisms and theories were borrowed to develop a rigorous framework. This paper was intended to show the power of a unified theoretical background for contracts, the use of contracts in present methodologies and the challenges for its effective applications in future applications. The mathematical elegance of the concepts underpinning this area provides confidence in a sustained continuation of the research effort.

C. Status of practice

The use of contract-based techniques in system design is in its infancy in industry. Further maturation is needed for its paradigm and concepts to become, on one side, clear and simple to be widely accepted by engineers in their dayto-day work and, on the other side, developed enough to allow for the development of tools for automatic verification and synthesis. While powerful contract-based proof-of-concept tools are being experimented-some of them were presented in this paper-the robustness of the tools and the underlying techniques is still weak, and contract-based design flows and methodologies are not yet fully developed nor mature.

D. The way forward

The ability of contracts to accommodate semi-formal and formal methodologies should enable a smooth and rapid migration from theory and proof-of-concepts to robust flows and methodologies. The need for jointly developing new systems while considering issues of intellectual property will make RR n°8147 it attractive to rely on contracts in supplier chains. In our opinion, contracts are primarily helpful for early stages of system design and particularly requirement engineering, where formal methods are desperately needed to support distributed and concurrent development by independent actors.

We have illustrated in this paper how suppliers can be given sub-contracts that are correct by construction and can be automatically generated from top-level specification. We believe, however, that the semi-assisted/semi-manual use of contracts such as exemplified by our AUTOSAR case study is already a significant help, useful for requirements engineering too. Altogether, a contract engine (such as the MICA tool presented in Section XI) can be used in combination with both manual reasoning and dedicated formal verification engines (e.g., for targeting the timing viewpoint or the safety viewpoint) as the basis for future development that will make contracts main stream.

Figure 2 .

 2 Figure 2. System architecture as specified by the designer.

Figure 4 .

 4 Figure 4. Stepwise refinement

Figure 5 .

 5 Figure 5. Conjunction for component reuse

63 Figure 6 .

 636 Figure 6. Mapping the application to the execution platform as C ∧ P.

63 and x d 63

 63 are related by some buffer of bounded size. The deployment is then captured by synchronizing x o 63 with the output x o 63 of the module implementing M 6 in the right computing unit, and by synchronizing x d 63 with the input x d 63 of the module implementing M 3 in the left computing unit.

  1 is in force; Properties 3, 4, and 5 hold Say that C 1 and C 2 are compatible if so is C 1 ⊗C 2 How composition is expressed and computed Quotient C 1 /C 2 = { C | C ⊗ C 2 C 1 }; Property 6 holds How quotient is expressed and computed

Definition 3 :

 3 A contract is a pair C = (A, G) of assertions, called the assumptions and the guarantees. The set E C of the legal environments for C collects all components E such that E ⊆ A. The set M C of all components implementing C is defined by A × M ⊆ G. Thus, any component M such that M ≤ G ∨ ¬A is an implementation of C and M C = G ∨ ¬A is the maximal implementation. Observe that two contracts C and C with identical input and output alphabets, identical assumptions, and such that G ∨ ¬A = G ∨ ¬A, possess identical sets of implementations: M C = M C . According to our meta-theory, such two contracts are equivalent. Any contract C = (A, G) is equivalent to a contract in saturated form (A, G ) such that G ⊇ ¬A, or, equivalently, G ∨ A = T, the true assertion; to exhibit G , just take G = G ∨ ¬A. A saturated contract C = (A, G) is consistent if and only if G = ∅ and compatible if and only if A = ∅.

  • b M C (M ) is performed by drawing non-deterministically a behavior σ of M and then evaluating b A (σ) ⇒ b M (σ).

Figure 8 .

 8 Figure 8. Translating the guarantee R g.3 of gate as an i/o-automaton (top) and then as a Modal Interface G gate (bottom) using Rules 1.

Figure 9 .

 9 Figure 9. Translating the assumptions of gate as a Modal Interface A gate using Rules 2. 1: translation of R g.1 ; 2: translation of R g.2 ; 3: the resulting conjunction; 4: the final result after applying rule R A 3 and renaming the states.

Figure 10 .

 10 Figure 10. Chapter gate of the top-level requirements document translated into a Modal Interface C gate .

Figure 15 .

 15 Figure 15. The three restrictions of the global contract C for the three subsystems EntryGate (top), ExitGate (mid), and PaymentMachine (bottom).

Figure 16 .

 16 Figure 16. Virtual Functional Bus model

Figure 19 .

 19 Figure 19. Extracting platform contracts from ECU configuration

Figure 20 .Figure 21 .

 2021 Figure 20. Functional architecture including safety function

Figure 22 .

 22 Figure 22. The role of Faults, Errors, and failures For instance, the contract C S4 of Table XVIII states that the error state of the PedalToLamp component is caused by a failure in the communication.

C S 4 :

 4 As true Aw true G Mode PedalToLampError is caused by fail(pos_pedal).

C S 8 :

 8 As true Aw only one of faila failb failc G Whenever ext_pedal occurs then ext_lamp or ext_indication occurs.

  Since is a pre-order, refinement is a transitive relation. For our current series of examples, and using previous notations, C C amounts to requiring that 1/ A C implies A C , and 2/ A C ⇒G C implies A C ⇒G C .

different design teams and refined further independently. In particular, C 12 is further decomposed into contracts C 121 and C 122 such that C 121 ⊗ C 122 C 12 , and similarly, C 13 is further decomposed into contracts C 131 and C 132 such that C 131 ⊗ C 132 C 13 .

  [START_REF] Antonik | 20 Years of Modal and Mixed Specifications[END_REF] , C 12 and C 13 , with the property that C 11 ⊗C 12 ⊗C 13 C 1 . Now, these three contracts can be handed to

  The contract C 1 formalizes the most crude and abstract requirements for a divider. It requires that the denominator value (input variable y) is not equal to 0, and only ensures that the output value of z is any real. Note that the contract C 1 does not declare the nominator input variable x. The contract C 2 specifies components that have an input variable x and an output variable of type y. The only requirement on the behavior of C 2 is that y is strictly greater than 0. The composition C 1 ⊗ C 2 is well defined. The contract C 1 refines C 1 , since it allows more inputs (the nominator input variable x) and restricts the behavior of the output variable z, by defining its behavior as the division x/y. It follows that C 1 is also compatible with C 2 and thatC 1 ⊗ C 2 C 1 ⊗ C 2 .Finally, we have that M 1 and M 2 are implementations of their respective contracts. It follows that M 1

		variables:	inputs: x outputs: y
		types: x, y ∈ R
		assumptions: T
		guarantees: y > 0

  . Requirement R g.1 is best described

	gate
	R g.1 :"vehicles shall not pass when gate is closed", see Fig. 7
	R g.2 : after ?vehicle_pass ?vehicle_pass is forbidden
	R g.3 : after !gate_open !gate_open is forbidden and
		after !gate_close !gate_close is forbidden
	payment
	supervisor
			Table III
	THE TOP-LEVEL SPECIFICATION, WITH CHAPTER gate EXPANDED;
	REQUIREMENTS WRITTEN IN italics ARE ASSUMPTIONS UNDER WHICH
		gate SHOULD OPERATE.
			?vehicle_pass
		!gate_close	!gate_open
		0	!gate_open !gate_close	1
	Figure 1.	Requirement R g.1 specified as an i/o-automaton. Prefix "?"
	indicates an input and prefix "!" indicates an output.

  ×M 2 is well defined if and only if M 1 and M 2 are composable; It is required that × is associative and commutative The definition of the composition Environment An environment for component M is a component E such that E×M is defined and closed Derived Contract A contract is a pair C = (E C , M C ), where M C is a subset of components and E C a subset of legal environments

	Concept	Definition and generic properties		What depends on the particular theory of contracts
	Primitive
	Component	Components are denoted by M ; they can be open or closed	How components are specified
	Composability of components	A type property on pairs of components (M 1 , M 2 )		How this type property is defined
	Composition of components	M 1 Which family C of contracts
					can be expressed, and
					how they are expressed;
					unless otherwise specified,
					quantifying is implicitly over C ∈ C
	Consistency	C is consistent iff it has at least one component: M C = ∅	How consistency is checked
				holds	How refinement is checked
	GLB and	C 1 ∧C 2 =	Greatest Lower Bound (GLB) for	we assume GLB exist	Whether and how
	LUB	C 1 ∨C 2 =	Least Upper Bound (LUB) for	we assume LUB exist	GLB and LUB can be
	of contracts		Property 2 holds		expressed and computed
	Composition
	of contracts

Compatibility

C is compatible iff it has at least one environment:

E C = ∅ How compatibility is checked Implementation M |= M C if and only if M ∈ M C E |= E C if and only if E ∈ E C How implementation is checked Refinement C C iff E C ⊇ E C and M C ⊆ M C ; Property 1

  C 1 ∧C 2 of two Modal

	Interfaces is only defined if Σ in 1 = Σ in 2 and Σ out 1	= Σ out 2

43

Pre-conjunction was originally denoted by the symbol & in

[START_REF] Raclet | Residual for Component Specifications[END_REF]

,

[START_REF] Raclet | Why are modalities good for interface theories?[END_REF]

,

[START_REF] Raclet | A modal interface theory for component-based design[END_REF]

.

  Table VII, compare with Table VI. Observe that the states of the restriction correspond to sets of states of the original Modal Interface. The restriction aims at avoiding incompatibilities when considering the composition, as the following lemma shows: Lemma 11: If C and C ↓Σ are both consistent, then so is their compatible quotient C/ /C ↓Σ , see Definition 12. Proof: Consider two alphabets Σ ⊇ Σ , and a consistent C on alphabet Σ, such that C ↓Σ is also consistent. The only case where quotient produces inconsistent states is whenever there input: C, Σ, Σ ; output: C

	let proj(Op, X) =
	if X has not been visited,
	then
	1. mark X visited
	2. for every α ∈ Σ do
	2.1 let

  R g.1 :"vehicles shall not pass when gate is closed", see Fig.7R g.2 : after ?vehicle_pass ?vehicle_pass is forbidden R g.3 : after !gate_open !gate_open is forbidden and after !gate_close !gate_close is forbidden payment supervisor Table VIII THE TOP-LEVEL SPECIFICATION, WITH CHAPTER gate EXPANDED; REQUIREMENTS WRITTEN IN italics ARE ASSUMPTIONS UNDER WHICH gate SHOULD OPERATE.

		?vehicle_pass
	!gate_close	!gate_open
	!gate_open !gate_close	1

Figure 7. Requirement R g.1 specified as an i/o-automaton. Prefix "?" indicates an input and prefix "!" indicates an output.

gate

  where x ∈{entry, exit} R g.1 (x): "vehicles shall not pass when x_gate is closed", see Fig. 7 R g.2 (x): after ?vehicle_pass ?vehicle_pass is forbidden R g.3 : after !x_gate_open !x_gate_open is forbidden and after !x_gate_close !x_gate_close is forbidden payment R p.1 : "user inserts a coin every time a ticket is inserted and only then", Fig. omitted R p.2 : "user may insert a ticket only initially or after an exit ticket has been issued", Fig. omitted R p.3 : "exit ticket is issued after ticket is inserted and payment is made and only then", Fig. omitted : "at most one ticket is issued per vehicle entering the parking and tickets can be issued only if requested and ticket is issued only if the parking is not full", see Fig 12 R s.4 : "when the entry gate is closed, the entry gate may not open unless a ticket has been issued", Fig. omitted R s.5 : "the entry gate must open when a ticket is issued", Fig. omitted R s.6 : "exit gate must open after an exit ticket is inserted and only then", Fig. omitted R s.7 : "exit gate closes only after vehicle has exited parking", Fig. omitted

	supervisor
		R g.1 (entry)
		R g.1 (exit)
		R g.2 (entry)
		R g.2 (exit)
		R s.1 :	initially and after !entry_gate close !entry_gate open is forbidden
		R s.2 :	after !ticket_issued !entry_gate open must be enabled
		R s.3 Table IX
					REQUIREMENTS FOR THE TOP-LEVEL
						?vehicle_pass
						!gate_close
						!gate_open
				?vehicle_pass	?vehicle_pass	1
	0	!gate_open !gate_close	2	?vehicle_pass	3
			!gate_close

• Regarding the context of operation: Legal inputs to the gate (e.g., vehicle_through when exiting state "1") have a must modality. This complies with the intuition that RR n°8147 gate(x)

  For the decomposed VFB model we derive horizontal contracts specifying the desired I/O behavior of the parts. As an example, for the component BrakePedalSensor, we state the contracts shown in TableXI. Contract C f IOBPS specifies that,

	• SwitchLightActuator	reads left and right signals
	((rla|rra)_signal) and provides feedback on the dashboard.
	Horizontal (functional) contracts associated to the VFB
	model: C f IO BPS	:	A f s A f w	whenever ext_pedal occurs ext_pedal does not occur during [ext_pedal,pos_pedal_out]. true
			G f	whenever ext_pedal occurs
				pos_pedal_out occurs.
			A f s	whenever pos_pedal_out occurs
				pos_pedal_out does not occur during
	C f SIGNAL BPS	:	A f w	[pos_pedal_out,pos_pedal_in]. true
			G f	whenever pos_pedal_out occurs
				pos_pedal_in occurs.
				Table XI
	A SAMPLE OF THE HORIZONTAL CONTRACTS OF THE DECOMPOSED VFB

MODEL; SUPERSCRIPT f REFERS TO "FUNCTION".

  the brake pedal on its provided Sender/Receiver port. The timing behavior of the component owning a timetriggered runnable can be characterized by the contract shown in Table XIII, top.We now focus on the second situation in which the supplier wants to reuse components from a library to implement contractC = C f IOBPS ∧ C t IOBPS .We consider the case where a component BrakePedalSensor has already been implemented and characterized by C = C f IBBPS ∧ C t IBBPS Now, observe that relation (62) holds. However, G ⊆ G. Taking a closer look at A t w , we see it assumes a worst case response time for BPSRunnable. Thus, the guarantee G t can be strengthened if weak assumption A t w is replaced by A t w ensuring a shorter response time. The supplier would then consider the contract C = C f IBBPS ∧ C t IBBPS , where the re-adjusted contract C t IBBPS corresponds to assuming A t w and guaranteeing G t . For that modified contract, relations

				BrakePedalSensor
				BPSRunnable
			ext_pedal	pos_pedal_out
				P=10ms
	Figure 18. Internal behavior of BrakePedalSensor-component
			A f s	whenever ext_pedal occurs
				ext_pedal does not occur during
	C f IB BPS	:	A f w	[ext_pedal,pos_pedal_out]. true
			G f	whenever ext_pedal occurs
				pos_pedal_out occurs.
			A t s	whenever ext_pedal occurs
				ext_pedal does not occur during
				[ext_pedal,pos_pedal_out].
			A t w	ext_pedal occurs sporadic
	C t IB BPS	:		with minperiod 10ms. BPSRunnable#act occurs each 10ms.
				delay between BPSRunnable#act and
				pos_pedal_out within [0ms,10ms].
			G t	delay between ext_pedal and
				pos_pedal_out within [0ms,10ms + 10ms].
			A t s	whenever ext_pedal occurs
				ext_pedal does not occur during
				[ext_pedal,pos_pedal_out].
			A t w	ext_pedal occurs sporadic
	C t IB BPS	:		with minperiod 10ms. BPSRunnable#act occurs each 10ms.
				delay between BPSRunnable#act and
				pos_pedal_out within [0ms,5ms].
			G t	delay between ext_pedal and
				pos_pedal_out within [0ms,10ms + 5ms].
				Table XIII
			CONTRACTS FOR INTERNAL BEHAVIOR OF
			BRAKEPEDALSENSOR-COMPONENT

runnable BPSRunnable, which is activated cyclically with a period of 10ms. Upon its activation it reads the sensor values from the ECU abstraction component and writes the position of

  Table XIV, top. Furthermore, P ALARM 1 :

		As	true.
		Aw	true.
		G	Alarm i occurs each 10ms.
		As	true.
	P BP SRunnable :	Aw G	true. delay between BPSRunnable#act and
			pos_pedal_out within [1ms,4ms].
			Table XIV
	PLATFORM CONTRACTS OBAINED BY ANALYSIS OF ECU CONFIGURATION
	RR n°8147

  Table XVI a contract C S1 stating the correct behavior in the absence As true Aw Only one of Fail(BrakeIndication) and Fail(SignalFailureDetection) occurs G Whenever BreakRequest occurs then BreakIndication or SignalFailureDetection is performed.

	C S 0 :
		Table XV
	HORIZONTAL CONTRACT REPRESENTING FUNCTIONAL SAFETY
		REQUIREMENT
		<<Function>>
		SafeBrakeIndication
	<<FunctionalExchange>> BrakeRequest	<<Function>> BrakeIndication	<<FunctionalExchange>>
			Detect(BrakeIndicationFail)
		<<SafetyFunction>>
		SignalingFailureDetection
	RR n°8147

Table XX HORIZONTAL

 XX Table XX. The nominal behavior of the C S 5 : Table XIX EXEMPLARY CONTRACT FOR NOMINAL BEHAVIOR SPECIFICATION BrakePedalSensor and the MalfunctionIndicator is formed similarly to C S5 . CONTRACT FOR SAFETY FUNCTION FOR BRAKING LAMP The composition of contracts C S4 . . . C S7 together with the not stated simple nominal contracts entails the contract C S8 shown on Table XXI stating the functional safety requirement.

			As	true
			Aw	Absence of fail(pos_pedal)
			G	Whenever pos_pedal occurs then
				lamp_intensity occurs.
		As	true
	C S 6 :	Aw G	true Mode BreakLampActuatorError is caused by
			fail(lamp_intensity) or mode PedalToLampError.

RR n°8147

VDC research, Track 3: Embedded Systems Market Statistics Exhibit II-13 from volumes on automotive/industrial automation/medical,

http://www-01.ibm.com/software/awdtools/doors/productline/

http://etc

PLM: Product Lifecycle Management. PLM centric design is used in combination with virtual modeling and digital mockups. PLM acts as a data base of virtual system components. PLM centric design is, for example, deployed at Dassault-Aviation http://www.dassault-aviation.com/en/aviation/ innovation/the-digital-company/digital-design/plm-tools.html?L=1 RR n°8147

See http://www.autosar.org/

See e.g. http://www.v-model-xt.de RR n°8147

http://www.omg.org/spec/SysML/

http://www.omg.org/spec/UML/

www.cesarproject.eu RR n°8147

http://www.w3.org/2005/rules/wiki/RIF_Working_Group

http://www.autosar.org/

http://www.osek-vdx.org/

http://www.iso.org/iso/search.htm?qt=Controller+Area+ Network&searchSubmit=Search&sort=rel&type=simple&published=true

http://www.flexray.com/

http://www.asam.net/

http://www.aeec-amc-fsemc.com/standards/index.html

http://www.rtca.org/

http://www.profibus.com/ RR n°8147

See[START_REF] Sudarsan | A product information modeling framework for product lifecycle management[END_REF] and also footnote 4.

http://www.iso.org/iso/catalogue_detail.htm?csnumber=43464

http://www.iec.ch/functionalsafety/

http://www.cenelec.eu/Cenelec/CENELEC+in+action/Web+Store/ Standards/default.htm

http://www.do178site.com/

Here we assume that the different application viewpoints are developed for the whole application and then combined by conjunction-this is just a methodological proposal; we could proceed differently.

In in a synchronization tuple, both occurrences and values of the different elements are unified.RR n°8147

http://www.geensoft.com/en/article/rtbuilder

This is unlike in compositional verification, where × i∈I M i |= M P is to be checked, where M i are detailed implementations and P is a property. In this case, the composition × i∈I M i typically gives raise to state explosion. Techniques have thus been proposed to verify such properties in an incremental way[START_REF] Stark | A proof technique for rely/guarantee properties[END_REF],[START_REF] Clarke | Compositional model checking[END_REF],[START_REF] Grumberg | Model checking and modular verification[END_REF],[START_REF] Abadi | Conjoining specifications[END_REF],[START_REF] Kupferman | Modular model checking[END_REF].RR n°8147

http://www.esterel-technologies.com/products/scade-suite/

http://www.geensoft.com/en/article/rtbuilder

http://www.mathworks.com/products/simulink/ RR n°8147

http://www.sdl-forum.org/MSC/index.htm RR n°8147

This is only an assumption intended to simplify the notations. It is by no means essential.

In fact, receptiveness is assumed in the original notion of i/o-automaton by Nancy Lynch[START_REF] Lynch | A proof of the kahn principle for input/output automata[END_REF],[START_REF] Lynch | Input/output automata: Basic, timed, hybrid, probabilistic, dynamic[END_REF]. We use here a relaxed version of i/o-automaton for reasons that will become clear later.

This is the usual wording in the literature.RR n°8147

This formalism is thus not purely synchronous and is mentioned in this section with a slight abuse.RR n°8147

Authors of[START_REF] Bertrand | Modal event-clock specifications for timed component-based design[END_REF] do not mention this fact for the following reason. They do not consider the issue of receptiveness for components and therefore the issue of compatibility does not arise.RR n°8147

In fact, the contract specification languages proposed in the projects SPEEDS[START_REF] Benveniste | Multiple viewpoint contract-based specification and design[END_REF] and CESAR (http://www.cesarproject.eu/) are examples of translations from a constrained English language to a formal models of contracts similar to Modal Interfaces.RR n°8147

We take the convention that the variables of the resulting i/o-automaton are those mentioned in the text of the requirement. Some adjustment is needed to this convention, however, as exemplified by Figure7. Suppose that some requirement says: "?gate_open never occurs". This is translated by having no mention of ?gate_open in the corresponding i/o-automaton. To express this "negative" fact we must keep track of the fact that ?gate_open belongs to the alphabet of actions of the i/o-automaton. Thus, when performing the translation, the explicit list of inputs and outputs should be explicitly given. To avoid such additional notational burden, we have cheated by omitting this unless necessary.RR n°8147

A case-study from the German SPES2020 project RR n°8147

Publisher Inria Domaine de Voluceau -Rocquencourt BP 105 -78153 Le Chesnay Cedex inria.fr ISSN 0249-6399

This work was funded in part by the European STREP-COMBEST project number 215543, the European projects CESAR of the ARTEMIS Joint Undertaking and the European IP DANSE, the Artist Design Network of Excellence number 214373, the MARCO FCRP TerraSwarm grant, the iCyPhy program sponsored by IBM and United Technology Corporation, the VKR Center of Excellence MT-LAB, and the German Innovation Alliance on Embedded Systems SPES2020.