Formose
Problem
Critical complex systems need a formally-grounded requirements engineering (RE) method that accounts for their architectural complexity, integrates verification and validation techniques to ensure the quality of requirements, and gives systematic guidelines and tool support for elaborating high-quality requirements models.
Contribution
The Formose ANR project (ANR-14-CE28-0009, 2014-2019) designed a formal, model-based requirements engineering method for critical complex systems, supported by an open-source environment. It defined a multi-view requirements modeling language extending existing RE languages with the abstract architecture of complex systems and with requirements for safety, performance and reconfiguration modes, together with translation rules to formal verification tools such as B and UPPAAL. The supporting platform was built on OpenFlexo, integrating the tools developed during the project with the existing provers. The project ended in 2019; its tools, documentation and examples remain available for download.
Partners
Two academic partners and three companies, all with a strong background in formal methods:
- ClearSy — safety-critical systems engineering based on the B formal method
- LACL (Laboratoire d'Algorithmique, Complexité et Logique, Université Paris-Est Créteil) — logic, computation and system verification
- Institut Mines-Télécom (Télécom Bretagne, Télécom SudParis) — design processes, product models, verification of critical systems
- OpenFlexo — the model federation platform used to build the project's supporting tool
- THALES — mission-critical information systems for aerospace, defense and security
Publications
2018
Bridging the Gap Between Informal Requirements and Formal Specifications Using Model Federation
Authors : Golra, Fahad Rafique and Dagnat, Fabien and Souquières, Jeanine and Sayar, Imen and Guerin, Sylvain
In Lecture Notes in Computer Science, Toulouse, France pp. 54-69 .jun, 2018.[PDF] [DOI] [BibTeX]Keywords: Formal models ; Requirement engineering ; Model federation
Einar Broch Johnsen, Ina Schaefer Springer
hal-01853610 v1
2016
Continuous Requirements Engineering Using Model Federation
Authors : Golra, Fahad Rafique and Beugnard, Antoine and Dagnat, Fabien and Guerin, Sylvain and Guychard, Christophe
In Proceedings RE 2016 : 24th IEEE International Requirements Engineering Conference, Beijing, China pp. 347 - 352 .sep, 2016.[PDF] [DOI] [BibTeX]Keywords: Requirements Modeling ; Traceability ; Continuous Requirements Engineering ; Model Federation ; Requirements Engineering
hal-01487055 v1
Download
Download the Formose prototype