Formal requirements modeling for critical systems: Method and Toolkit – FORMOSE

The Formose project is an industrial research project that aims to provide a formally-grounded, model-based requirements engineering method for critical complex systems, supported by an open-source environment. Formose is a 48 months project proposed by a consortium made up of 2 academic partners (LACL—project leader— and Institut Mines-Telecom) and 2 companies (THALES and ClearSy).
It is well-known that requirements engineering (RE) is critical in software and system design. Indeed, a major part of the cost of software and system development is known to be traceable to the understanding of the problem domain and requirements. Today’s current industrial practices and tools are not sufficiently efficient. They mainly consist of in-house processes, lessons learnt documents, and requirements management tools (word processor macros, traceability tools, requirements database). Even if, in the last decade, much research on this topic reached maturity, recent studies have pointed out that issues remain open. The Formose project will address several challenges raised by these issues, the most crucial in the domain of RE for critical complex systems. They concern the need of taking into account the high complexity of such systems, the need of a better integration of RE with verification and validation techniques to ensure a better quality of requirements, and more generally the need of method guidance and tool support during the process of elaborating high quality requirements models. The main results of the project will be the following.
First, we will define a requirements modeling language integrating basic concepts of existing languages, such as KAOS or Tropos/i*, and adding new ones to take into account the specific characteristics of critical complex systems: their abstract architecture will be considered by allowing requirements to be defined at different abstraction layers and verifying their consistency; the language will allow to specify not only non-functional requirements related to safety and performance but also specific requirements related to the presence of different operational modes and reconfigurations in such systems. The language will be multi- views (natural language, graphical notations, formal notations) to be understandable by all the stakeholders. For verification purpose, we will adopt existing and complementary formal methods, supported by efficient tools: the B method and the timed model-checker UPPAAL. Then we will define a highly customizable process for requirements engineering of complex systems to guide the engineers in their different activities for elaborating requirements models. To support the enactment of the process we will use the OpenFlexo platform that will integrate not only the ad-hoc tools developed during the project but also the existing verification tools (Atelier B and UPPAAL model-checker). We also envision to ensure a two way exchange: OpenFlexo will be able to send proof obligations to a prover and will also be able to get the answer from the prover and interpret it to present it to engineers, using adequate representations.
Finally, all along the project, we intend to regularly assess the method and the tools using the case studies provided by the industrial partners (THALES and ClearSy). Last but not least, THALES and ClearSy engineers will follow the method and be active users of the tools to provide real world usage return on the usability of the Formose method. ClearSy will ensure tools exploitation and maintenance beyond project completion and THALES will develop the industrial version of the tools.
The dissemination of the results will be ensured by a web site, publications in national and international journals and conferences, and free availability of the platform. We also intend to communicate towards industrial communities that are concerned by critical complex systems by presenting publications in national and international industrial conferences.