Spin-to-Grape
Spin-to-Grape: a tool for analysing symmetry in Promela models We provide two examples of Promela models of concurrent, distributed systems, whose associated Kripke structures have more complex symmetry groups than those of models commonly cited in the literature. We present a tool, Spin-to-Grape, which allows the state-graph of a Promela model to be manipulated using the group-theoretic package Gap and its graph-theoretic add on, Grape. Through studying these examples we show a correspondence between the symmetry group of the channel diagram of a system and the symmetry group of the Kripke structure associated with the system. We then identify some general classes of systems and describe the symmetry groups of the associated models. Finally we discuss ways in which symmetry reduction techniques incorporated within Spin, e.g., the SymmSpin package, could be extended to exploit symmetry in such models.
This software is also peer reviewed by journal TOMS.
This software is also peer reviewed by journal TOMS.
Keywords for this software
References in zbMATH (referenced in 8 articles , 1 standard article )
Showing results 1 to 8 of 8.
Sorted by year (- Jaghoori, Mohammad Mahdi; Sirjani, Marjan; Mousavi, Mohammad Reza; Khamespanah, Ehsan; Movaghar, Ali: Symmetry and partial order reduction techniques in model checking Rebeca (2010)
- Leuschel, Michael; Massart, Thierry: Efficient approximate verification of B and Z models via symmetry markers (2010)
- Donaldson, Alastair F.; Miller, Alice: On the constructive orbit problem (2009)
- Miller, A.; Calder, M.; Donaldson, A.F.: A template-based approach for the generation of abstractable and reducible models of featured networks (2007)
- Donaldson, Alastair F.; Miller, Alice; Calder, Muffy: SPIN-to-grape: A tool for analysing symmetry in promela models. (2005)
- Donaldson, Alastair F.; Miller, Alice; Calder, Muffy: Finding symmetry in models of concurrent systems by static channel diagram analysis. (2005)
- Donaldson, Alastair F.; Miller, Alice; Calder, Muffy: Finding symmetry in models of concurrent systems by static channel diagram analysis (2005)
- Donaldson, Alastair; Miller, Alice; Calder, Muffy: Spin-to-Grape: a tool for analysing symmetry in Promela models (2005)