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.

-- GunterMussbacher - 12 Oct 2005


  • Please feel free to discuss this article directly on this page. Constructive comments are welcomed! Please sign your TWiki name.

FormForVirtualLibrary edit

Title Formalization of Timethreads Using LOTOS
Authors D. Amyot
Type Thesis
Conference/Journal Title
Publisher SITE, University of Ottawa
Month December
Year 1994
Pages 213
Keywords LOTOS, timethreads
Topic attachments
I Attachment Action Size Date Who Comment
da_thesis.pdfpdf da_thesis.pdf manage 1 MB 12 Oct 2005 - 18:56 GunterMussbacher D. Amyot's MSc thesis
Topic revision: r3 - 08 Mar 2010, DanielAmyot
This site is powered by FoswikiCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding Foswiki? Send feedback