Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
|
 |
On the Verification of Coordination
| |
|
On the Verification of Coordination
Paul Dechering6 and Izak van Langevelde7 
| (6) |
Hollandse Signaalapparaten B.V., P.O. Box 42, 7550 GD Hengelo, The Netherlands |
| (7) |
Centrum voor Wiskunde en Informatica, P.O. Box 94079, 1090 GB Amsterdam, The Netherlands |
Abstract
Scenario-based verification is introduced as a technique to deal with the complexity of coordination languages, which feature
both data manipulation and concurrency. The approach is exemplified by a verification study of the software architecture Splice that is used by Hollandse Signaalapparaten. A detailed specification of Splice, including the Ethernet network that Splice is using, is written in the process-algebraic language μcrl and for a number of selected scenarios the transition system
is automatically generated. For the resulting models, the properties of deadlock freeness, soundness, and weak completeness
are automatically proven by model checking.
Supported by ORKEST: “Onderzoek naar Randvoorwaarden voor de Konstruktie van Embedded SysTemen”
Fulltext Preview (Small, Large)
 References secured to subscribers.
|
|
|
|
|
|