It has been our long time wish to combine the best parts of the real-time verification methods based on timed automata (TA) (the use of regions and zones), and of the process-algebraic approach of languages like LOTOS and timed muCRL. This could provide us with additional verification possibilities for real-time systems, not available in existing timed-automata-based tools like UPPAAL. In this paper we extend the applicability of such discretization to extensions of TA available in UPPAAL as networks of timed automata and shared variables. To this end, we make use of mCRL2, the newer version of muCRL that includes time and multi-actions. The multi-actions are used to model the simultaneous access to shared variables and action synchronization.
|Title of host publication||Proceedings 22nd IEEE International Parallel and Distributed Processing Symposium (IPDPS 2008, Miami FL, USA, April 14-18, 2008)|
|Place of Publication||Piscataway NJ|
|Publisher||Institute of Electrical and Electronics Engineers|
|Publication status||Published - 2008|