Model-checking performability properties

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.

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:	Design and Analysis of Communication Systems (DACS) Formal Methods and Tools (FMT)
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