FAUST

Formal Analysis Using Specification Tools

The FAUST toolset was developed to help reaching high quality in requirements document, especially for complex systems with critical aspects. FAUST provides tools for the validation, verification and test generation based on requirements of such systems. The formal level of analysis is made accessible through a natural integration within text and graphical notations. Moreover, an graphical animation tool also allow the stakeholders to have a direct understanding based on domain specific visualizations. The integration in industrial methods and tool chains was also addressed.

Factsheet:

Project type: Structural funds in Wallonia
Status: Finished
Collaboration: Wallonia
Role: Coordinator
Started: 1 June 2001
Program: Phasing out Objectif 1
CETIC budget: 2351923 €

Project team

Objectives of the project

Requirements engineering is a crucial step in the development of an software system. More particularly when considering mission critical systems, it is imperative to be able to reach high quality levels.

The objective of the FAUST project is to propose an integrated toolset for the analysis of requirements enabling the production of high quality requirements documents for complex industrial systems. This toolset relies on the requirements formalization in a goal-oriented methodology and proposes a number of rigorous reasoning on those models, among them:

Verification : checking that the requirements are complete/consistent, robust.
Validation : checking that the requirements are reflecting the user needs.
Acceptation : checking that the delivered system meets the requirements.

In order to make the tools accessible to the industrial user, formal techniques are hidden as much as possible. Automated techniques like model-checking and SAT engines are used and can yield explanation in case of failures. Visualisation tools are also provided for displaying system behaviors based on domain specific notations.

Results of the project

Software toolset for the formal modeling and analysis of requirements of critical systems.
Set of requirements and design-level services available to companies having mission critical needs

Appreciation of the project for the companies

Method and tools for managing requirements of critical system by formalising where and when needed and based on tools easing and hidding the formalism as much as possible.
Better link between the requirements process and downstream development steps: traceability, generation of architectures, data models, etc. Those links are reflecting a model-driven engineering/model-driven development.
Integration in industrial toolchain, based on the Objectiver toolset and the Eclipse platform. AADL and B/Event B are more specifically treated in more specific projects.
Industrial validation through experiments in security (Grid, eID) and safety related domains (transport, aerospace)