Abstract
The development of complex computer-based systems poses two fundamental challenges. On one side, the architectural decomposition must be complemented by a suitable refinement of the requirements. On the other side, it is fundamental to provide the means for component reuse in order to limit development costs. In this chapter, the authors discuss the approach taken in FoReVeR, a project funded by the European Space Agency (ESA), where these two issues are tackled in the setting of space systems. The approach taken in FoReVeR is based on the idea of contracts, which allow one to formally specify the requirements of components at different levels of abstraction and to formally prove the correctness of requirements decomposition. In particular, the authors show how system-level requirements can be progressively refined into software requirements and how the contract-based framework supports the reuse of the components of a reference architecture under development by ESA. The authors discuss how the proposed solution has been integrated in a space development process and present the results of case studies.
TopIntroduction
The top-down design of complex critical system poses two fundamental challenges. The first one is the refinement of requirements, along with the progressive decomposition of the system architecture. In general, the quality and the traceability of requirements are fundamental for the whole design. Flaws in the requirements are in fact recognized as a major source of problems in the development, and may require major revisions in the advanced phases of the development cycle (Lutz, 1993). The second challenge is to enable for a correct reuse of (previously certified) components, which can lead to huge savings in development and certification costs. Unfortunately, the composition of correct components does not necessarily result in a correct system.
In this chapter we report how these issues have been addressed, in the context of space systems, within the FoReVeR project (see https://es.fbk.eu/tools/nusmv3/), an extended version of the NuSMV symbolic model checker.
Key Terms in this Chapter
Meta-Model: The set of frames, rules, constraints, models and theories applicable and useful for the modeling in a predefined class of problems.
Contract: Property of a system or component composed of an assumption and a guarantee. A contract represents an agreement between the system/component and its environment: the environment must respect the assumption, and in response the implementation of the system/component respects the guarantee.
Environment: Context of a system or component determining the data and events in input to the system/component.
Interface: The boundary of a component consisting of the declaration of a set of public features, data and/or events, used to interact with the environment.
Proof Obligation: A logical formula associated to a correctness claim for a given verification property. The formula is valid if and only if the property holds. The correctness of the property under verification is “delegated” to proving the correctness of the new formula.
Stepwise Refinement: A development technique in which the requirements and design of a system are first defined at a high-level of abstraction and then further define increasing the level of detail.
Requirement: A condition that should be satisfied or capability that should be possessed by the system or component under definition.
Functional Requirement: A requirement that define a function that a component or system must be able to perform.