Premium
Efficient model checking of properties of a distributed application: a multimedia case study
Author(s) -
Mazzocca Nicola,
Santone Antonella,
Vaglini Gigliola,
Vittorini Valeria
Publication year - 2002
Publication title -
software testing, verification and reliability
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.216
H-Index - 49
eISSN - 1099-1689
pISSN - 0960-0833
DOI - 10.1002/stvr.222
Subject(s) - concurrency , workbench , computer science , model checking , property (philosophy) , basis (linear algebra) , process (computing) , programming language , temporal logic , theoretical computer science , calculus (dental) , distributed computing , artificial intelligence , mathematics , visualization , medicine , philosophy , geometry , dentistry , epistemology
A system supporting video on demand is modeled in the process calculus CCS (Calculus of Communicating Systems), while some properties are expressed in a temporal logic and verified by means of the model checkers of the North Carolina Concurrency Workbench. This application was chosen as a case study to evaluate the usefulness of a methodology, by means of which a property is checked on reduced models obtained issuing abstractions of the system on the basis of the formula. Experimental results are shown and discussed. Copyright © 2001 John Wiley & Sons, Ltd.