spine -eRel fileL fileRHere Rel indicates the particular semantic relation (usually a preorder or an equivalence) to be verified (trace inclusion, trace equivalence, testing equivalence), and fileL and fileR are two files containing the PROMELA models to be compared.
An efficient algorithm translates LTL formulae directly into PROMELA's never claims, allowing immediate automatic verification by SPIN. Although in general the translation gives an exponential automaton, the algorithm performs quite well on the temporal formulas typically encountered in verification.
We describe the new version of SPIN which incorporates a partial order reduction technique. Experimental results show significant reductions. The partial order reduction affects how a subset of the successors are selected from each state, to guarantee that at least one sequence per equivalence class is generated. Care is taken to minimize the time and space used to calculate these subsets. Thus, achieving the reduction with least overhead. The reduction algorithm preserves safety and liveness properties of LTL. Parts of the reduction algorithm have been formally verified using the theorem prover HOL.
From the ultimate specification two different implementations are derived. The first one is in Synchronous C++, a concurrent extension of C++, and the second is in Regis/Darwin. This application shows that SPIN is quite appropriate for developing control process problem from scratch and with requirements to be checked in mind. It appeared clearly that the specification phase was very important for obtaining a satisfactory specification from which a well behaved implementation was derived easily in a few days.
Return toIndex of Spin Newsletters