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 Automatic verification

• Type: Journal
• Year: 2008
• Where: JAR
• Authors: Alastair F. Donaldson, Alice Miller
• Keywords: JAR 2008, Promela, Promela Specifications, Specifications