This thesis describes a method where UCMs (formerly known as Timethreads) are transformed into LOTOS specifications for simulation and validation purposes. Two case studies are included: a traveller agency and a telepresence system.
Timethreads are a new notation for visual description of the different causality paths of a system. They illustrate causality sequences of activities through systems. A design process based on the use of timethreads has already been defined.
The Formal Description Technique LOTOS (Language Of Temporal Ordering Specification) is a specification language based on the temporal ordering of observational behaviour.
This thesis aims at the integration of formal methods in the design of real-time and distributed systems by presenting a LOTOS interpretation of timethreads. With the help of a timethread grammar and a suite of techniques, LOTOS specifications are derived from timethread maps. The designer can then play with the design by validating the specifications during the early stages of requirements capture and analysis.
- 12 Oct 2005
- Please feel free to discuss this article directly on this page. Constructive comments are welcomed! Please sign your TWiki name.
| Title || Formalization of Timethreads Using LOTOS |
| Authors || D. Amyot |
| Type || Thesis |
| Conference/Journal Title || |
| Volume/Number || |
| Editors || |
| Publisher || SITE, University of Ottawa |
| Month || December |
| Year || 1994 |
| Pages || 213 |
| DOI || |
| Keywords || LOTOS, timethreads |