Using a coordination language to specify and analyze systems containing mobile components
- 1 April 2000
- journal article
- Published by Association for Computing Machinery (ACM) in ACM Transactions on Software Engineering and Methodology
- Vol. 9 (2), 167-198
- https://doi.org/10.1145/350887.350893
Abstract
New computing paradigms for network-aware applications need specification languages able to deal with the features of mobile code-based systems. A coordination language provides a formal framework in which the interaction of active entities can be expressed. A coordination language deals with the creation and destruction of code or complex agents, their communication activites, as well as their distribution and mobility in space. We show how the coordination language PoliS offers a flexible basis for the description and the automatic analysis of architectures of systems including mobile entities. Polis is based on multiple tuple spaces and offers a basis for defining, studying, and controlling mobility as it allows decoupling mobile entities from their environments both in space and in time. The pattern-matching mechanism adopted for communication helps in abstracting from addressing issues. We have developed a model-checking technique for the automatic analysis of PoliS specifications. In the article we show how this technique can be applied to mobile code-based systemsKeywords
This publication has 22 references indexed in Scilit:
- Mobile ambientsTheoretical Computer Science, 2000
- A logic for a coordination model with multiple spacesScience of Computer Programming, 1998
- Context constraints for compositional reachability analysisACM Transactions on Software Engineering and Methodology, 1996
- Coordination models and languages as software integratorsACM Computing Surveys, 1996
- Experiences with software specification and verification using LP, the Larch proof assistantFormal Methods in System Design, 1996
- Itinerant agents for mobile computingIEEE Wireless Communications, 1995
- Vision, issues, and architecture for nomadic computing [and communications]IEEE Wireless Communications, 1995
- Symbolic model checking: 1020 States and beyondInformation and Computation, 1992
- The chemical abstract machineTheoretical Computer Science, 1992
- Automatic verification of finite-state concurrent systems using temporal logic specificationsACM Transactions on Programming Languages and Systems, 1986