Model-checking performability properties


Share/Save/Bookmark

Haverkort, Boudewijn and Cloth, Lucia and Hermanns, Holger and Katoen, Joost-Pieter and Baier, Christel (2002) Model-checking performability properties. In: International IEEE Conference on Dependable Systems and Networks, DSN, 23-26 June 2002, Bethesda, MD, USA.

[img]PDF
Restricted to UT campus only
: Request a copy
166Kb
Abstract:Model checking has been introduced as an automated technique to verify whether functional properties, expressed in a formal logic like computational tree logic (CTL), do hold in a formally-specified system. We present a number of computational procedures to perform model checking of continuous stochastic reward logic (CSRL) over finite Markov reward models, thereby stressing their computational complexity (time and space) and applicability from a practical point of view (accuracy, stability). A case study in the area of ad hoc mobile computing under power constraints shows the merits of CSRL and the new computational procedures.
Item Type:Conference or Workshop Item
Copyright:© 2002 IEEE
Faculty:
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/63324
Official URL:http://dx.doi.org/10.1109/DSN.2002.1028891
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page