ISSN:
1432-010X
Keywords:
Key words:Animation – Formal methods – Message sequence charts – Scenarios
Source:
Springer Online Journal Archives 1860-2000
Topics:
Computer Science
Notes:
Developing complex, safety critical systems requires precise, unambiguous specification of requirements. A formal specification language is thus well suited to this task. Formal specification languages require, but also exacerbate, the need for tools. In particular, tools should support the elaboration (how to build the formal specification) and the validation (how to check the adequacy of the specification towards the informal needs of the various stakeholders). This paper focuses on the language Albert II, a formal language designed for the purpose of expressing requirements for distributed real-time systems. It presents two contributions supporting its use. The first contribution aims at improving the elaboration process by providing a method for constructing an Albert II description from scenarios expressing the stakeholders’ requirements. These are represented through message sequence charts extended to deal with composite systems. The second contribution takes the form of a requirements validation tool (a so-called animator) that the stakeholders can use interactively and cooperatively in order to explore different possible behaviours (or instance-level scenarios) of the future system. These behaviours are automatically checked against the formal requirements specification.
Type of Medium:
Electronic Resource
URL:
http://dx.doi.org/10.1007/s007660050005
Permalink
