Tool Supported Methodology
1: Requirements Fragmentation and Categorization Phase
1.1 (Categorization): The user identifies and categorizes the informal requirement fragments;
1.2 (Dependencies): The user can create dependencies among the categorized requirement fragments.
Goto Top
2: Formalization Phase
2.1 (Formalization): The user formalizes each categorized requirement exploiting Unified Modelling Language (UML) constructs abd a Controlled Natural Language based on Property Specification Language;
2.2 (Traceability linking): The user links the elements of the formalization to the textual requirements.
Goto Top
3: Formal Validation Phase
3.1 (Requirements selection): The user chooses a set of requirements to focus the validation on particular aspects of the specification;
3.2 (Problem Definition): The user defines a set of problems, each one consisting of a set of objects and a set of scenarios and of properties;
3.3 (Model Checking): The user checks the defined problems and analyzes the results.
