This thesis applies formal techniques to the process of developing designs for systems constructed from a set of concurrent components. In particular, a technique for developing designs called slicing
is identified and formalized. In the slice technique the designer identifies triggering events at the edges of a system, and then specifies the global behaviour patterns which ripple through the different components of the system as a result of these triggering events. The basic novelty lies in a combination of formal specification of global behaviour patterns with a formal representation of design structures that is not found in "pure" behavioural specification techniques and that is inspired by the way practical engineers design such systems. From this follow novel techniques for developing and analyzing complete designs for concurrent systems. A method for representing slice behaviour of a system using the LOTOS specification language is developed. In order to facilitate design capture, a number of visual notations are developed to represent both structural and behavioural design. The visual notations allow the designer to express the design in a clear and intuitive manner while maintaining an underlying formal representation.
It is shown how slice based techniques can be used within a design process. Beginning with basic slices identifying the critical end to end behaviour of a system, specific techniques are developed for refining these slices to specify more complex behaviour. From these slice expressions, techniques are developed which allow a designer to analyze a design for correctness, and to assist in the specification and verification of individual component behaviours.
Examples and case studies are used to explore the applicability of the techniques and the visual notations. A discussion of the practical issues identifies how the slice style can be applied to large scale systems and discusses areas where automated tools can be used to assist the designer in the design process.
- 08 Jul 2010
- Please feel free to discuss this article directly on this page. Constructive comments are welcomed! Please sign your TWiki name.
| Title || Applying Formal Techniques to the Design of Concurrent Systems |
| Authors || Mark Vigder |
| Type || Thesis |
| Conference/Journal Title || PhD Thesis |
| Volume/Number || |
| Editors || |
| Publisher || SCE Dept., Carleton University |
| Month || July |
| Year || 1992 |
| Pages || 293 |
| DOI || |
| Keywords || Slicing, LOTOS, Use Case Maps, Specification, Design |