RECENTLY COMPLETED EPP DOCTORAL THESIS...(CONTINUED)

Vasiliki Hartonas-Garmhausen, Probabilistic Symbolic Model Checking with Engineering Models and Applications.
Committee:  Ed Clarke - chair (CS), Granger Morgan (EPP/ECE/Heinz), Gary Powers (ChemE), and Mitchell Small (CEE/EPP)

     Verifying the safety of computer systems is important, especially when they control and monitor life-critical operations.  Industries such as transportation, pharmaceutical, chemical, and nuclear power need "industrial-strength" formal methods and real-world case studies that demonstrate the feasibility of these methods.  This thesis presents a new tool for the formal verification of stochastic systems and provides case studies of railway signaling control systems, flexible manufacturing systems, reliable systems, and networks that illustrate the verification methodology.
     Model checking is a formal method for the specification and verification of concurrent reactive systems.  A system is modeled by a state transition graph represented by binary decision diagrams.  Specifications are written using a propositional branching-time temporal logic called Computation Tree 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.  Our approach models stochastic systems as finite state Markov processes.  We convert a state transition graph to a finite-state Markov chain by assigning probabilities on the transitions.  We use multi-terminal binary decision diagrams for the representation of the transition probability matrices.
     While model checking can tell whether a system is correct, probabilistic model checking can also tell whether a system is timely and reliable.  It 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." 
     The thesis includes case studies in railway signaling, manufacturing, networks, and safety analysis of reliable systems, which 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.
     The work was supported by SRC contract 97-DJ-294, NSF grant CCR-9505472, and DARPA contract DABT63-96-C-0071.

Columbia and Georgia Tech Announce Washington Effort

     Columbia University and Georgia Institute of Technology have announced that they will create a center of science and technology policy studies in Washington, DC.  The idea for the Center grew out of a series of three conferences held at Columbia in the mid-1990s which were designed to take a fresh look at the post-war model of R&D as articulated in the landmark report by Vannevar Bush, "Science the Endless Frontier."  Support for the new effort is being sought from a variety of sources.