WP5 - Foundations for the Elaboration and Analysis of Requirements Specifications

Partners Involved: IMP / ULEIC / UBA / UNRC / ITBA

This work package is concerned with the formal foundations, as well as with the development of practical techniques founded in these, for the elaboration and analysis of requirements specifications. Requirements specifications are often developed incrementally utilizing a variety of notations with different characteristics in terms of expressiveness, tractability, and understandability. Each notation plays a different role in a requirements engineering effort. Some are more appropriate for initial stages, others are simpler for interaction with non-technical stakeholders, while others are aimed at integrating with design and implementation activities. Thus, requirements elaboration and analysis is constrained by two major issues: the heterogeneity of the descriptions, and their intrinsic partial nature. Providing effective mechanisms for aiding in the elaboration and analysis of partial heterogeneous specifications of requirements calls for suitable formal foundations of these, as well as practical sound mechanisms that enable us to deal with partiality and heterogeneity. Within this work package, we shall work in various directions, most notably the formal foundations for heterogeneous requirements specifications, foundations and languages for formally expressing partial specifications, and properties of the studied formalisms in relation to their automated and semi- automated analysis. Analysis (and its automation) has an obvious significant relevance in the tasks of validating requirements, and helping elicit or discover further properties in this domain.

1. Partial Modelling Frameworks. We will investigate declarative and operational modelling frameworks in which it is possible to capture both common existential (e.g., sequence diagrams and use cases) and universal statements (e.g., invariants and safety properties) used commonly in requirements modelling languages and the partial nature of requirements specifications (e.g., behaviour that satisfies both existential and universal statements is not assumed to be valid). The challenge, from the logic side, is to identify logics with appropriate expressiveness and complexity characteristics that can support reasoning in this context. From the perspective of operational models, the challenge is to capture partial behaviour, and hence, identify appropriate variations of multi-valued state-machines and compositions mechanisms.
2. Automated and Semi-automated Tools for Validation, Verification and Elaboration of Requirements Specifications. We will investigate fully automated, tractable methods for identifying issues in partial specifications that can prompt corrections or further elaboration. Focus shall be on the use of model checking and satisfiability procedures that can automate heuristics commonly used in an informal manner in requirements engineering efforts (e.g., vacuity, inconsistencies, obstacles, conflicts, realizability, etc.). In addition, the use of symbolic machine learning techniques shall be investigated as a means for proposing automated and semi-automated diagnostic information.
3. Validation and Case Studies. We will experiment with the modelling frameworks and tools developed in the context of academic and industrial case studies to validate the applicability of our theoretical results and tools, and to postulate further hypotheses.
4. Formal foundations for requirements in the context of service oriented software. In the context of global ubiquitous computing, the structure of software systems is becoming more and more dynamic and heterogeneous as applications need to be able to respond and adapt to changes in the environment in which they operate. We will focus on providing solutions to the following two problems: (1) Most of the languages used in the development of such systems are not logical, in the formal sense, thus the existing theory does not apply as formal foundations for them. (2) The fact that in frameworks such as SCA (Service Component Architecture) the specifications of entities play different roles in service provision that are discovered and assembled at run time, not design time.

Publications in this work package