Speaker: Gianfranco Ciardo , Department of Computer Science, College of William and Mary
The Importance of Being Structural
(better symbolic model-checking for asynchronous systems)
Abstract: Symbolic algorithms based on binary-decision diagrams (BDDs) have enabled the exhaustive logic verification of enormous discrete-state systems. For example, in state-space generation, the currently-known set of reachable states and the next-state function are compactly encoded using BDDs. Then, a fixed-point iteration explores the entire state space in as many steps as the maximum distance of any state from the initial state. However, the time and memory requirements can still be excessive for large models.
We present a new approach to target globally-asynchronous locally-synchronous systems, such as protocols, Petri nets, or, especially, concurrent software. We employ a boolean Kronecker encoding of the next-state function (an idea originally developed for the exact solution of large Markov chains) paired with multi-way decision diagrams (MDDs) to store the state space. We introduce several improvements made possible by the use of structural information automatically extracted from the model, such as taking into account the locality of effect for an event, the symmetry and monotonicity properties inherent in our MDD manipulations, and, above all, the use of "saturation", a completely different style of fixed-point iteration. Since these ideas complement each others, the overall effect is cumulative, resulting in huge improvements in both memory and time with respect to state-of-the-art symbolic tools. We also briefly illustrate how this "structural approach" can be applied to shortest counter-example generation and symbolic model checking, with excellent results.
We conclude by describing an application of our techniques, implemented in the tool SMART, to an embedded software system being developed at NASA for use in civil aviation.
Short Bio: Gianfranco Ciardo is currently a Professor of Computer Science at the College of William and Mary, Williamsburg, Virginia, but he will join the University of California at Riverside in 2004. He has been a Visiting Professor at the University of Torino, Italy, and the Technical University of Berlin, Germany, and held research positions at HP Labs (Palo Alto, California), Software Productivity Consortium (Herndon, Virginia), and CSELT (Torino, Italy). He received a PhD degree in Computer Science from Duke University, Durham, North Carolina and a Laurea in Scienze dell' Informazione from the University of Torino, Italy.
He is interested in theoretical research and practical tool building for logic and stochastic analysis of discrete-state models, symbolic model checking, performance and reliability evaluation of complex hardware/software systems, Petri nets, and Markov models.
He is on the editorial board of IEEE Transactions on Software Engineering, was the keynote speaker at PNPM'01, and will be a keynote speaker at ICATPN'04.
Host: Billy Stewart, Computer Science, NCSU