Modelling and verification of real-time systems with Alvis

Abstract

Alvis is a formal language specifically intended for modelling systems consisting of concurrently operating units. By default, the time dependencies of the modelled system are taken into account, what is expressed by the possibility of determining the duration of each statement performed by the model components. This makes Alvis suitable for modelling and verification of real-time systems. The paper focuses on Alvis time models. The article outlines the syntax and semantics of such models, and discusses the main issues related to the generation of Labelled Transition Systems for time models. Particular attention was paid to tools that support the verification process.