Loading...
Please wait, while we are loading the content...
Similar Documents
Using the theorem prover setheo for verifying the development of a communication protocol in focus - a case study (1995).
| Content Provider | CiteSeerX |
|---|---|
| Author | Schumann, Johann |
| Abstract | . This paper describes experiments with the automated theorem prover SETHEO. The prover is applied to proof tasks which arise during formal design and specification in Focus. These proof tasks originate from the formal development of a communication protocol (Stenning protocol). Its development and verification in Focus is described in "C. Dendorfer, R. Weber: Development and Implementation of a Communication Protocol -- An Exercise in Focus" [DW92a]. A number of propositions of that paper deal with safety and liveness properties of the Stenning protocol on the level of traces. All given propositions and lemmata could be proven automatically using the theorem prover SETHEO. This paper gives a short introduction into the proof tasks as provided in [DW92a]. All steps which were necessary to apply SETHEO to the given proof tasks (transformation of syntax, axiomatization) will be described in detail. The surprisingly good results obtained by SETHEO will be presented, and adv... |
| File Format | |
| Publisher Date | 1995-01-01 |
| Access Restriction | Open |
| Subject Keyword | Communication Protocol Theorem Prover Setheo Proof Task Focus Case Study Stenning Protocol Formal Design Formal Development Good Result Short Introduction Automated Theorem Prover Setheo Liveness Property Focus Dw92a Paper Deal |
| Content Type | Text |
| Resource Type | Article |
