EECS 298-11: CAD Seminar Wednesday, April 3, 1996, 5pm 531 Cory Hall, Hogan Room Temporal Verification by Diagram Transformations Luca de Alfaro Stanford University This talk presents a methodology for the verification of temporal properties of systems based on the gradual construction and algorithmical checking of {\em fairness diagrams}. Fairness diagrams correspond to abstractions of the system and of its progress properties, and have a simple graphical representation. In the proposed methodology, a proof of a temporal property consists in a chain of fairness diagram transformations, starting from a diagram representing the original system and ending with a diagram that is either obtained from the specification, or that can be shown to satisfy it by purely algorithmical methods. Each diagram transformation is simple, and is meant to capture a natural step of the gradual process of system analysis and proof discovery. We discuss two types of transformations: the first type relies on the construction of simulation relation between diagrams; the second type analyzes the progress properties of a diagram. The structure of fairness diagrams simplifies reasoning about progress properties, and the graphical representation provided by the diagrams enables the user to direct the construction of the proof in an effective way. The resulting methodology is complete for proving specifications written in first-order linear-time temporal logic, provided no temporal operator appears in the scope of a quantifier. Upcoming seminars: April 8: Henry Verheyen, Aptix Corp. April 10: N. Shankar and M. Srivas, SRI April 15: Peter Kopke, Cornell