Loading...
Please wait, while we are loading the content...
Similar Documents
The Application of Model-checking to Veriication Problems in Telephone Switching Systems
| Content Provider | Semantic Scholar |
|---|---|
| Author | Reii, Stephan Calder, Muuy |
| Abstract | Model-checking is becoming very popular for automated reasoning about hardware and software. The input can be in any language provided there is a translation to transition systems or Kripke structures; properties are then expressed in a temporal logic. Telephone switching systems are concurrent systems which are naturally described by a composition of interacting nite automata. We describe a model of one switching system in IO-Automata, express it in Promela (process meta language) and then formulate certain properties in LTL (linear temporal logic). Using the model-checker Spin, we have attempted to verify the model with respect to some properties. A particular challenge is that even a simple switching system leads to state space explosion. |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://www.dcs.gla.ac.uk/~sreiff/publications/aisb.ps.gz |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
