Efficient model checking of properties of a distributed application: a multimedia case study
Nicola Mazzocca, Antonella Santone, Gigliola Vaglini, Valeria Vittorini · Software Testing Verification and Reliability · 2001
Abstract 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.