Expression caching for runtime verification based on parameterized probabilistic models

• Published in: The Journal of systems and software 2019-10, Vol.156, p.300-311
• Main Authors: Nakagawa, Hiroyuki, Toyama, Hiromu, Tsuchiya, Tatsuhiro
• Format: Article
• Language: English
• Subjects: Caching; Discrete time Markov chain; Probabilistic model checking; Runtime verification; Self-adaptive systems
• ISSN: 0164-1212; 1873-1228
• DOI: 10.1016/j.jss.2019.07.007

•Expansion of efficient runtime verification mechanism by using caching mechanism.•Parameterization efficiently works for reducing the computational time of runtime verification.•Experiments on randomly generated DTMC models shows better stability in performance. Self-adaptive software systems change their behaviors to adapt to their environmental changes at runtime. Runtime verification, which checks the correctness of behaviors after adaptation, sometimes uses probabilistic model checking, because the verification has to deal with uncertainty. However, since probabilistic model checking is usually computation intensive and time consuming, a more efficient verification mechanism is desired. A possible approach is to pre-generate some expressions for model checking at design time and execute model checking simply by evaluating the expressions at runtime. A problem with this approach is that when environmental changes require changes of the system model, these expressions need to be re-generated at runtime. In order to cope with such significant changes, we develop a caching mechanism that reduces computational time at runtime. We also introduce a parameterization technique in order to improve the efficiency of caching. The experimental results show that our new implementation of the caching mechanism greatly improves the computational time of runtime verification.