Formalization of Timethreads Using LOTOS
Formalization of Timethreads Using LOTOS
University of Ottawa, October 1994
Chapter 1: Introduction
This thesis is part of an ongoing project from the Formal Methods in Design (FMD) research group.
This project aims at defining a framework for the integration and support of formal methods in the
timethread-centered design process. For that purpose, one of the first steps defined was to show
that LOTOS specifications could be generated from timethread designs. This thesis addresses this issue.
Formal Methods in the Design Process
Formal methods in software engineering intend to provide a mathematical foundation to the process
of software design, transformation, and validation. Many such methods were developed in the last decade.
Their integration in the design process may indeed prove very profitable, if this is done in an appealing
and cost-effective way for use in the industrial environment. Nevertheless, industrial developers are not
inclined to integrate these new methods in their design processes. Some of the main reasons concern the
relative complexity of formal languages, and the new ways of thinking they impose on designers.
A certain degree of informality is essential in early stages of the development process. Designers in industry
regularly use a variety of notations in a partially informal manner to capture requirements and candidate
solutions. These notations, although informal, are useful as thinking tools. However, one cannot proceed
from the informal to the formal by formal means. We cannot go automatically from these informal diagrams
and sketches to a complete formal specification. It is also almost impossible to capture the requirements
correctly by using formal methods directly. Design decisions have to be made, and many intermediate
steps are often required.
We need a less painful way of creating formal specifications in industry. We want a method where
designers could use the power of formal techniques through a user-friendly interface. One of the
purposes of our work is to be able to capture the requirements and then to do high-level requirement
testing in early stages of development. This is very important since the further errors are detected in
a product's development, the more costly it is to fix them [Pro92]: "Fixing a problem in the requirements
costs 1% as much as fixing the resulting code" [Pfl92].
We believe that formal methods do not intend to replace the whole design process, but their integration
in the development process could lead to solutions with fewer errors in a shorter time period. The real
question then becomes: how should formal methods be integrated in the design process of real-time
and distributed systems in an appealing way for industrial engineers?
We think that the integration of formal methods is best achieved when designers do not have to change
their way of thinking and communicating. The following requirements, already discussed in [BBO94],
present the main issues from our point of view:
Many problems arise from such general requirements. This thesis proposes a solution based on the
Timethread notation and the formal description technique LOTOS.
- Designers should be allowed to use whichever design description model offers them
the expressiveness and flexibility they need to design real-time and distributed
systems. The way people actually work does not have to be radically changed.
- Designers can use different formal methods to analyze different aspects of these systems.
One formal method is not expressive enough to capture the whole design. It is only a
projection. A multi-formalism approach has many advantages over a single-formalism
- Designers do not have to be experts in a specific formal language to use it. A formal
method should be transparent to the user while its strengths are being used.
- Since visual notations are more expressive and easier to conceptualize at a high
level of abstraction than textual descriptions, they should be used to capture the
major concepts and basic scenarios from the requirements.
- Tools must be available to help the designer go from the informal to the formal. Tools
specialized for a formal method can be used afterwards on the formal description.
This thesis aims at providing elements for the integration of the formal technique LOTOS in a
timethread-centered design process while conforming to the five requirements enumerated in the
We define four main objectives in this context:
To satisfy these objectives, we will use an approach based on formal interpretation methods.
Chapter3 presents more deeply this approach and the different contributions of the thesis.
- To demonstrate that we can manually generate LOTOS specifications from timethread maps
- To show that these specifications are meaningful and that they can be used to execute
the design. This is also referred as play the design.
- To show that tools could eventually support the transformation from timethreads to LOTOS.
- To discuss resulting problems, difficulties, and new research issues.
The seven remaining chapters will cover the following issues:
CHAPTER 2: Background
We review the Timethread visual notation, the formal language LOTOS, and the LARG model
for architectural graphs. Several terminology definitions are also given.
CHAPTER 3: The Approach and the Contributions
We present the approach taken by the FMD research group for the integration of formal methods
in the design process. This approach is based on formal interpretation methods. Four sub-methods
(map decomposition, LAEG, mapping, and composition) are introduced. Then, the contributions of
the thesis are enumerated w.r.t. the objectives of the previous section. Finally, we present an ongoing
case study: the Traveler system.
CHAPTER 4: From Timethreads to LOTOS
This chapter presents the LOTOS semantics given to the Timethread notation. It enumerates a few
basic concerns and according solutions, and then discusses a new timethread grammar. Single
timethreads, simple interactions, and special timethread symbols are developed using this grammar,
for which mapping rules are given for the generation of LOTOS specifications. Examples inspired
from the Traveler system are given all along the chapter.
CHAPTER 5: Elements of a Life-Cycle Methodology
We firstly present a short overview of a timethread-oriented life-cycle methodology, and then
different techniques related to this methodology are discussed. We present the complete mapping
procedure of the Traveler timethread map onto LOTOS, followed by a discussion about a few
transformation techniques. Finally, we apply LOTOS-based validation techniques to our
CHAPTER 6: Case Study: Telepresence A Multimedia System Design Example
The methods and techniques introduced in the previous chapters are applied to a more realistic
real-time and distributed system: the multimedia application Telepresence. We present two
timethread maps where one is a transformation of the other. The first one is constructed from
basic use cases, mapped onto LOTOS, and then validated against the requirements. The
second timethread map is a transformation (factoring) of the first one that preserves path
equivalence. Again, a LOTOS specification is generated and validated using different simulation
and testing techniques.
CHAPTER 7: Discussion
This chapter discusses several issues encountered in the research work of this thesis.
We chose to emphasize four main issues related to: the first architecture, the STDL grammar,
validation in general, and a few ideas on possible tools.
CHAPTER 8: Conclusion and Future Work
This last chapter concludes the thesis. It reviews the contributions with respect to the thesis
objectives. Then, short-term and long-term research issues are identified.