Modelling of signals handling with alvis

Alvis is a modelling language defined for the design and a formal verification of embedded systems. The key concept of Alvis is an agent which denotes any distinguished part of the system under consideration with a defined identity persisting in time. Alvis combines a graphical modelling of interconnections among agents with a high level programming language used for the description of agents behaviour. Embedded systems collect inputs that come from sensors and provide outputs that go to controllers. The distinguished kind of inputs are interrupts signals. The paper deals with the problem of modelling interrupts handlers with Alvis. The proposed solutions are illustrated with examples of Alvis models.