Formalization of timethreads using LOTOS.

Abstract

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.