Title :

Early validation of system requirements and design through correctness-by-construction

Author(s) :

Stachtiari, Emmanouela [Auteur]
Aristotle University of Thessaloniki
Mavridou, Anastasia [Auteur]
NASA Ames Research Center [ARC]
Katsaros, Panagiotis [Auteur]
Aristotle University of Thessaloniki
Bliudze, Simon [Auteur]
Self-adaptation for distributed services and large software systems [SPIRALS]
Sifakis, Joseph [Auteur]
VERIMAG [VERIMAG - IMAG]

Journal title :

Journal of Systems and Software

Pages :

52-78

Publisher :

Elsevier

Publication date :

2018

ISSN :

0164-1212

English keyword(s) :

Requirements formalization
Rigorous system design
Model-based design
Correctness-by-construction

HAL domain(s) :

Informatique [cs]/Systèmes embarqués
Informatique [cs]/Système multi-agents [cs.MA]
Informatique [cs]/Modélisation et simulation
Informatique [cs]/Systèmes et contrôle [cs.SY]
Informatique [cs]/Génie logiciel [cs.SE]

English abstract : [en]

Early validation of requirements aims to reduce the need for the high-cost validation testing and corrective measures at late development stages. This work introduces a systematic process for the unambiguous specification ...
Show more >Early validation of requirements aims to reduce the need for the high-cost validation testing and corrective measures at late development stages. This work introduces a systematic process for the unambiguous specification of system requirements and the guided derivation of formal properties, which should be implied by the system 's structure and behavior in conjunction with its external stimuli. This rigorous design takes place through the incremental construction of a model using the BIP (Behavior-Interaction-Priorities) component framework. It allows building complex designs by composing simpler reusable designs enforcing given properties. If some properties are neither enforced nor verified, the model is refined or certain requirements are revised. A validated model provides evidence of requirements' consistency and design correctness. The process is semi-automated through a new tool and existing verification tools. Its effectiveness was evaluated on a set of requirements for the control software of the CubETH nanosatellite and an extract of software requirements for a Low Earth Orbit observation satellite. Our experience and obtained results helped in identifying open challenges for applying the method in industrial context. These challenges concern with the domain knowledge representation , the expressiveness of used specification languages, the library of reusable designs and scalability.Show less >

Language :

Anglais

Popular science :

Non

Collections :

• Centre de Recherche en Informatique, Signal et Automatique de Lille (CRIStAL) - UMR 9189

Source :

Harvested from HAL