{"id":358,"date":"2018-11-06T00:57:02","date_gmt":"2018-11-06T00:57:02","guid":{"rendered":"http:\/\/se.kaist.ac.kr\/starlab\/?page_id=358"},"modified":"2018-12-10T03:17:37","modified_gmt":"2018-12-10T03:17:37","slug":"statistical-model-checking","status":"publish","type":"page","link":"https:\/\/se.kaist.ac.kr\/starlab\/studies\/study-2-statistical-verification-of-sos\/statistical-model-checking\/","title":{"rendered":"Statistical Model Checking"},"content":{"rendered":"

Background<\/strong><\/h4>\n

Since an SoS is composed of many autonomous and independent CSs, SoS behavior is uncertain and unpredictable. Modeling an SoS with a probabilistic model is considered the proper way to deal with this issue. Probabilistic models express various behaviors using probability. When a probabilistic model comes to the verification stage, Statistical Model Checking (SMC) is a promising method of verification, especially when the model is large and\/or complex. SMC is based on hypothesis testing. It checks the verification property of a sample set of simulations to decide whether the model satisfies the property within a certain probability, which is based on the number of executions for which the property holds compared to the total number of executions in the sample set. Such sampling-based methods are far less memory and time intensive than traditional model checking methods. In this paper, we use an SMC tool called PRISM to model and verify an SoS that exhibit probabilistic behavior.<\/p>\n

 <\/p>\n

Overall Approach\/Method<\/strong><\/h4>\n

We verify the SoS-level goal achievement by claiming it as the verification property. We perform SMC using PRISM models. We first explain the verification property (i.e., the SoS-level goal) for the MCI example. We provide the verification results.<\/p>\n

Figure: SMC verification property for the MCI example<\/em><\/p>\n

\"\"<\/a><\/p>\n

In the MCI example, the SoS-level goal is saving as many patients as possible. We formalize this in Figure 6. In Figure 6, line 1 represents the goal of the number of patients to be saved. Since there are 250 patients in our example (200 patients in the MCI area and 50 patients in the non-MCI area), we set the goal at 90% (i.e., 225) of the patients. Line 2 represents the formal verification property for SMC. It verifies the probability of saving at least 90% of patients within 10,000 steps of each sample simulation. [Note: we set 10,000 steps to limit the number of steps in each simulation.] The SMC considers 10,000 samples with a confidence level 0.01. In other words, the verification property is verified using 10,000 samples with 99% accuracy. To execute the PTS and ENV models, we set the environmental parameters. We assume that the patients in the MCI area appear five times more than the patients in nonMCI area. This is modeled via MCI_OCCUR_RATE = 5 and NON_OCCUR_RATE = 1. We also assign the probabilities of death in the MCI and non-MCI areas by PR_MCI_DEAD = 0.1 and PR_NON_DEAD = 0.02, since the patients in the MCI area are more critical than the patients in the non-MCI area.<\/p>\n

 <\/p>\n

Results<\/strong><\/h4>\n

\"\"<\/a><\/p>\n

In order to verify the probability of saving more than or equal to 90% of total patients, we conducted SMC on the DIR-SoS, ACK-SoS, and COL-SoS for the MCI example using PRISM.<\/p>\n

First, we observed the minimum probability of SoS-level goal achievement according to the SoS types. Figure 7 shows the results. The graph shows that the types of SoS\u2014the degree of authority\u2014significantly affect the probability of goal achievement as well as behaviors of PTSs. In every case of different rate_SoS, a directed type of MCI-SoS (DIR-SoS) succeeded in achieving the SoS-level goal, while curves are plotted by other types of SoSs. This is because the DIR-SoS is not affected by rate_SoS. In case of ACK-SoS, the probability of achieving the SoS-level goal increases with an increase in rate_SoS. This is because the SoS-level manager can effectively manage PTSs with an increasing degree of authority (i.e., increasing rate_SoS). Similarly, in COL-SoS, the probability of achieving the SoS-level goal increases when rate_SoS increases and rate_info is fixed as 0.8.<\/p>\n

We conducted statistical verification again to identify the effect of both rate SoS and rate info on the probability of achieving the SoS-level goal of a collaborative SoS (COL-SoS). Figure 8 shows six graphs of goal achievement possibilities. Each graph shows a tendency to increase as rate_SoS increases, except in two cases where it resulted in zero probability (rate_info=0 and rate_info=0.2). Judging by the result, a greater affinity to the SoS-level goal leads to a higher possibility of achieving the goal in COL-SoSs. Furthermore, the increased possibility of acquiring MCI-related information (rate_info) brought an improvement in the probability of achieving the SoS-level goal at the same level of rate_SoS. For example, a graph that has 0.4 rate info has a probability less than half of the graph with 0.6 rate_info at rate_SoS 0.8. Therefore, it can be inferred that collaborative MCI-SoSs are significantly affected by the degree (or capability) of acquisition of MCI-related information.<\/p>\n

From the experiments that observed the differentiated behaviors and possibilities of achieving the SoS-level goal, we observed different behaviors and possibilities to achieve the SoS-level goal according to the three types of SoS using an MCI example. By analyzing the results, we identified the need to analyze SoS types and their behaviors, and we also found that the degree of authority of an SoS could have a great influence on emergent behaviors and CS behaviors. In summary, SoSs that differ from each other based on degree of authority; types of SoS can be modeled through probabilistic modeling, and their behaviors can be verified via statistical verification technique, such as PRISM.<\/p>\n

 <\/p>\n

Related Publications<\/strong><\/h4>\n