A model checker for LOTOS.

Abstract

LOTOS (Language Of Temporal Ordering Specification) is a Formal Description Technique (FDT) based on the temporal ordering of observational behaviour. It was developed by ISO (International Organization for Standardization) for the specification of OSI (Open Systems Interconnections) services and protocols. CTL (Computation Tree Logic) is a branching-time temporal logic, which can be used to express properties of the system being designed. Efficient algorithms were reported in the literature which make it possible to check whether a given behaviour tree enjoys a property expressed in CTL. Such algorithms constitute what is commonly called "model checking". The topic of this thesis is the design and implementation of a model checker for LOTOS specifications called LMC (LOTOS Model Checker). LMC allows users to check whether a specification behaves correctly. To do so, LMC requires a graph model obtained by expanding the LOTOS specification symbolically, and a set of correctness properties describing the requirements behaviour of the system to be checked. These properties are expressed in the branching temporal logic CTL. We present an introduction to formal description techniques along with a review of some relevant existing work. We then present the technical framework of the branching temporal logic CTL, and discuss some important aspects such as correctness properties of concurrent systems and their classification. We discuss the algorithms used in our model checker together with their application to LOTOS. Finally, we use two examples to illustrate the validation methodology.