A Framework Based on Implementation Relations for Implementing LOTOS Specifications

in Computer Networks & ISDN Systems (1992), 25(1), 23-41

A framework is developed for studying the implementation process, as a stepwise process in which an abstract specification is successively transformed to reach a final compilable specification adapted to ... [more ▼]

A framework is developed for studying the implementation process, as a stepwise process in which an abstract specification is successively transformed to reach a final compilable specification adapted to the computer environment. In this context, an implementation relation is referred to as the relation which should link any ``valid'' implementation to its abstract formal specification. In other words, the implementation relation is intended to express formally the notion of validity. Our framework allows the exact characterization of the transformations which may take place at each step for a given implementation relation. This framework is essential for dealing with non-transitive implementation relations. In the second part of the paper, these results are exemplified in LOTOS on some existing relations, and an apparent paradox is presented. Some new results about these relations are also derived. [less ▲]

An Upward Compatible Timed Extension to LOTOS

in Parther, Ken; Rose, Gordon (Eds.) Formal Description Techniques IV (1992)

We propose a timed extension of LOTOS, denoted TLOTOS, which is upward compatible with the standard LOTOS. It means first that a timed behaviour expression which does not use any language extension will ... [more ▼]

We propose a timed extension of LOTOS, denoted TLOTOS, which is upward compatible with the standard LOTOS. It means first that a timed behaviour expression which does not use any language extension will have the same semantics as in standard LOTOS. In addition, we have pushed this upward compatibility one step beyond by requiring and obtaining that all the familiar equivalence laws of standard LOTOS be preserved e.g. B [] B approximately B, B [] stop approximately B. This is needed in order to keep the intuition of a standard LOTOS user unchanged. TLOTOS has been mainly inspired by other approaches such as Moller Tofts's TCCS (Temporal CCS), Hennessy Regan's TPL (Temporal Process Language) and Nicollin Sifakis's ATP (Algebra of Timed Processes). Our model is not strictly asynchronous (like standard LOTOS, CCS, CSP, ACP) nor strictly synchronous (like SCCS, CIRCAL, Meije). For compatibility and simplicity, we decided to keep the model asynchronous for a large part and, for dealing with time, to introduce a `'synchronous part'' by way of a new basic `'synchronous'' or timed action in the asynchronous semantic model. The design of our TLOTOS is presented together with other possible design alternatives which are all rejected according to our compatibility or expressive power requirements. The solution that we obtain is simple and satifactory, and its operational semantics is presented in depth. Two examples are provided to illustrate the use of TLOTOS. [less ▲]

Equivalence associée à la relation de conformité "conf" et simplification du testeur canonique en LOTOS

in Rafiq, Omar (Ed.) CFIP'91 Ingénierie des Protocoles (1991, September)

On the role of implementation relations in the design of distributed systems using LOTOS

Book (1991)

Les applications informatiques des années 90 et leurs implications sur les réseaux de communication

in Bulletin Scientifique de l'Association des Ingénieurs Electriciens sortis de l'Institut Electrotechnique Montefiore (1991), 2

Architectural and Behavioural Modelling in Computer Communication

in Barton, M.; Dagless, E.; Reijns, G. (Eds.) Distributed Processing (1987, October)

LOTOS, un outil utile ou un autre langage académique ?

in Danthine, André (Ed.) Les réseaux de communication - nouveaux outils et tendances actuelles (1987, January)