Chapter 1: Introduction

1.1 Motivation

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].

Problem Definition

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:

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 approach.
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.

Many problems arise from such general requirements. This thesis proposes a solution based on the Timethread notation and the formal description technique LOTOS.

1.2 Objectives

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 previous section.

We define four main objectives in this context:

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.

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.

1.3 Organization

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 timethread-oriented specification.

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.