Automatic symmetry detection for Promela We introduce a specification language, Promela-Lite, which captures the essential features of Promela but which, unlike Promela, has a formally defined semantics. We show how we can detect symmetry in specifications defined in Promela-lite by constructing a directed, coloured bipartite digraph called a static channel diagram, and applying computational group theoretic techniques. We extend our approach to Promela and introduce a tool, SymmExtractor, for automatically detecting symmetries of Promela specifications. We demonstrate the effectiveness of our approach via experimental results for a suite of Promela specifications. Unlike previous approaches our technique is fully automatic, and not restricted to fully symmetric systems.
Keywords for this software
References in zbMATH (referenced in 2 articles )
Showing results 1 to 2 of 2.
- Donaldson, Alastair F.; Kaiser, Alexander; Kroening, Daniel; Tautschnig, Michael; Wahl, Thomas: Counterexample-guided abstraction refinement for symmetric concurrent programs (2012)
- Donaldson, Alastair F.; Miller, Alice: Automatic symmetry detection for Promela (2008)