ReSpecT Nets: Towards an Analysis Methodology for ReSpecT Specifications


Mirko Viroli, Andrea Omicini

A key feature for infrastructures providing coordination services is the ability to define the behaviour of coordination abstractions according to the requirements identified at design-time. We take as a representative for this scenario the logic-based language ReSpecT (Reaction Specification Tuples), used to program the reactive behaviour of tuple centres. ReSpecT specifications are at the core of the engineering methodology underlying the TuCSoN infrastructure, and are therefore the "conceptual place" where formal methods can be fruitfully applied to guarantee relevant system properties.

In this paper we introduce ReSpecT nets, a formalism that can be used to describe reactive behaviours that can succeed and fail, and that allows for an encoding to Petri nets with inhibitor arcs. ReSpecT nets are introduced to give a core model to a fragment of the ReSpecT language, and to pave the way for devising an analysis methodology including formal verification of safety and liveness properties. In particular, we provide a semantics to ReSpecT specifications through a mapping to ReSpecT nets. The potential of this approach for the analysis of ReSpecT specifications is discussed, presenting initial results for the analysis of safety properties.

(keywords) Tuple spaces, ReSpecT, Tuple centres, Petri nets, Formal analysis

Proceedings of the Third International Workshop on Foundations of Coordination Languages and Software Architectures (FOCLASA 2004), Electronic Notes in Theoretical Computer Science 180(2), pp. 123-144, June 2007.
Antonio Brogi, Jean-Marie Jacquet, Ernesto Pimentel (a cura di), Elsevier Science B.V..
3rd International Workshop on Foundations of Coordination Languages and Software Architectures (FOCLASA'04), CONCUR'04, London, UK, 30 August 2004. Post-proceedings

@article{respect-entcs180,
Author = {Viroli, Mirko and Omicini, Andrea},
Doi = {10.1016/j.entcs.2006.10.049},
Editor = {Brogi, Antonio and Jacquet, Jean-Marie and Pimentel, Ernesto},
Issn = {1571-0661},
Journal = {Electronic Notes in Theoretical Computer Science},
Keyword = {Tuple spaces, {\sf {ReSpecT}}, Tuple centres, {P}etri nets, Formal analysis},
Month = jun,
Note = {3rd International Workshop on Foundations of Coordination Languages and Software Architectures (FOCLASA'04), CONCUR'04, London, UK, 30~} # aug # {~2004. Post-proceedings},
Number = 2,
Pages = {123--144},
Publisher = {Elsevier Science B.V.},
ScopusId = {2-s2.0-34250167192},
Title = {{{\sf ReSpecT}} Nets: Towards an Analysis Methodology for {{\sf ReSpecT}} Specifications},
Url = {http://www.sciencedirect.com/science/article/pii/S1571066107003258},
Volume = 180,
Year = 2007}

Riviste & collane

Tags: ReSpecT

Pubblicazione

— autori/autrici

Mirko Viroli, Andrea Omicini

— a cura di

Antonio Brogi, Jean-Marie Jacquet, Ernesto Pimentel

— stato

pubblicato

— tipo

articolo in atti

Sede di pubblicazione

— volume

Proceedings of the Third International Workshop on Foundations of Coordination Languages and Software Architectures (FOCLASA 2004)

— collana

Electronic Notes in Theoretical Computer Science 180

— data di pubblicazione

June 2007

— pagine

123-144

— collana

Electronic Notes in Theoretical Computer Science 180

— data di pubblicazione

June 2007

URL & ID

pagina originale

— DOI

10.1016/j.entcs.2006.10.049

— Scopus

2-s2.0-34250167192

— print ISSN

1571-0661

BibTeX

— BibTeX ID
respect-entcs180
— BibTeX category
article

Partita IVA: 01131710376 - Copyright © 2008-2021 APICe@DISI Research Group - PRIVACY