Priority inversion detection in Alvis models

Embedded systems verification can be a very challenging task. Most of such systems is composed of subsystems that run concurrently, communicate one with another, compete for shared resources etc. Concurrent systems reveal errors such as deadlocks, livelocks, process starvation and so on. The paper focuses on detection of a priority inversion in Alvis models. Alvis is a novel modelling language defined especially for the embedded systems design and formal verification. Based on CCS and XCCS process algebras, Alvis combines a flexible graphical modelling of interconnections between agents with a high level programming language used for the description of agents behaviour. A priority inversion is a common pitfall in embedded systems. It is hardly possible to detect the problem using tests only. We discuss how the problem can be detected in Alvis models. The discussion is illustrated with real-life examples.