-For software systems that need to adapt to their environment at run-time, run-time verification is useful to guarantee the correctness of their behaviors. Probabilistic model checking using discrete time Markov chain (DTMC) model has been applied to implement run-time verification. A current existing approach provides an efficient run-time verification mechanism by pre-generating expressions for model checking at design time. In case that a system model is changed, the system is required to re-generate the expressions. In order to expand the applicability of the approach, we propose three strategies, caching, prediction, and reduction, for reducing computational time for re-generated expressions at run-time. We conduct preliminary experiments and demonstrate that our approach could expand the applicability of run-time verification by reducing the computational cost at runtime.
Software systems are often required to be able to
maintain high performance and high reliability even though their
environments are changeable or uncertain at design time.
Traditional software systems are difficult to demonstrate the
best performance or even run correctly under their
changeable or uncertain environments. Constructing systems as
selfadaptive systems [
Unlike verification techniques at design-time, run-time
verification techniques should be efficiently executed not to
degrade system performance. Some studies on efficient
verification for self-adaptive systems have been developed. Filieri
et al [
In expression generation, variables in DTMC models,
which represent uncertain transition probabilities, lead to a
large computational cost. DTMC models are represented as
matrices, and the expression generation requires the
computation of determinants. The computation of determinants is
performed by using Laplace expansion and LU-decomposition.
We previously evaluated the computational cost for
generating expressions and concluded that the number of times
of performing Laplace expansions considerably affects the
computational cost [
In this study, we aim to expand the applicability of the efficient run-time verification technique by reducing the computational time for executing Laplace expansions. We reuse intermediate expressions obtained in pre-computation. Our approach is on the basis of caching. We store pairs of a partial matrix in DTMC and the corresponding intermediate expression as key-value pairs into cache. Moreover, to increase cache hit ratio and decrease cache size, we apply additional strategies, prediction and reduction.
We conduct preliminary experiments on randomly generated DTMC models. The experimental results demonstrate that our approach could expand the applicability of run-time verification by reducing the computational cost at run-time while keeping from rapidly increasing memory usage.
This paper is organized as follows: Section II describes theoretical background of our study. Section III explains our approach for an efficient run-time verification with three strategies. Section IV evaluates our approach from preliminary experimental results. Section V presents related work, and Section VI concludes this paper.
Since systems that need to adapt to their environment
have to face uncertainty, we deal with the systems under
development as probabilistic systems. In many cases, behaviors
of such systems are described in Discrete Time Markov Chain
(DTMC) [
Figure 1 illustrates an efficient run-time verification process
that Filieri et al. proposed in [
A DTMC model is a state transition diagram that has state transitions represented as probabilities. DTMC is a stochastic process [14] that has transitions from one state to another state on a state space. DTMC must respect the following property of Markov chains: the probability distribution of the next state depends only on the current state and not on the sequence of events that preceded the current state. We consider finite and time-homogeneous DTMC models, i.e., where the state space is finite and transition probabilities between states do not change with time, in this paper.
V
ݔ 1 െ ݔ ଵ
V 1 െ ݔ ସ
V
Formally, a DTMC is represented as a tuple (S ; S 0; P; L), where S is a set of states; S 0 ( S ) is a set of initial states; P : S S ! [0; 1] is a stochastic matrix, in which an element of P(si; s j) represents the probability that the next state of the process will be s j given the current state is si; L : S ! 2AP is a labeling function, where AP is a set of atomic propositions that represent basic properties. A state s 2 S with P(s; s) = 1 is called an absorbing state. A state that is not an absorbing state is called a transient state. A DTMC is said to be absorbing if it contains at least one absorbing state and from every state it is possible to go to an absorbing state. In order to apply the Filieri’s approach, the DTMC must be absorbing. It should be noted that the approach can sometimes be applied to a non-absorbing DTMC with some modifications to the model. For example, if the DTMC contains an absorbing connected component that has no absorbing state, then replacing the component with an absorbing state yields an alternative DTMC model that is absorbing.
We show an example of a DTMC model in Figure 2. This model represents a behavioral model for a cleaning robot. Since some of the transition probabilities are determined by monitoring the environment at run-time and cannot be determined at design time, these transitions are described as variables. For example, the cleaning robot detects obstacles by using sensors that the robot has and decides a direction to move by using data collected by sensors. The robot moves in different directions by executing going forward and turning commands. Since which sensor is used is adjusted at runtime, transition probabilities to sensing states are represented as variables x0, :::, x3.
A DTMC model can be represented as a matrix. For example, the matrix illustrated in Figure 3 represents the DTMC model of our cleaning robot example (Figure 2). An absorbing DTMC that has r absorbing states and t transient states is represented by the matrix P that is in the following canonical form:
(Q P = O
R) I where I is an r by r identity matrix, O is an r by t zero matrix, R is a t by r nonzero matrix and Q is a t by t matrix. The element qi j of the matrix Q is the transition probability from the transient state si to the transient state s j. The element rik of the matrix R is the transition probability from the transient state si to the absorbing state sk. An absorbing state has probability 1 from the absorbing state to itself. Therefore, the probabilities of absorbing states to themselves are represented as the identity matrix I. Since transition probability from an absorbing state to a transient state is 0, O is a zero matrix.
The transition probability from the transient state si to the transient state s j in two steps is calculated by ∑sx2S P(si; sx) P(sx; s j) = ∑sx2S Q(si; sx) Q(sx; s j). The k-step transition probability, with which the state s j is reached from the state si in k steps, is the element qikj of the matrix Qk. Since the element qi0j (of the matrix Q0) represents the transition probability from the state si to the state s j in zero steps, this matrix Q0 is a t by t identity matrix. Due to the fact that R must be a nonzero matrix, Q has uniform-norm strictly less than 1, thus Qn ! 0 when n ! 1, which implies that eventually the process will be absorbed with probability 1.
The requirements are expressed in probabilistic computational tree logic (PCTL), which can be used to describe the properties of the system. Filieri et al. proposed an efficient approach to verify whether DTMC models satisfy requirements expressed by PCTL. PCTL is an extension of Computational Tree Logic (CTL) that allows probabilistic quantification of described properties. The PCTL formula [11] is defined by the following : φ ::= ::= true j a j X j
U ^ j j : U t j P▷◁p (φ) (2) (3) where a is an atomic proposition. Probabilistic operator P▷◁p (φ) represents whether the expression φ satisfies the constraint ▷◁ p or not, where p 2 [0; 1], ▷◁2 f ; <; ; >g. Operators X and U, which appear in path formulae φ, represent “next” and “until”, respectively. For example, P<0:01(X s = 1) means that the reachability probability from the current state to the next state s1 is less than 0.01.
In Section IV, we conduct an experiment to evaluate our approach by observing the computational time for the determination of reachability property. The reachability property states that a target state is eventually reached from a given initial state. Many safety properties can be checked by reachability property verifications. In most cases, the state to be reached is one of absorbing states. An example of a PCTL formula that represents a reachability property is as follows:
P 0:01(true U s = 6) (= P 0:01(F s = 6)) (4) Expression (4) states that the probability from an initial state to the absorbing state s6 has to be less than 0:01. Since many practical requirements can be specified as the reachability of an absorbing state [15], we focus on the reachability properties in this paper. (1)
As we described, the probability of moving from the transient state si to the absorbing state sk in one step is represented as the element pik of the matrix P. In the case of more than 1 step, we have to compute the probability of the transition from a transient state to another transient state and the transition from the transient state to the destination state. The transition probability in two steps is the element qi2j of the matrix Q2(= Q Q), and the transition probability in k steps is the element qikj (of the matrix Qk). Therefore, the expected number of visits to the transient state s j before arriving at an absorbing state, starting from the state si is the (i; j)-th element of the matrix N = I + Q + Q2 + Q3 + = ∑k1=0 Qk. The probability from the transient state si to the absorbing state sk in some steps is defined as the element bik of the matrix B: The computation for the matrix B requires the computation for the matrix N. We can replace N as follows:
N
I + Q + Q2 + Q3 + = = =
B = N
R 1 ∑ Qk k=0 (I
Q) 1 ni j =
1 det(W) ji(W) where W is I Q, and i j is the cofactor. Using Expression (5) and (7), the element bi j of the matrix is calculated as follows: bik = =
∑ x20:::t 1
1 det(W) nix rx j
∑ x20:::t 1 xi(W) rx j
element ni j of the matrix N as follows:
(5) (6) (7) (8) (9) Here, the computation of bik requires the computation of determinants. Determinants are calculated by applying Laplace expansion [16] and LU-decomposition [17] (Figure 4). Laplace expansion removes variables from a matrix; LUdecomposition, on the other hand, computes determinants of the matrix that contains no variables. The determinant jAj of the n n matrix A is the sum of the product of the element ai j by each determinant of n sub-matrices of A with size (n 1) (n 1). The expression of jAj with the i-th row expanded is as follows: jAj(= det(A)) = n ∑( 1)i+ jai jjA′ji j j=0 Ai′j is the (n 1) (n 1) sub-matrix generated by removing the i-th row and the j-th column of the matrix A.
As we mentioned, the computation of reachability property requires the determinant computation. The determinant computation is executed by using LU-decomposition and Laplace ݔ ଶ 0.7 expansion; while the former requires O(n3) computational cost, the latter requires O(n!), that is, considerably larger computational cost. The rows that include variables representing unknown parameters are expanded by using Laplace expansion. The high number of times of Laplace expansions leads to a huge computational cost. Models of systems that have to deal with uncertain environments, such as self-adaptive systems, usually have variables that are represented as unknown parameters in the matrices. The large number of variables leads to the large number of times of Laplace expansions and large computational time.
III.
The advantage of Filieri’s approach is that it can shift the large computational cost from run-time to design time. This process provides an efficient run-time verification mechanism under the assumption that the structure of the system model, i.e., the DTMC model, is not changed. On the other hand, if the structure is changed, such as states and transitions addition, the pre-computed expressions no longer correspond to the new model.
V 1 െ ݔ 1 െ ݔ ଵ
V 1
1 െ ݔ ସ 1 െ ݔ ଷ *0.9 0.8
For example, Figure 6 shows a model after an adaptation that causes to add state and transitions to the model illustrated in Figure 2. In such a case, the system has to re-execute the pre-computation process at run-time. This re-execution usually requires large computational time. Especially, Laplace expansions in the pre-computation process require a large amount of computational time.
The goal in this paper is to reduce the number of executing Laplace expansions at run-time. Figure 5 illustrates the overview of our approach. In this paper, we propose the following three strategies:
Caching: To avoid the re-execution of Laplace expansion, we store pairs of sub-matrix and the corresponding expression for re-use into the memory (cache). When the system needs to re-generate an expression, it searches for the matrix from the cache. If the system finds it, the matrix is replaced with the stored expression with no calculation.
Prediction: Since a DTMC model is changed by adaptation, the cache hit ratio may be decreased when we search for sub-matrices of the new DTMC model. In order to increase hit ratio of caching, we store additional pairs that are similar to the stored pairs based on the caching strategy.
Reduction: Caching and prediction strategies require an additional memory space. We need to reduce the increase of the required space. In this paper, we try to
0 0.2 0.1 0.5 LRHV[SQD URHW6SLDVIEPX[ 0.01 ݔ ଵ 0 0.9 00.2 0ݔ.ଶ7 00.0.51 0.002 PRGHLQF8SWV/
0.2 0.1 0.5 0 0.1 0.5 = 0.01 ݔ ଶ 0.5 0 0 0.5 0 0.7 0.01 0.02 + ݔ ଵ 0.2 0.01 0.02
0 0.2 0.1 + 0.9 0 ݔ ଶ 0.5
0.2 0.7 0.01 ݔ 000ସ + ݔ ଷ 00.000.21 00ݔݔ..ଵଶ27 000.00..151 000.00..952 0 0.01 0 0.2 0 = 1 െ ݔ ଷ 0.2
In many cases, self-adaptive systems change only a part of their behaviors. Even though the systems requires regeneration of expression for verification at run-time, the most part of the system models are not changed in many cases.
Figure 7 illustrates the caching strategy. We store the pairs of sub-matrix and the corresponding (sub-)expression at design time. Since LU-decomposition does not require the large computational cost, we store the sub-matrices that require Laplace expansion. When the system needs to regenerate expressions at run-time, it searches for the matrix to be processed from the cache. If the system finds the same matrix in the cache, the matrix is replaced with the paired sub-expression.
Effectiveness of caching depends on the size of matrix to be replaced with an expression. Even though we can replace a small size of sub-matrix with the corresponding expression, the improvement of computational cost is limited. We should find as large a size of matrix as possible.
In order to match a large size of matrix, we additionally register matrices that are similar to the matrix representing the system model before adaptation.
In this paper, we focus on the behavioral changes such that new states and transitions are added. For example, the model shown in Figure 6 is an example of such cases. Figure 8 is the corresponding matrix. The prediction strategy makes such matrices at design time by adding one state and one transition from the existing matrix. These matrices can be constructed as follows: 1)
Insert a new row and column in the rear of Q. Let the inserted row and column be the i-th row and the j-th column. All elements in the added row and column are 0. 2) 3) 4)
Choose a non-zero value from the elements in Q. Let the selected element be akl and its value be kl.
Introduce a new variable xnew and put this variable at ak j. Since the sum of transition probabilities in each row should be 1, we change the value kl at akl to kl xnew. We regard this matrix as a matrix similar to the existing matrix.
Repeat Steps 2 and 3 and generate matrices by changing a non-zero element in Q at Step 2 until all of the non-zero elements in Q are selected.
For example, our prediction strategy can make the matrix illustrated in Figure 8 from the matrix illustrated in Figure 3, that is, the model before adaptation.
Caching and prediction strategies are expected to require a large amount of memory space. To restrain the increase of memory usage, we try to reduce the candidate matrices on the basis of grouping. The reduction strategy defines sets of states in DTMC model as groups. This strategy removes the matrices that the prediction strategy generated by injecting transitions over different groups. This restriction saves certain degree of matrix generation.
Considering the cleaning robot example illustrated in Figure 2, we can define groups for sensing (the set of states s0 to s3 and the state s6) and migration (the set of states s4, s5, s7, and s8). When we prepare the similar matrix added a new state into the sensing group, we consider new transitions from the states within the sensing group, i.e., s0, s1, s2, s3, and s6, to the new state and transitions from the new state to these states. The reduction strategy prevents generating similar matrices that have less possibility of re-use.
IV.
In order to evaluate the effectiveness of our strategies, we conducted preliminary experiments on randomly generated DTMC models. We implemented three strategies in Java and compared the computational time and memory size of four methods of re-generation as follows:
Method 1: baseline (no caching), denoted as none in Figures 9 to 12; Method 2: caching, denoted as C in the figures; Method 3: caching and prediction, denoted as CP in the figures; Method 4: caching, prediction, and reduction, denoted as CPR in the figures.
As problem instances, we randomly generated DTMC models with the size ranging from 20 to 40 states increased by five, including two absorbing states. Some generated models contain loops. In these DTMC models, the number of outgoing transitions of each state follows a Gaussian distribution with mean 10 and standard deviation 2. Initial DTMC models, that is, the system models before adaptation, contain one or two variables as transition probabilities, and adaptation causes to introduce two variables into the models. We divided all states P = Added row into groups of size 10. We compared the averages of 10 runs for each configuration.
Figures 9 and 10 show the computational time to regenerate an expression. We can find that caching (Method 2) speeds up expression re-generation (faster than Method 1) but ĐĂĞŚ sometimes it does not affect computational time. Prediction (Method 3) and reduction (Method 4) further make the computation faster.
As for the cache size illustrated in Figures 11 and 12, on the other hand, prediction (Method 3) requires the largest memory size. Reduction (Method 4) partly reduces the memory size for caching.
The results of the experiments shows that the prediction strategy, on the basis of caching, is effective to reduce the computational time and the reduction strategy works to prevent the increase of memory size for caching. These strategies partially work; however, we also find that the effects of these strategies are still limited.
The current design of prediction with reduction prepares similar matrices for all elements in the same group in Q. We could make more precise prediction using the semantic of the system model. As for the memory size, our current reduction strategy is effective when behavioral changes are limited within the group. Since the effectiveness of reduction strategy is different between the cases illustrated in Figures 11 and 12, we should improve the applicability of reduction strategy. For further memory usage reduction, we could discard ϭ͘Ϭϳн small matrices that do not substantially affect computational time and redundant ones.
When using the proposed strategies, software developers should estimate the benefits of the strategies because they are still limited. The time required to generate expressions is reduced in the range of 10 to 30%. Also memory consumption should be taken into account. Even though prediction and reduction strategies are effective for reducing computational time, they consume a large amount of memory; this trade off should be carefully considered.
V.
Runtime verification, such as one in [
Kwiatkowska et al. [19] proposed an incremental quantitative verification of probabilistic models. This method uses the previous verification results that are acquired at runtime to speed up run-time verification. This approach can also deal with the structural changes of models. While this approach requires the analysis of change impact on the model before re-use of the previous verification results, our approach determines where the re-use can be applied by only checking cache hit, which can be implemented by a simpler mechanism.
VI.
We presented the current state of our approach that supports run-time verification when the structure of the system model is changed by adaptation. In order to reduce the computational time for re-generating expressions, we proposed three strategies, i.e., caching, prediction, and reduction. The preliminary evaluation demonstrated the possibilities of our strategies.
From the experimental results, we identified the directions for future work. First, we should address the reduction of cache size. Some Markov model simplification techniques, such as ones based on SCC (strongly connected components) reduction [20], partial order reduction [21], and bisimulation [22], can be beneficial to reduce cache size; however, excessive reduction could prevent our strategies from reusing stored matrices for regenerating expressions.
Second, we plan to improve the precision strategy of the prediction strategy. The improvement of prediction helps to keep the cache size from increasing. We also plan to improve the applicability of reduction strategy. One direction is discarding small size matrices and redundant ones. Third, after the sufficient improvement of our strategies, we will take into account different adaptation patterns, such as state removal or larger changes in the system model. In order to evaluate our approach on real world examples, we plan to embed the verification mechanism in our programming framework [23] for self-adaptive systems.
This work was supported by JSPS Grants-in-Aid for Scientific Research (No. 15K00097). The Telecommunications Advancement Foundation also supported this work.