Loading...
Please wait, while we are loading the content...
Similar Documents
Implementing and Verifying Scenario-Based Specifications Using Promela/XSpin : Extended Abstract
| Content Provider | Semantic Scholar |
|---|---|
| Author | Leue, Stefan Ladkin, Peter B. |
| Copyright Year | 1996 |
| Abstract | In previous work we de ned a nite state semantics for Message Sequence Charts (MSCs) and suggested a translation of MSC speci cations into Promela. We call this translation an `implementation'. In this paper we reconsider the implementation of MSCs and discuss what information needs to be added when implementingMSC speci cations containing so-called nonlocal choices. Next, we show how to model-check liveness requirements imposed on MSC specications. We use the Promela models obtained from our implementation, describe how to use control state propositions based on these models, use Linear Time Temporal Logic formulas to specify the liveness properties, and demonstrate the use of XSpin as a model checker for these properties. |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://www.inf.uni-konstanz.de/soft/research/publications/pdf/spin96.pdf |
| Alternate Webpage(s) | https://kops.uni-konstanz.de/bitstream/handle/123456789/5462/Implementing_and_Verifying_Scenario_Based_Specifications_Using_Promela.pdf?isAllowed=y&sequence=1 |
| Alternate Webpage(s) | http://spinroot.com/spin/symposia/ws96/Le.pdf |
| Alternate Webpage(s) | http://www.uni-konstanz.de/soft/research/publications/pdf/spin96.pdf |
| Alternate Webpage(s) | http://spinroot.com/spin/Workshops/ws96/Le.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |