Jinlin Yang
ABSTRACT
Model checking requires a specification of the target system's desirable properties, some of which are temporal. Formulating a temporal 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.
- G. Ammons, R. Bodik, and J. R. Larus. Mining specifications. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '02), January 2002. Google Scholar
Digital Library
- G. Ammons, D. Mandelin, R. Bodik, and J. R. Larus. Debugging temporal specifications with concept analysis. In SIGPLAN Conference on Programming Language Design and Implementation, June 2003. Google ScholarDigital Library
- T. Ball and S. K. Rajamani. Automatically validating temporal safety properties of interfaces. In 8th International SPIN Workshop on Model Checking of Software, May 2001. Google ScholarDigital Library
- G. Brat, K. Havelund, S. Park, and W. Visser. Model checking programs. In 15th IEEE International Conference on Automated Software Engineering, September 2000. Google ScholarDigital Library
- J. E. Cook, Z. Du, C. Liu, and A. L. Wolf. Discovering models of behavior for concurrent systems. New Mexico State University Technical Report, NMSU-CSTR-2002-010.Google Scholar
- J. Corbett, M. Dwyer, J. Hatcliff, S. Laubach, C. Pasareanu, Robby, H. Zheng. Bandera: extracting finite-state models from Java source code. In 22nd International Conference on Software Engineering, June 2000. Google ScholarDigital Library
- J. Corbett, M. Dwyer, and J. Hatcliff, and Robby. Expressing checkable properties of dynamic systems: the Bandera specification language. KSU CIS Technical Report 2001 -04, Kansas State University, 2001.Google Scholar
- M. Dwyer, G. Avrunin, and J. Corbett. Patterns in property specifications for finite-state verification. In 21 st International Conference on Software Engineering, May 1999. Google ScholarDigital Library
- M. D. Ernst, J. Cockrell, W. G. Griswold, and D. Notkin. Dynamically discovering likely program invariants to support program evolution. In IEEE Transactions on Software Engineering, February 2001. Google ScholarDigital Library
- G. J. Holzmann. The model checker Spin. In IEEE Transactions on Software Engineering, May 1997. Google ScholarDigital Library
- G. J. Holzmann. The logic of bugs. In 10th ACM SIGSOFT International Symposium on Foundations of Software Engineering, November 2002. Google ScholarDigital Library
- K. Havelund and T. Pressburger. Model checking Java programs using Java PathFinder. In International Journal on Software Tools for Technology Transfer, September 1999.Google Scholar
- K. Havelund. Using runtime analysis to guide model checking of Java programs. In 7th International SPIN Workshop on Model Checking of Software, August/September 2000. Google ScholarDigital Library
- J. W. Nimmer and M. D. Ernst. Invariant inference for static checking: an empirical evaluation. In ACM SIGSOFT 10th International Symposium on the Foundations of Software Engineering, November 2002. Google ScholarDigital Library
- K. M. Olender and L. J. Osterweil. Cecil: a sequencing constraint language for automatic static analysis generation. In IEEE Transactions on Software Engineering, March 1990. Google ScholarDigital Library
- A. Pnueli. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science, October/November 1977.Google ScholarDigital Library
- J. Whaley, M. C. Martin, and M. S. Lam. Automatic extraction of object-oriented component interfaces. In International Symposium on Software Testing and Analysis, July 2002. Google ScholarDigital Library
Index Terms
- Dynamically inferring temporal properties
Recommendations
A compositional automata-based semantics and preserving transformation rules for testing property patterns
AbstractDwyer et al. provide a language to specify dynamic properties based on a limited number of predefined patterns and scopes. The semantics of these properties is defined by translating each combination of a pattern and a scope into usual temporal ...
Specifying and Monitoring Temporal Properties in Web Services Compositions
ECOWS '09: Proceedings of the 2009 Seventh IEEE European Conference on Web ServicesCurrent Web service composition approaches and languages such as WS-BPEL do not allow to define temporal constraints in a declarative and separate way. Also it is not possible to verify if there are contradictions between the temporal constraints ...
Checking temporal properties under simulation of executable system descriptions
HLDVT '00: Proceedings of the IEEE International High-Level Validation and Test Workshop (HLDVT'00)The verification of systems, i.e., hardware or hardware/software systems, is an important task in the design process. More than 70% of the development time is spend for locating and correcting error in the design. Therefore, many techniques have been ...
Comments