Diagrams for Dataflow

The behavior of reactive systems can be described by their black box properties as a relation between input and output streams. More operational is the behavior's description by state machines. While the first view enjoys easy compositionality, the second leads directly to implementations. In this paper we show how these two views can be integrated by offering a technique for proving that a state machine indeed has specified safety and liveness properties. We use graphical description techniques both for specifying the state machines and for structuring the proofs, and sketch how theorem provers help to generate and discharge resulting proof obligations.

• Type: Conference
• Year: 2000
• Where: FBT
• Authors: Max Breitling, Jan Philipps
• Keywords: Black Box Properties, FBT 2000, Formal Methods, State Machines, Theorem Provers Help