Communication with Environment in Alvis Models

Alvis is a modelling language defined for the design and a formal verification of embedded systems. An Alvis model is a system of agents that usually run concurrently, communicate one with another, compete for shared resources etc. Due to the fact that an embedded system usually collects inputs that come from its environment and provides outputs that go to the environment it is necessary to provide a mechanism to describe such a communication. In contrast to another formal languages used to model embedded systems it is not necessary, using Alvis, to design such an environment as a part of a model. The paper deals with the problem of modelling a communication with an embedded system environment with Alvis.