Formal Verification of Real-time Systems Developed for Single-processor Platform with Alvis

J. Baniewicz, M. Szpyrka (AGH Univ. of Science and Techn., Poland)

Formal verification is gaining importance today, taking into account the huge demand for IT systems as well as the costs caused by their erroneous operation. Formal languages considered in the literature implicitly assume that theoretically parallel processes can be performed at the same time, and the number of processors is unlimited. The paper describes an extension of the Alvis language for modelling embedded real-time systems that operate on a single-processor platform. The main advantage of the presented solution is that the same Alvis model can be verified assuming that the target platform is one- or multi-processor. We present main concepts of the new approach and illustrate them with appropriate examples.