Name
Abstract | ||
|---|---|---|
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 rst view enjoys easy compositionality, the second leads directly to implementations. In this paper we show how these two views can be integrated by oering a technique for proving that a state machine indeed has specied 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. |
Year | Venue | Keywords |
|---|---|---|
2000 | FBT | state machine,theorem prover,reactive system |
Field | DocType | Citations |
Programming language,Theoretical computer science,Dataflow,Mathematics | Conference | 6 |
PageRank | References | Authors |
0.60 | 8 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Max Breitling | 1 | 29 | 2.81 |
| Jan Philipps | 2 | 162 | 16.45 |