Further steps towards efficient runtime verification: handling probabilistic cost models
File(s)
Accepted version
Author(s)
Filieri, A
Ghezzi, C
Type
Conference Paper
Abstract
We consider high-level models that specify system behaviors probabilistically and support the specification of cost attributes. Specifically, we focus on Discrete Time Markov Reward Models (D-MRMs), i.e. state machines where probabilities can be associated with transitions and rewards (costs) can be associated with states and transitions. Through probabilities we model assumptions on the behavior of environment in which an application is embedded. Rewards can instead model the cost assumptions involved in the system's operations. A system is designed to satisfy the requirements, under the given assumptions. Design-time assumptions, however, can turn out to be invalid at runtime, and therefore it is necessary to verify whether changes may lead to requirements violations. If they do, it is necessary to adapt the behavior in a self-healing manner to continue to satisfy the requirements. We have previously presented an approach to support efficient runtime probabilistic model checking of DTMCs for properties expressed in PCTL. In this paper we extend the approach to D-MRMs and reward properties. The benefits of the approach are justified both theoretically and empirically on significant test cases.
Date Issued
2012-06-02
Date Acceptance
2012-06-02
Citation
Formal Methods in Software Engineering: Rigorous and Agile Approaches, 2012, pp.2-8
ISBN
978-1-4673-1907-2
Publisher
IEEE
Start Page
2
End Page
8
Journal / Book Title
Formal Methods in Software Engineering: Rigorous and Agile Approaches
Copyright Statement
© 2012 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works.
Source
Formal Methods in Software Engineering: Rigorous and Agile Approaches
Publication Status
Published
Start Date
2012-06-02
Finish Date
2012-06-02
Coverage Spatial
Zurich, Switzerland