Using Parallelism and Randomness in the Analysis of Large- Scale Real-Time Systems

点击翻译按钮获取中文摘要

9311622 Lee The goal of this project is to develop efficient algorithms for the automated analysis of communicating systems and distributed real-time systems. We base this research on a general framework, called a Communicating Timed State Machine with Probability (CTSMP). CTSMPs are state machines that communicate messages synchronously over one-to-many channels. In addition, CTSMPs support several features that are useful in describing real-time computer systems. Examples of such features include local variables, timed state transmissions, and probabilistic state transitions. The compositional semantics of CTSMPs allows a complex system to be specified as a collection of simple machines that communicate and synchronize with one another. The inclusion of both timed state transitions and probabilistic state transitions allows the modeling of faults and timing properties in the same framework. The fundamental issue in the automated analysis of communicating systems is the efficient generation of the reachable state space. For finite state systems, the problem is state explosion. For infinite state systems, it is not possible to generate all the states; instead, we need to find a way of combining sets of states. There are two approaches to address the state explosion and exploration problem: 1) reduce the state space either through efficient encoding or by clustering sets of equivalent states; and 2) generate or explore less space using probability. This research employs both of these approaches and consists of several related parts: 1) design of CTSMP state minimization algorithms; 2) discovery of probabilistic state generation and exploration algorithms; 3) design of efficient model checking algorithms using CTSMP and comparison with binary decision diagram based algorithms; and 4) improving the efficiency of the above algorithms using parallelism and randomization. This project will implement these algorithms and evaluate their effectiveness exper imentally. ***