Affiliations: AGH University of Science and Technology, Department of Applied Computer Science, Al. Mickiewicza 30, 30-059 Krakow, Poland. {mszpyrka,ptm,Rafal.Mrowka,kotulski}@agh.edu.pl
Note: [] Address for correspondence: AGH University of Science and Technology, Department of Applied Computer Science, Al. Mickiewicza 30, 30-059 Krakow, Poland
Abstract: The paper presents a formal description of a subset of the Alvis language designed for the modelling and formal verification of concurrent systems. Alvis combines possibilities of a formal models verification with flexibility and simplicity of practical programming languages. Alvis provides a graphical modelling of interconnections among agents and a high level programming language used for the description of agents behaviour. Its semantic depends on the so-called system layer. The most universal system layer α0, described in the paper, makes Alvis similar to other formal languages like Petri nets, process algebras, time automata, etc.
