Timed Automata Semantics for Analyzing Creol
Mohammad Mahdi Jaghoori (LIACS, CWI), Tom Chothia (University of, Birmingham)
TL;DR
This paper introduces a real-time semantics for the Creol language by translating processes into timed automata, enabling verification of timing properties such as deadlines in multi-core embedded systems using Uppaal.
Contribution
It provides a novel semantics for Creol that facilitates real-time analysis through timed automata mapping, supporting verification of scheduling and deadlines.
Findings
Verification of real-time properties in Creol models
Mapping Creol to timed automata enables analysis in Uppaal
Supports analysis of multi-core embedded systems
Abstract
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.