Showing 1–2 of 2 results for author: Jaghoori, M

Decidability Problems for Actor Systems

Authors: Frank De Boer, Mahdi Jaghoori, Cosimo Laneve, Gianluigi Zavattaro

Abstract: We introduce a nominal actor-based language and study its expressive power. We have identified the presence/absence of fields as a crucial feature: the dynamic creation of names in combination with fields gives rise to Turing completeness. On the other hand, restricting to stateless actors gives rise to systems for which properties such as termination are decidable. This decidability result still… ▽ More We introduce a nominal actor-based language and study its expressive power. We have identified the presence/absence of fields as a crucial feature: the dynamic creation of names in combination with fields gives rise to Turing completeness. On the other hand, restricting to stateless actors gives rise to systems for which properties such as termination are decidable. This decidability result still holds for actors with states when the number of actors is bounded and the state is read-only. △ Less

Submitted 3 December, 2014; v1 submitted 17 September, 2014; originally announced September 2014.

Journal ref: Logical Methods in Computer Science, Volume 10, Issue 4 (December 4, 2014) lmcs:1091

Timed Automata Semantics for Analyzing Creol

Authors: Mohammad Mahdi Jaghoori, Tom Chothia

Abstract: We give a real-time semantics for the concurrent, object-oriented modeling language Creol, by map** 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 model… ▽ More We give a real-time semantics for the concurrent, object-oriented modeling language Creol, by map** 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. △ Less

Submitted 28 July, 2010; originally announced July 2010.

Comments: In Proceedings FOCLASA 2010, arXiv:1007.4993

Journal ref: EPTCS 30, 2010, pp. 108-122