Browse by author
Lookup NU author(s): Professor Gabriel Ciobanu, Professor Maciej KoutnyORCiD, Dr Jason Steggles
This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License (CC BY-NC 4.0).
The process algebras Timed Mobility (TiMo) and its extension Permissions, Timers and Mobility (PerTiMo) were recently proposed to support engineering applications in distributed system design. TiMo provides a formal framework in which process migration between distinct locations and timing constraints linked to local clocks can be modelled and analysed. This is extended in PerTiMo by associating access permissions to communication to model security aspects of a distributed system. In this paper we develop a new semantic model for TiMo using Rewriting Logic (RL) and strategies, with the aim of providing a foundation for tool support; in particular, strategies are used to capture the locally maximal concurrent step of a TiMo specification which previously required the use of action rules based on negative premises. This RL model is then extended with access permissions in order to develop a new semantic model for PerTiMo. These RL semantical models are formally proved to be sound and complete with respect to the original operational semantics on which they were based. We present examples of how the developed RL models for TiMo and PerTiMo can be implemented within the strategy-based rewriting system Elan and illustrate the range of (behavioural) properties that can be analysed using such a tool.
Author(s): Ciobanu G, Koutny M, Steggles J
Publication type: Article
Publication status: Published
Journal: Formal Aspects of Computing
Year: 2015
Volume: 27
Issue: 3
Pages: 525-549
Print publication date: 01/05/2015
Online publication date: 09/12/2014
Acceptance date: 26/10/2014
Date deposited: 16/12/2014
ISSN (print): 0934-5043
ISSN (electronic): 1433-299X
Publisher: Springer
URL: http://dx.doi.org/10.1007/s00165-014-0324-9
DOI: 10.1007/s00165-014-0324-9
Altmetrics provided by Altmetric
