Dynamically inferring temporal properties

Model checking requires a specification of the target system’s desirable properties, some of which are temporal. Formulating a property of the system based on either its abstract model or implementation requires a deep understanding of its behavior and sophisticated knowledge of the chosen formalism. This has been a major impediment to documenting and verifying temporal properties. We propose a dynamic approach to automatically infer a program’s temporal properties based on a set of property pattern templates. We describe a preliminary implementation of this approach, and report on our experience using it to discover interesting temporal properties of a small program. Categories and Subject Descriptors D.2.4 [Software/Program Verification] General Terms Experimentation, Verification. Keywords Invariants, temporal properties, concurrent programming, dynamic analysis, property patterns.

• Type: Conference
• Year: 2004
• Where: PASTE
• Authors: Jinlin Yang, David Evans
• Keywords: PASTE 2004, Program’s Temporal Properties, System’s Desirable Properties, Temporal Properties