We give a simple language for Transition Diagrams (TDs), which is motivated both by the understanding that designers often refer to the need for synchronization diagrams in concurrent systems, and by anticipating the designer's wish to organize and re-organize the diagrams. Furthermore, we extend LOTOS with certain meta-combinators to facilitate the translation from these TDs to LOTOS. The resulting LOTOS is called metaLOTOS. Also, some transformations of metaLOTOS are provided.

The transition-style of diagrams is widely used to assist understanding of computing, e.g. finite state automata, flowcharts, statecharts and Petri nets. Recently, this style of diagrams has been applied to the field of human-computer interaction as well. Basically, this is to model user structures within system specifications [H90]. Following this idea, we can use interactive (behavioural) languages like CSP [H85], CCS [M89] and LOTOS [BB88] to model user-interfaces [A90], where their semantics are given by structural operation semantics and this semantics is very much in a transition-style.

On the other hand, a practical use of a specification language like LOTOS needs many tools to support the design process and to facilitate the associated formal methods. For instance,

(a) construction of a specification may be supported by an editor;

1

Abstrct

Yong Sun

Human Computer Interaction Group (HCI)

Department of Computer Science

University of York

Heslington, York YO1 5DD

UK

1 Introduction

Extensions of Transition Diagrams and LOTOS Specifications

from the View of Designers