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.
My Menu
Saved Items

On the Verification of Coordination

Paul DecheringContact Information and Izak van LangeveldeContact Information

(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”

Contact Information Paul Dechering
Email: paul@dechering.net

Contact Information Izak van Langevelde
Email: izak@cwi.nl
Fulltext Preview (Small, Large)
Image of the first page of the fulltext

References secured to subscribers.



Export this chapter
Export this chapter as RIS | Text
 
Remote Address: 38.107.191.105 • Server: MPWEB25
HTTP User Agent: CCBot/1.0 (+http://www.commoncrawl.org/bot.html)