Department of Applied Computer Science, Faculty of Electrical Engineering, Automatics, Computer Science and Biomedical Engineering, AGH University of Science and Technology, Kraków, Poland
Michal Wypych
Department of Applied Computer Science, Faculty of Electrical Engineering, Automatics, Computer Science and Biomedical Engineering, AGH University of Science and Technology, Kraków, Poland
Jerzy Biernacki
Department of Applied Computer Science, Faculty of Electrical Engineering, Automatics, Computer Science and Biomedical Engineering, AGH University of Science and Technology, Kraków, Poland
Lukasz Podolski
Department of Applied Computer Science, Faculty of Electrical Engineering, Automatics, Computer Science and Biomedical Engineering, AGH University of Science and Technology, Kraków, Poland
Alvis is a formal modeling language intended for developing systems consisting of concurrently operating units (real-time, embedded, and distributed systems). This paper describes the timed version of Alvis that is suitable for modeling discrete-time systems. This paper is the first relatively complete description of timed Alvis. We present formal definition and semantics of timed models and the algorithm of labeled transition system generation and introduce the computer software that we developed to support Alvis. All concepts are illustrated by examples.
