Static analysis of formal, high-level specifications of safety critical software can discovery flaws in the specification that would escape conventional syntactic and semantic analysis. As an exmaple, specifications written in the Reuqirements 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.
展开▼
