Intelligent Systems Lab

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 different 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:

1. the static architecture that provides a static decomposition of the software into components with all the derived properties allocated to them, and
   
2. 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)