Verifying Semantic Relations in SPIN
Hakan Erdogmus · NPARC · 2002
Introduction Spine is an experimental verification system based on Promela/Spin version 1.5.7. Spin is a general verification tool for proving correctness properties of concurrent/distributed systems specified in the CSP-like modeling language Promela [8, 9]. This extended abstract describing the Spine system and its foundations assumes familiarity with Promela/Spin. The Spine system extends Spin with `limited' semantic relation checking capability implemented in terms of a new option, -e, whose usage is given below: spine -eRel fileL fileR Here Rel indicates the particular semantic relation (usually a preorder or an equivalence) to be verified 1 and fileL and fileR are two files containing the Promela models t