Multitasking real-time systems verification
This topic deals with modeling of multitasking real-time application running under operating system by timed automata and its formal verification by model checking tool UPPAAL.
Since precise modeling of preemption is not possible by timed automata, we have focused on non-preemptive scheduling at first. The following two publication can be downloaded:
Waszniowski, L., Hanzálek, Z. Analysis of Real Time Operating System Based Applications. In Proceedings of First International Workshop on Formal Modeling and Analysis of Timed Systems ( FORMATS'03), Marseille, France, Lecture Notes in Computer Science, Springer-Verlag, September 2003. (Related models for UPPAAL (version 3.4.3) can be downloaded here.)
Waszniowski, L., Hanzálek, Z. Analysis of OSEK/VDX Based Automotive Application. In Proceedings of IFAC Symposium on Advance in Automotive Control (AAC'04). University of Salerno, Italy - April 19-23, 2004. (Related models for UPPAAL (version 3.4.3) can be downloaded here.)
Time automata allow to create over-approximate model of preemption.
Waszniowski, L., Hanzálek, Z. Formal Verification of OSEK/VDX Based Applications. In proceedings of Work-in-progress Session of 25th IEEE International Real-Time Systems Symposium, December 5-8, 2004, Lisbon, Portugal. Related models for UPPAAL (version 3.4.3) can be downloaded here.
Since the complexity of the model-checking verification exponentially grows with the number of clocks used in the model, The following model uses only one clock for all modeled tasks. Download it here.
Distributed real-time systems verification
To model distributed real-time systems, we have extended the above mentioned model of multitasking application by model of Controller Area Networ (CAN). This model is described in the following paper:
Krákora, J., Waszniowski, L., Píša, P., Hanzálek, Z.: Timed Automata Approach to Real Time Distributed System Verification. Submitted for 5th IEEE International Workshop on Factory Communication Systems, Work in Progress section. (Related models for UPPAAL (version 3.4.3) can be downloaded here).