Non-Deterministic Behavior Analysis for Embedded Software Based on Probabilistic Model Checking

The real-time interaction between embedded software and its external environment is conducted through the interrupt mechanism. Since the interrupt request is random and responds according to priority, the execution of embedded software is non-sequential, which leads to the non-deterministic software behaviors. If these non-deterministic behaviors can be quantitatively pre-analyzed during the software design phase, the reliability of embedded software can be improved effectively. In this paper, we first provide an embedded software behavior model based on extended deterministic and stochastic Petri nets (EDSPN). Through EDSPN, the interrupt behavior of embedded software can be effectively modeled. Then we put forward a probabilistic model checking method of Continuous Stochastic Logic (CSL) for EDSPN to analyze embedded software behavior. For alleviating the state explosion problem, the above method uses the bounded model checking (BMC) technique. We present the model checking methods and the probability metric calculation methods for CSL operators under bounded semantics. Finally, by analyzing the EDSPN model of embedded software with multiple interrupts, we compare the analytical capabilities of BMC method and non-BMC method. The experiment shows that when the state space of EDSPN is large and is hard to calculate, the bounded checking algorithm can be used to approximate the software behavior. The conclusions obtained are helpful to understand the properties to be verified.