|
Département d'ingénierie informatique |
Project leader : A. van Lamsweerde
Researchers : S. Brohez, C. Damas, R. De Landtsheer, B. Lambeau, E. Letier, D. Janssens, H. Tran Van
Collaborations :
- P. Massonet, C. Ponsard, J.F. Molderez, A. Rifaut (CETIC, Belgium)
- D. Ballant, R. Darimont, C. N?ve, J.L. Roussel (CEDITI, Belgium)
- J. Kramer, J. Magee, S. Uchitel (Department of ComputingImperial College, UK)
- S. Fickas (Computer and Information ScienceUniversity of Oregon, USA)
Funds : FNRS, Walloon Region (MILOS and REQUEST projects)
Description :
Requirements engineering (RE) is widely recognized as the most critical phase of the software lifecycle. Goal-oriented RE refers to the use of goals for eliciting, elaborating, structuring, specifying, analyzing, negotiating, documenting, and modifying requirements. Such use is based on a multi-view model showing how goals, objects, agents, scenarios, operations, and domain properties are inter-related in the system-as-is and the system-to-be. (By "system" we mean the target software together with its environment made of human agents, devices, legacy software, etc.). The KAOS methodology developed by our group provides a multi-view graphical language for system modeling, a lightweight formalism for model specification, an optional real-time temporal logic for model analysis, a systematic method for model elaboration, and various dedicated techniques for goal refinement and operationalization, conflict management, hazard analysis, agent responsibility assignment, goal mining from scenarios, etc. The methodology is supported by various tools (http://www.objectiver.com/, http://faust.cetic.be/) and has been used over more than 25 industrial projects.
- Exploring alternative options is at the heart of the requirements and design processes. Different alternatives contribute to different degrees of achievement of non-functional goals about system safety, security, performance, usability, etc. Such goals in general cannot be satisfied in an absolute, clear-cut sense. The KAOS framework has been extended with a probabilistic layer to model, specify and reason about goals that can be satisfied only partially. Non-functional goals are specified in a precise, probabilistic way ; their specification is interpreted in terms of application-specific measures ; constructive support is provided for guiding the refinement of such goals ; and the impact of alternative goal refinements can be evaluated in terms of refinement equations over random variables involved in such goals.
- Various syntactic/semantic mappings have been explored for transforming upstream KAOS models into downstream operational models. The motivation there is to enable the integrated use of complementary toolsets. In this perspective, we have defined a set of transformation rules for mapping KAOS models to (a) SCR mode, event and condition tables, and (b) LTS state machine models ananlyzable by the LTSA toolset. As an interesting side-effect, this work reveals tricky semantic issues arising from attempts to integrate multiple formalisms.
- In close collaboration with the Distributed Software Engineering Group at Imperial College, a novel technique has been devised to detect undesirable scenarios that may be covered by state machine models synthesized from other scenario examples. The detected scenarios belong to a new class of implied scenario ; they are generated by analysis of monitoring/control links among agents interacting through events in the model.
- The KAOS modeling framework has been extended to capture and analyze threat models that capture intentions of malicious agents in the environment, see the " Secure System Engineering " theme.
- On the tool side, progress has been made in close collaboration with the CETIC research center. A first version of our goal-oriented animator has been issued. This tool is built on a client-server architecture for concurrent model animation by multiple users. It executes parallel state machines compiled from goal operationalizations. The animation can be focussed on partial model fragments within the scope of some specific goal of interest. Violations of requirements/assumptions can also be detected by monitors generated from the corresponding temporal logic formalization. Beside the animator, a refinement checker has been developed. This tool checks the correctness of goal refinements into sets of subgoals or operations ; in case the refinement is incorrect the tool generates counter-example scenarios that may suggest missing subgoals or operations. The tool uses a bounded SAT solver to achieve this.
Portion of a model for a Train Control System:
goal refinement and assignment