The Formose ANR project (ANR-14-CE28-0009) aims to design a formally-grounded, model-based requirements engineering (RE) method for critical complex systems, supported by an open-source environment.
Formose addresses three challenges:
- to take into account the high complexity of such systems,
- to better integrate RE with verification and validation techniques to ensure a better quality of requirements,
- to provide systematic guidelines and tool support during the
process of elaborating high quality requirements models.
Formose will define a formal language extending existing RE languages to consider the abstract architecture of complex systems and specific requirements for safety, performance and reconfiguration modes purposes. The language will be multi-views for validation purpose. The enactment of the RE process will be supported by a platform that will integrate tools developed during the project and existing verification tools used for verification activities.
Organization
The Formose project is structured in four Work Packages
(WP), plus a WP (WP0) dedicated to the management of the project. The
four WP go from the definition of a requirements modeling language to
the elaboration of a support open-source platform, including a formal
verification task. As an industrial project, it also includes real
industrial case studies and the assessment of the Formose method.
More precisely, the WP are defined as follows:
- WP1: Applicability and Evaluation of the Formose Method
- WP2: Requirements Modeling Language
- WP3: Requirements Verification
- WP4: Formose Method and its Support Tool
The objective of WP1 is to present real case studies provided by the industrial partners (THALES and ClearSy) and to evaluate the Formose method on these case studies. The 2 case studies are typical examples of critical complex systems developed in industry. They will be used to identify industrial needs related to the definition of a requirements engineering method (WP2 and WP4).
WP2 is intended to define the requirements modeling language. The aim of WP2.1 is to devise concepts to be introduced in a RE modeling language, taking inspiration in the state of the art (such as KAOS or Tropos/i*) but also adding support for concerns such as the architectural structural of hierarchical systems or as modes and reconfigurations. WP2.2 consists in defining and implementing user-oriented views for the requirements language.
WP3 gives a formal base to the method. WP3.1 defines the formal semantics of the requirements language while WP3.2 deals with verification issues. We plan to use existing tools, like B or UPPAAL, to perform formal verification of properties and consequently translation rules from the requirements language to these tools are defined. We also plan to devise an interpreter for errors detected by the provers during the properties verification task. The aim of the interpreter is to determine which parts of the requirements model are concerned by these errors.
WP4 consists in defining the Formose process and its support
platform, based on OpenFlexo, that integrates the tools developed in
the previous WP and the existing provers.
