William Chan's Research Page

I am a PhD candidate in the Department of Computer Science and Engineering at the University of Washington. Please see my home page for more personal information.

In January 2000, I will be joining the Department of Computer Science at Brown University as an assistant professor.

Research Interests

I am interested in formal methods and verification for software systems. In particular, I am working on verifying the specifications of large software systems using symbolic model checking, under the guidance of Professors Richard Anderson, Paul Beame, and David Notkin.

Temporal-Logic Queries

I have a new idea of using "temporal-logic queries" for model understanding. Stay tuned for more details.

Symbolic Model Checking for Statecharts-like Specifications

Software errors cost money, and can threaten lives as more and more safety-critical systems rely on computers (e.g., computing systems used in airplanes, automobiles, and nuclear plants). The most dangerous and expensive software flaws often occur not in the implementation, but rather in the specification from which the code is derived. Many researchers and practitioners therefore recognize the needs for specifying software systems in formal languages that allow mechanical analysis. But even so, the analysis performed is usually limited to simulation and syntactic checks, which are simple but provide little correctness guarantee, and theorem proving, which requires extensive human efforts.

Symbolic model checking is a practical formal-verification technique that is automatic and is capable of analyzing a wide range of semantic properties (e.g., safety and liveness). Although the technique is mostly used for hardware verification, we use it to analyze the finite-state models of the state-machine specifications of two non-trivial airborne software systems. Applying the technique to a new domain allowed us to discover new research problems and devise some innovative solutions.

More specifically, we used and modified SMV, a model checker based on binary decision diagrams (BDDs), to analyze an early version of the TCAS II (Traffic Alert and Collision Avoidance System II) System Requirements Specification. TCAS II is a complex airborne collision avoidance system used on most commercial aircraft in the United States, and its requirements specification is written in RSML, a hierarchical state-machine language based on Harel's statecharts. After overcoming a number of obstacles, we were able to analyze part of the requirements, verifying as well as falsifying a number of interesting properties [TSE98]. The performance of the analysis can be improved by orders of magnitude using various optimizations [ISSTA98].

Despite the promising results, a large part of the requirements remains beyond reach because of the numerous complicated nonlinear arithmetic predicates. One approach we have considered to attack the problem is to couple the BDD-based model checker with a decision procedure for nonlinear arithmetic [CAV97].

For more information on TCAS II, see

Rannoch's description of TCAS: http://www.rannoch.com/tcasf.html They have examples on TCAS's statechart diagrams and AND/OR tables, as well as an article in Inside FAA, and an article in Federal Computer Week on TCAS.

AlliedSignal's explanation of TCAS: http://aerospace.alliedsignal.com:80/aerospace/products/aircraft_products/products/traffic_alert_collision_avoidance.html

RTCA's home page which contains information on obtaining TCAS documents: http://www.rtca.org

William J. Hughes Technical Center's TCAS group home page: http://tcas.tc.faa.gov/

CAASD's TCAS page: http://info.caasd.org/Research/TCAS/

TCAS home page at FAA: http://www.faa.gov/and/and600/and620/newtcas.htm

With David Jones and William Warner from Boeing, we have recently looked at another statecharts specification that models an airborne fault-tolerant electrical power distribution system. Combining the experience of the two case studies, we found out how the styles of synchronization among the state machines can affect the efficiency of the analysis. New optimization techniques allowed us to discover a number of design flaws not found by simulation [ICSE99].

Selected Publications

William Chan, Richard J. Anderson, Paul Beame, David H. Jones, David Notkin, and William E. Warner. Decoupling synchronization from local control for efficient symbolic model checking of statecharts. In Proceedings of the 1999 International Conference on Software Engineering (ICSE'99), pages 142-151, May 1999, Los Angeles, USA. [Abstract | Postscript | PDF]

William Chan, Richard J. Anderson, Paul Beame, and David Notkin. Improving efficiency of symbolic model checking for state-based system requirements. In ISSTA 98: Proceedings of the ACM SIGSOFT International Symposium on Software Testing and Analysis, pages 102-112, March 1998, Clearwater Beach, Florida, USA. [Abstract | Postscript | PDF]

William Chan, Richard Anderson, Paul Beame, and David Notkin. Combining constraint solving and symbolic model checking for a class of systems with non-linear constraints. In Computer Aided Verification, 9th International Conference, CAV'97 Proceedings, LNCS 1254, pages 316-327. Springer-Verlag, June 1997, Haifa, Israel. [Abstract | Postscript | PDF]

William Chan, Richard J. Anderson, Paul Beame, Steve Burns, Francesmary Modugno, David Notkin, and Jon D. Reese. Model checking large software specifications. In IEEE Transactions on Software Engineering 24(7), pages 498-520, July 1998. Preliminary version appeared in SIGSOFT'96: Proceedings of the Fourth ACM SIGSOFT Symposium on the Foundation of Software Engineering, pages 156-166, October 1996, San Francisco, USA. [Abstract | Postscript | PDF]

William Chan (wchan@cs.washington.edu) http://www.cs.washington.edu/homes/wchan/work/