SPHIN: A model checker for reconfigurable hybrid systems based on SPIN

We present SPHIN, a model checker for reconfigurable hybrid systems based on the model checker SPIN. We observe that physical (analog) mobility can be modeled in the same way as logical (discrete) mobility is modeled in the π-calculus by means of channel name passing. We chose SPIN because it supports channel name passing and can model reconfigurations. We extend the syntax of PROMELA and the verification algorithms based on the expected semantics. We demonstrate the tool's capabilities by modeling and verifying a reconfigurable hybrid system.