Alvis is a formal modelling language being developed at AGH-UST in Krakow, Department of Applied Computer Science. The main aim of the project is to provide a flexible modelling language for concurrent systems with possibilities of a formal models verification. Alvis combines advantages of high level programming languages with a graphical language for modelling interconnections between subsystems (called agents) of a concurrent system.

Alvis uses a very small number of graphical items and language statements. Our goal was to provide a flexible language with a small number of concepts, but with a possibility of a formal verification of models. An Alvis model semantic finds expression in a LTS graph (labelled transition system). Execution of any language statement is expressed as a transition between formally defined states of such a model.

The key concept of Alvis is agent that denotes any distinguished part of the system under consideration with defined identity persisting in time. An Alvis model is a system of agents that usually run concurrently, communicate one with another, compete for shared resources etc. Agents are divided into three groups: active agents can be treated as processing nodes, passive agents represent shared resources and hierarchical agents represent submodels.

An Alvis model is composed of three layers:

1. Graphical layer is used to define data and control flow among distinguished parts of the system under consideration that are called agents. The layer takes the form of a hierarchical graph called communication diagram and supports both top-down and bottom-up approaches to systems development.
2. Code layer is used to describe the behaviour of individual agents. It uses both Haskell functional programming language and original Alvis statements.
3. System layer that is predefined and provides information about a running environment i.e. the hardware and/or operating system. It is necessary for the simulation and verification purposes.

Go back