The Albert II Language. On the Design and the Use of a Formal Specification Language for Requirements Analysis

The requirements engineering activity,
which concerns the elicitation, the modelling, the analysis, and the
validation the customers' needs, is recognized as a crucial activity
in the software lifecycle.

Specification languages supporting this activity for
complex systems, like real-time systems, are expected possess two main
qualities:

• expressiveness so that requirements can be modelled in a natural
  way,
  
• formality allowing automated reasoning on a specification document
  in order to discover potential incompletenesses and/or inconsistencies.
  

The Albert II language has been designed with these objectives in mind.

In this thesis, the Albert II language is presented intuitively
and formally, and is illustrated through the handling of a real-size
case study. Various issues around the language are discussed, e.a. methodological
issues, availability of tools, link with other phases of the software
lifecycle,...