Timed Automata Semantics for Analyzing Creol

Mohammad Mahdi Jaghoori
Tom Chothia
(University of Birmingham)

We give a real-time semantics for the concurrent, object-oriented modeling language Creol, by mapping Creol processes to a network of timed automata. We can use our semantics to verify real time properties of Creol objects, in particular to see whether processes can be scheduled correctly and meet their end-to-end deadlines. Real-time Creol can be useful for analyzing, for instance, abstract models of multi-core embedded systems. We show how analysis can be done in Uppaal.

In MohammadReza Mousavi and Gwen Salaün: Proceedings Ninth International Workshop on the Foundations of Coordination Languages and Software Architectures (FOCLASA 2010), Paris, France, 4th September 2010, Electronic Proceedings in Theoretical Computer Science 30, pp. 108–122.
Published: 28th July 2010.

ArXived at: https://dx.doi.org/10.4204/EPTCS.30.8 bibtex PDF

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org