Loading...
Please wait, while we are loading the content...
Similar Documents
Using Setheo for Verifying a Communication Protocol in Focus | a Case Study |
| Content Provider | Semantic Scholar |
|---|---|
| Author | Schumann, Johann |
| Copyright Year | 2007 |
| Abstract | This paper describes experiments with the automated theorem prover SETHEO. The prover is applied to proof tasks which arise during formal design and speciication in FOCUS. This case study is based on the formal development of a communication protocol (Stenning protocol). Its development and veriication in FOCUS is described in \C. Dendorfer, R. Weber: Development and Implementation of a Communication Protocol { An Exercise in FOCUS" DW92]. 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 SETHEO system and the proof tasks as provided in DW92]. All steps which were necessary to apply SETHEO to the given proof tasks (formalization, axiomatization) will be described in detail. The surprisingly good results obtained by SETHEO will be presented, and advantages and problems using an automated theorem prover for such applications, as well as possibly ways for improvements will be discussed. All formulae are listed in the appendix. |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://wwwjessen.informatik.tu-muenchen.de/~schumann/focus-tr.ps.gz |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
