Lookup NU author(s): Dr Alexei Iliasov,
Dr Victor Khomenko,
Professor Maciej Koutny,
Professor Alexander Romanovsky
Full text for this publication is not currently held within this repository. Alternative links are provided below where available.
In this paper, we investigate context aware location-based mobile systems. In particular, we are interested how their behaviour, including fault tolerant aspects, could be captured using a formal semantics, which would then be suitable for analysis and verification. We propose a new formalism and middleware, called CAMA, which provides a rich environment to test our approach. The approach itself aims at giving CAMA a formal concurrency semantics in terms of a suitable process algebra, and then applying efficient model checking techniques to the resulting process expressions in a way which alleviates the state space explosion. The model checking technique adopted in our work is partial order model checking based on Petri net unfoldings, and we use a semantics preserving translation from the process terms used in the modelling of CAMA to a suitable class of high-level Petri nets.
Author(s): Iliasov A, Khomenko V, Koutny M, Romanovsky A
Editor(s): Butler, M., Jones, C., Romanovsky, A., Troubitsyna, T.
Publication type: Conference Proceedings (inc. Abstract)
Publication status: Published
Conference Name: Rigorous Engineering of Fault Tolerant Systems (REFT)
Year of Conference: 2005
ISSN: 0302-9743 (Print) 1611-3349 (Online)
Publisher: Springer Berlin / Heidelberg
Notes: Book title: Rigorous Development of Complex Fault-Tolerant Systems. Proceedings (including this article) also posted at:
Technical Report Series, CS-TR-915
Library holdings: Search Newcastle University Library for this item
Series Title: Lecture Notes in Computer Science