Stochastic Model Checking of the Stochastic Quality Calculus

Research output: Chapter in Book/Report/Conference proceedingBook chapterResearchpeer-review

Abstract

The Quality Calculus uses quality binders for input to express strategies for continuing the computation even when the desired input has not been received. The Stochastic Quality Calculus adds generally distributed delays for output actions and real-time constraints on the quality binders for input. This gives rise to Generalised Semi-Markov Decision Processes for which few analytical techniques are available.
We restrict delays on output actions to be exponentially distributed while still admitting real-time constraints on the quality binders. This facilitates developing analytical techniques based on stochastic model checking and we compute closed form solutions for a number of interesting scenarios. The analyses are applied to the design of an intelligent smart electrical meter of the kind to be installed in European households by 2020.
Original languageEnglish
Title of host publicationSoftware, Services, and Systems : Essays Dedicated to Martin Wirsing on the Occasion of His Retirement from the Chair of Programming and Software Engineering
EditorsRocco De Nicola, Rolf Hennicker
PublisherSpringer
Publication date2015
Pages522-537
ISBN (Print)978-3-319-15544-9
ISBN (Electronic)978-3-319-15545-6
DOIs
Publication statusPublished - 2015
SeriesLecture Notes in Computer Science
Volume8950
ISSN0302-9743

Cite this

Nielson, F., Nielson, H. R., & Zeng, K. (2015). Stochastic Model Checking of the Stochastic Quality Calculus. In R. De Nicola, & R. Hennicker (Eds.), Software, Services, and Systems: Essays Dedicated to Martin Wirsing on the Occasion of His Retirement from the Chair of Programming and Software Engineering (pp. 522-537). Springer. Lecture Notes in Computer Science, Vol.. 8950 https://doi.org/10.1007/978-3-319-15545-6_30