The Catalogue of System and Software Properties (CSSP) aims to systematize a catalogue-guided speci fication of requirements per system level through the use of requirement boilerplates.
The whole process is based on a Catalogue of Requirements in the form of a knowledge base that will guide the engineer(s) throughout the decomposition of requirements and their coverage check through the maintained traceability links. The Catalogue comprises boilerplates, which are semi-complete requirements. Boilerplates are instantiated into complete requirements by replacing placeholders with system entities appropriate for the particular system context of the mission under design. The concepts referenced in the boilerplate placeholders are mapped to a concrete semantic model of the system’s domain, which is encoded in a well-organized OWL ontology. We thus aim to avoid indeterminate references in the speci ed requirements and eventually retrieve from the ontology the relevant information for the subsequent modeling activities.
In the conducted case study, we focused on the software related system requirement process that produces the information for input to the System Requirements Review (SRR). This establishes the functional and the performance Requirements Baseline (RB) of the software development and constitutes the link between the space system processes and the software processes. The RB consists of explicit requirements for the system from the viewpoint of a system engineer and/or a customer. We studied the properties derived from the requirements as formal speci cations that constrain the structure and the behavior of the system under design, such that the requirements from which they are derived are properly covered.
Our CSSP model-based speci fication and veri fication process aims to the early establishment of behavioral correctness through two diff erent types of properties:
- (i) those that can be enforced by design through one of nine formal architecture styles and
- (ii) those that should be speci ed in a verifi able form (logic language speci cation amenable to model checking).
The modeling language of our choice is the BIP (Behavior, Interaction, Priority), which has been formally proven a sufficiently expressive modeling language and it has been succesfully used as a unifying semantic framework for heterogeneous models in various modeling languages.
The BIP model derived from RB-level requirements can be compiled and used for simulation, thus serving as a proof-of-concept design for requirement validation. It can subsequently be used as a baseline for formal design re finement aiming to preserve the established properties, while introducing Technical Speci cation (TS) level requirements with their derived properties, which take into account software and hardware constraints in the system. We also advocate a catalogue-guided speci cation of requirements at this level and an analogous approach for the speci cation of properties.
The software requirements are transformed, once they have been specifi ed, into a description of the software’s top-level structure, the so-called software architecture. This involves:
- the static architecture that provides a static decomposition of the software into components with all the derived properties allocated to them, and
- the dynamic architecture that speci es the software’s behavior by identifying all active objects such as threads, tasks and processes, along with their resource and I/O dependencies.
The CSSP model-based speci cation and veri cation process has been automated through the use of existing mature modeling and veri cation tools along with a new tool with a GUI for the catalogue-guided speci cation of requirements (and their derived properties) on top of the CSSP ontology. We collectively refer to this set of tools as the Property Speci cation & Veri cation (PSV) framework.
This project was funded by the European Space Agency (ESA).
Partners:
- Aristotle University of Thessaloniki (Greece)
- EPFL (Switzerland)
- Thales-Alenia Space (France)