caa a22 4500 605516200 CHVBK 20210128100713.0 cr unu---uuuuu 210128e20150501xx s 000 0 eng 10.1007/s00165-014-0324-9 doi (NATIONALLICENCE)springer-10.1007/s00165-014-0324-9 Strategy based semantics for mobility with time and access permissions [Elektronische Daten] [Gabriel Ciobanu, Maciej Koutny, Jason Steggles] 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. British Computer Society, 2014 Process algebra nationallicence Mobility nationallicence Time nationallicence Access permissions nationallicence Rewriting Logic nationallicence Strategies nationallicence Ciobanu Gabriel Romanian Academy, Institute of Computer Science, Iaşi, Romania aut Koutny Maciej School of Computing Science, University of Newcastle, Newcastle, UK aut Steggles Jason School of Computing Science, University of Newcastle, Newcastle, UK aut Formal Aspects of Computing Springer London 27/3(2015-05-01), 525-549 0934-5043 27:3<525 2015 27 165 https://doi.org/10.1007/s00165-014-0324-9 text/html Onlinezugriff via DOI BK010053 XK010053 XK010000 Metadata rights reserved Springer special CC-BY-NC licence nationallicence 1 research-article jats NATIONALLICENCE NATIONALLICENCE NL-springer NATIONALLICENCE 856 40 https://doi.org/10.1007/s00165-014-0324-9 text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Ciobanu Gabriel Romanian Academy, Institute of Computer Science, Iaşi, Romania aut NATIONALLICENCE 700 1- Koutny Maciej School of Computing Science, University of Newcastle, Newcastle, UK aut NATIONALLICENCE 700 1- Steggles Jason School of Computing Science, University of Newcastle, Newcastle, UK aut NATIONALLICENCE 773 0- Formal Aspects of Computing Springer London 27/3(2015-05-01), 525-549 0934-5043 27:3<525 2015 27 165