Reachability Analysis Method Using Abstraction and Refinement of Priced Probabilistic Timed Automaton and Its Application for 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. Considering the above background, we adopt the approach of specifying and verifying embedded systems using 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 via 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. The model of verification is a WSN with four sensor nodes and three point hops and the verification problem is (lerror,λ=0.3,κ=32). The experimental result shows that the verification was completed with 22 CEGAR loops and 66 states. This paper is innovative and significant as a milestone in the development of an extension of CEGAR to priced probabilistic timed automata.