Towards a Formal Framework for Mobile, Service-Oriented Sensor-Actuator Networks

Helena Gruhn
Sabine Glesner

Service-oriented sensor-actuator networks (SOSANETs) are deployed in health-critical applications like patient monitoring and have to fulfill strong safety requirements. However, a framework for the rigorous formal modeling and analysis of SOSANETs does not exist. In particular, there is currently no support for the verification of correct network behavior after node failure or loss/addition of communication links. To overcome this problem, we propose a formal framework for SOSANETs. The main idea is to base our framework on the π-calculus, a formally defined, compositional and well-established formalism. We choose KLAIM, an existing formal language based on the π-calculus as the foundation for our framework. With that, we are able to formally model SOSANETs with possible topology changes and network failures. This provides the basis for our future work on prediction, analysis and verification of the network behavior of these systems. Furthermore, we illustrate the real-life applicability of this approach by modeling and extending a use case scenario from the medical domain.

In Barbora Buhnova, Lucia Happe and Jan Kofroň: Proceedings 10th International Workshop on Formal Engineering Approaches to Software Components and Architectures (FESCA 2013), Rome, Italy, March 23, 2013, Electronic Proceedings in Theoretical Computer Science 108, pp. 49–62.
Published: 20th February 2013.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: