Automated reasoning for verification and validation

The main objective of this WP is the development of methodologies for the analysis, using formal methods, of the requirements of the various actors involved in the development of the software project. In order to reach this objective, the first step is the definition of a formal semantics for all the data, even the part that is expressed in form of diagrams. We foresee the usage of a modal temporal logic suitably extended to deal with all the aspects of the framework I*. As soon as a common representational language is chosen, we will focus on the methodologies for the integration of the requirements of the various actors. In fact, one of the difficult problems of the early requirements phase is the handling of the inconsistencies between the requirements of the various stakeholders or actors. In such a situation, it is difficult to come up with a unique model of the requirements. The second objective of this WP is the definition of semantics for the integration of information (requirements) coming from different actors having possibly conflicting goals.

The methodologies for requirements integration require the ability to assess the consistency of a specification. This consistency check must also apply to the successive phases of the software system development. In order to automatize this check we will first study the computational properties of the proposed formalisms. As a consequence, we will be able to devise an efficient reasoning tool that will allow for the integration of the requirements and the consistency checking of the specifications at each phase of the software development.

The overall model of the software system must be consistent but also satisfy all the expectations of the designers. It is of crucial importance that the designers can verify automatically that all requirements are satisfied. In this research project we intend to use model-checking techniques to validate the system.


ResearchWP1 - Methodology and processWP2 - Specification and analysisWP3 - Verification and ValidationWP4 - Automated planningWP5 - Natural languageWP6 - Analysis and testingWP7 - ToolWP8 - Case study