The Theory of Reachability Analysis Method Using Abstraction and Refinement of Priced Probabilistic Timed Automaton, and Its Application to Design Verification of Wireless Sensor Networks

The design and reliability assurance of embedded systems is a complex issue, since they need to handle not only digital behavior but also physical quantities such as time, cost, and sometimes randomness. In addition, since many embedded systems, such as networks and automobiles, have systems in which errors can be fatal, design verification for reliability assurance is an important research topic. With the above background, we adopt the approach of specifying and verifying embedded systems by formal models. Specifically, we focus on a priced probabilistic timed automaton as a specification description language, and propose a reachability analysis method based on Counterexample-guided abstraction refinement (CEGAR) to reduce the state explosion. To demonstrate the effectiveness of the proposed method, we attempt to verify the design of important wireless sensor networks (WSNs). In this paper, we model WSNs by a priced probabilistic timed automaton that can express their power characteristics in terms of cost, uncertainty in terms of probability, real-time in terms of time, and attribute WSNs’ characteristics to the cost bound probabilistic reachability problem. To the best of our knowledge, this paper is the first CEGAR development and implementation of a priced probabilistic timed automaton. We have developed a prototype of the verifier and confirmed that it is verifiable.