Chunhui Guo

Chunhui Guo, Zhicheng Fu, Zhenyu Zhang et al.

Improving the effectiveness and safety of patient care is the ultimate objective for medical cyber-physical systems. Many medical best practice guidelines exist, but most of the existing guidelines in handbooks are difficult for medical staff to remember and apply clinically. Furthermore, although the guidelines have gone through clinical validations, validations by medical professionals alone do not provide guarantees for the safety of medical cyber-physical systems. Hence, formal verification is also needed. The paper presents the formal semantics for a framework that we developed to support the development of verifiably safe medical guidelines. The framework allows computer scientists to work together with medical professionals to transform medical best practice guidelines into executable statechart models, Yakindu in particular, so that medical functionalities and properties can be quickly prototyped and validated. Existing formal verification technologies, UPPAAL timed automata in particular, is integrated into the framework to provide formal verification capabilities to verify safety properties. However, some components used/built into the framework, such as the open-source Yakindu statecharts as well as the transformation rules from statecharts to timed automata, do not have built-in semantics. The ambiguity becomes unavoidable unless formal semantics is defined for the framework, which is what the paper is to present.

Chunhui Guo, Hao Wu, Xiayu Hua et al.

Reliability, longevity, availability, and deadline guarantees are the four most important metrics to measure the QoS of long-running safety-critical real-time applications. Software aging is one of the major factors that impact the safety of long-running real-time applications as the degraded performance and increased failure rate caused by software aging can lead to deadline missing and catastrophic consequences. Software rejuvenation is one of the most commonly used approaches to handle issues caused by software aging. In this paper, we study the optimal time when software rejuvenation shall take place so that the system's reliability, longevity, and availability are maximized, and application delays caused by software rejuvenation is minimized. In particular, we formally analyze the relationships between software rejuvenation frequency and system reliability, longevity, and availability. Based on the theoretic analysis, we develop approaches to maximizing system reliability, longevity, and availability, and use simulation to evaluate the developed approaches. In addition, we design the MIN-DELAY semi-priority-driven scheduling algorithm to minimize application delays caused by rejuvenation processes. The simulation experiments show that the developed semi-priority-driven scheduling algorithm reduces application delays by 9.01% and 14.24% over the earliest deadline first (EDF) and least release time (LRT) scheduling algorithms, respectively.