A Scalable, Reconfigurable, and Dependable Time-Triggered Architecture
John Rushby · 2003
The research performed in this project began with a study and comparison of time-triggered bus architectures for critical systems and with development of flexible methods for scheduling time-triggered systems. Later work focused on automated synthesis and refutation (debugging) and developed a new method for bounded model checking over infinite domains based on integration of efficient decision procedures with SAT solving. The method was then extended to automated verification. Implementations of the method are available from SRI in our tools ICS and SAL. The approach pioneered in this project for combining decision procedures with a SAT solver has now become the dominant one for bounded model checking and automated verification.