Static analysis of formal, high-level specifications of safety critical software can discover flaws in the specification that would escape conventional syntactic and semantic analysis. As an example, specifications written in the Requirements State Machine Language (RSML) should be checked for consistency: two transitions out of the same state that are triggered by the same event should have mutually exclusive guarding conditions. The check uses only behavioral information that is local to a small set of states and transitions.

However, since only local behavior is analyzed, information about the behavior of the surrounding system is missing. The check may consequently produce counterexamples for state combinations that are not possible when the behavior of the whole system is taken into account. A solution is to identify invariants of the global system that can be used to exclude the impossible state combinations. Manually deriving invariants from designs of realistic size is laborious and error-prone. Finding them by mechanically enumerating the state space is computationally infeasible. The challenge is to find approximate methods that can find fewer but adequate invariants from abstracted models of specifications.

We present an algorithm for deriving invariants that are used to exclude impossible counterexamples resulting from checking consistency of transitions in RSML. The algorithm has been implemented in an RSML prototype tool and has been applied successfully to the static checking of version 6.04a of the (air) Traffic alert and Collision Avoidance System (TCAS II) specification.