Probabilistic symbolic model checking with engineering models and applications

Verifying the safety of computer systems is of paramount importance, especially when such systems control and monitor life-critical operations. However, this problem is very difficult due to the size and complexity of the analyzed systems, and the stochastic nature of the physical world with which they interface. The transportation, pharmaceutical, chemical, and nuclear industries need robust tools and real-world case studies that demonstrate the feasibility of applying formal methods. This thesis presents a new tool for the formal verification of stochastic systems and provides case studies of railway signalling control systems, flexible manufacturing systems, reliable systems, and networks that illustrate the verification methodology.; Symbolic model checking is a formal method for the verification of finite-state systems. Systems are modeled by state transition graphs represented using binary decision diagrams, and specifications are written in temporal logic. Efficient symbolic algorithms perform an exhaustive search of the state space to determine if the specification is true or not. Symbolic model checking has proved to be very successful in finding design errors in several industrial systems and protocols. This extends symbolic model checking to the analysis and verification of stochastic systems. Our approach models stochastic systems as finite state Markov processes, which are obtained from state transition graphs by assigning probabilities to the transitions. The novelty of this thesis is the use of multi-terminal binary decision diagrams in representing the transition probability matrix and performing the probability calculations.; Probabilistic model checking makes it possible to check specifications such as “there is at least a 0.001% probability that the system will fail during the first 4 hours of operation” or “once a request occurs, there is a 98% probability that the request will be acknowledged within 5 seconds.” While model checking can tell us whether a system is correct, probabilistic model checking can also tell us whether a system is timely and reliable.; The case studies demonstrate that the methods we have proposed are efficient enough to use in the formal verification of real-world systems and can ultimately lead to the design of safer and better products.