A transformational method for verifying safety properties in real-time systems

A two-step method is presented for verifying that safety properties are not violated by an HMS (hierarchical multistate) specification of a system. In the first step, the question of safety verification is recast as a reachability problem in an extension of the HMS machine. In the second step, reachability is determined by the use of correctness-preserving and partial correctness-preserving transformations. The method is shown to be complete, and it is illustrated by verifying that a safety property holds for a simple railroad-crossing system if all of its deadlines are met