I briefly introduce our approach and how we evaluated it. First, you'll see why PASTA was proposed. This paper is about proactive adaptation of a self-adaptive system. Proactive adaptation, sometimes called predictive adaptation, is a relative

concept to reactive adaptation. A self-adaptive system somehow decides its operation, changing its behavior or its architecture, responding to its current runtime environment. If the system makes its decision reactively based on the current situation, we call it reactive adaptation. But if the decision is made based on the prediction,

we call it a predictive or proactive adaptation. For example, of an error condition controller that automatically controls its operation to achieve users' desired target condition. If the adaptation is reactive, it will decide

its control vector only based on the current condition. However, if the indoor condition keeps changing, the reactive adaptation control can cause unexpected result. In that case, if the environment change can be predicted, an adaptation based on the prediction could be more effective.

Recent years, in self-adaptive system research community, proactive adaptation research were emerging and they showed the proactive adaptation is more effective than reactive adaptation if acceptable prediction can be made. However, the prediction of future

environment change brings uncertainty because the prediction is usually non-deterministic. Therefore, an adaptation decision based on the uncertain prediction can also bring uncertain or unexpected results. In this context, proactive adaptation approaches have tried to find ways to guarantee or verify the expected adaptation results.

The major and effective approach until now is using probabilistic verification to evaluate an adaptation tactic. The probabilistic model checker such as PRISM returns a probabilistic expectation of an adaptation result, and among the numerous tactics, the best one is chosen and executed.

However, probabilistic model checking so-called PMC has typical known problems. One is its state explosion problem. PMC requires two inputs. One is verification target model, and the other is verification property specification. Because PMC returns

theoretically correct verification results, exhaustively examining the given models, the verification space becomes exponentially larger depending on the input model's complexity. So, if the input model of the target adaptive system is complex,

it becomes hard to apply PMC within a short verification time and small memory. Another limitation is that the language that PMC checkers support are very limited to some formal modeling languages such as some types of Markov chains. Therefore, engineers should represent

system and environment in the given languages. In this context, if a system is too complex, or if the system is blackbox or graybox system, fully specifying the system in those languages could be impossible. Within the limitations of using PMC,

the alternatives to PMC-based proactive adaptation were not actively considered because the field itself is quite new yet. So, we propose on a proactive adaptation approach based on statistical model checking, which is known as an efficient alternative to PMC.

The statistical model checking so-called SMC is known to verify probabilistic models much faster than PMC. In addition, it can be applied to any simulation executable models or system itself, so it has high freedom to the system specification language.

So, I'll introduce our proactive adaptation based on statistical model checking so-called PASTA comparing to the PMC-based approach. First, this is typical PMC-based proactive adaptation process. When system monitors its environment at runtime, it forecasts the future

environmental change with the historical data. The prediction is probabilistic, and the prediction is modeled as an environmental change model, and here the model template or skeleton should be given by engineers in a specific formal language. In addition, the system should

also have its own system model that includes the specification of its possible adaptation tactics written in the formal language. The system and environment models are coupled and verified to find an optimal adaptation path that is expected to bring best reward.

When all adaptation tactics have been evaluated, the best one is chosen and executed. In PASTA process, the previous process is modified to use SMC instead of PMC. PASTA

also forecasts probabilistic future environment based on the environment data. Unlike to that PMC models, the environment change SMC just simply generates a future environment value sample. The system specification language is not limited only if it is executable by a simulator. Therefore, a black box system is also acceptable if it is executable by a

simulator, or any simulation model of a specific domain's simulator is also acceptable. In addition to the simulation model, a set of tactic specifications that is interpretable by the system is given. A set of values of configurable variables can be one example

of the tactic specification. A combination of the system model and a tactic is iteratively simulated with numerous samples. Then, the accumulated simulation results are used to

evaluate a specific tactic's score by user-defined evaluation method. When all tactics have been evaluated, the best one is selected and executed. Let me explain the steps with more concrete examples of error condition controller. The error conditioner monitors current temperature. Based on the historical temperature change data

and current data, it predicts the future temperature. But the prediction is not a concrete value but a probabilistic expectation. Based on the prediction, a temperature sample with a concrete value is randomly selected. Here, an error conditioner simulation model is given.

The simulation calculates future goal achievement based on the sample temperature and the system's operation. The system's possible actuating operations, I mean the adaptation tactics, are also specified based on the error conditioner's capability. A sample, the system

model, and an adaptation tactic is combined and simulated. The simulation calculates the expected results of a specific tactic. And the tactic is repeatedly simulated with samples. The sufficient number of samples can be decided by the existing SMC algorithms,

and the well-known algorithms are explained in our paper. Based on the simulation result, expected indoor temperature manipulated by the error conditioners is evaluated by the difference of the goal and current temperature.

These iterative simulations and evaluations are repeated for all adaptation tactics. When the evaluations for all adaptation tactics are done, the best one is selected and executed in the real system. This whole process is an adaptation loop,

and it goes back to the monitoring step. With the general process of PASTA, we also provide a reference architecture and code skeleton of PASTA for easier implementation of our approach. Because the proposed PASTA process is general and abstract, engineers can also extend our

skeleton to their specific domains. Then we evaluated the PASTA. To evaluate PASTA as an efficient alternative to PMC-based approach, we compared PASTA and PMC-based approach with the three questions. First, we show how much time is required

for an adaptation loop by each approach. Second, we can theoretically believe PMC will return a correct verification result, but SMC doesn't. Because SMC's verification result relies on the numerous randomly selected samples, the adaptation planning result made by SMC was

compared to PMC. Third, domain-specific adaptation goals of two case systems achieved by PASTA were also evaluated. For the experiment, PASTA was implemented, as we described before, in Java. A well-known SMC algorithm, Simple Monte Carlo Simulation,

was implemented. For PMC-based approach, we reproduced a pioneering paper of PMC-based model checker. We simulated the two approaches in two case systems. One is air-conditioned

controller, and another is traffic signal controller of an intersection. In this presentation, I'll keep explaining only the air conditioner's evaluation result. In RQ1, we could see that PASTA is much faster to verify all adaptation tactics than

PMC-based approach. Although PASTA execution time is linearly dependent on the number of samples used in verification, PMC-based approach consumes much more larger costs for verification. In RQ2, we evaluated how similar adaptation decisions are made by PASTA

and PMC-based approach. We could see PASTA's adaptation decision was almost similar or identical to the PMC-based approach. In RQ1 and 2, we could see PASTA plans a suboptimal adaptation tactic faster than PMC-based approach. In this case system, the user's

desired temperature was 25°C. In the perspective of its goal, PMC-based productive adaptation and our PASTA approach shows almost similar performance. In addition, both of them outperforms

reactive adaptation. So, we could see both PMC and SMC-based approach achieved the adaptation goal similarly in this RQ3. In conclusion, we proposed PASTA as a cost-efficient alternative to PMC-based proactive adaptation approach. PASTA can make statistically verified

proactive adaptation decision with more shorter time compared to PMC-based approach. Because our SMC-based approach, PASTA, is cost-efficient, it might be more appropriate for real-time system than PMC-based approach. We provided this comparative analysis in our paper,

so if you are interested in our work, please check it in our paper. Thank you for listening today's talk.