Research Article
A Formalization of the SMEPP Model in Maude
@INPROCEEDINGS{10.4108/ICST.MOBIQUITOUS2008.3916, author={Francisco Dur\^{a}n and Francisco Guti\^{e}rrez and Pablo L\^{o}pez and Ernesto Pimentel}, title={A Formalization of the SMEPP Model in Maude}, proceedings={1st International ICST Workshop on Middleware for Mobile Embedded Peer-to-Peer Systems}, publisher={ACM}, proceedings_a={MIMES}, year={2010}, month={5}, keywords={Peer-to-Peer Systems Service-Oriented Models Formal Semantics Automated Verification}, doi={10.4108/ICST.MOBIQUITOUS2008.3916} }- Francisco Durán
Francisco Gutiérrez
Pablo López
Ernesto Pimentel
Year: 2010
A Formalization of the SMEPP Model in Maude
MIMES
ICST
DOI: 10.4108/ICST.MOBIQUITOUS2008.3916
Abstract
This paper introduces a service-oriented model for the description of embedded Peer-to-Peer (EP2P) systems and formalizes the proposed model in Maude. The model is organized around the notions of groups of peers and services offered by these groups. We first summarize the main concepts of the model and then present aSMoL, an abstract language with a formal semantics that provides a solid ground to develop tools for the automated analysis and verification of EP2P specifications. We then describe a formalization of aSMoL in Maude, and introduce an example to illustrate both the expressive power of the model and the possibilities of Maude to support automated verification of properties of aSMoL programs.
Copyright © 2008–2024 ICST
