Cyber-physical systems (CPS) are expected to continuously monitor the physical components to autonomously calculate appropriate runtime reactions to deal with the uncertain environmental conditions. Self-adaptation, as a promising concept to fulfill a set of provable rules, majorly needs runtime quantitative verification (RQV). Taking a few probabilistic variables into account to represent the uncertainties, the system configuration will be extremely large. Thus, efficient approaches are needed to reduce the model state-space, preferably with certain bounds on the approximation error. In this paper, we propose an approximation framework to efficiently approximate the entire model of a self-adaptive system. We split up the large model into strongly-connected components (SCCs), apply the approximation algorithm separately on each SCC, and integrate the result of each part using a centralized algorithm.
کلید واژگان :Self-adaptive systems, Probabilistic model checking, Runtime verification, Markov decision process, Approximation techniques, Cyber-physical system
ارزش ریالی : 600000 ریال
با پرداخت الکترونیک