Constructing Property-Oriented Models for Verification

He, J.; Qin, S.; Sherif, A.

Abstract

This paper advocates a general approach to formal verification by constructing property-oriented models. We instantiate the approach using timing properties, and construct a heterogeneous untimed model in which time is abstracted away, so that we can verify timing properties in an untimed framework. The correctness of property-oriented model construction is ensured by the conformance of semantic and syntactic mappings.

Citation

He, J., Qin, S., & Sherif, A. (2006, February). Constructing Property-Oriented Models for Verification. Presented at First International Symposium on Unifying Theories of Programming (UTP 2006), County Durham, UK

• Presentation Conference Type: Conference Paper (published)
• Conference Name: First International Symposium on Unifying Theories of Programming (UTP 2006)
• Start Date: Feb 5, 2006
• End Date: Feb 7, 2006
• Publication Date: Feb 1, 2006
• Deposit Date: Nov 16, 2009
• Publicly Available Date: Dec 10, 2009
• Print ISSN: 0302-9743
• Publisher: Springer Verlag
• Pages: 85-100
• Series Title: Lecture notes in computer science
• Series Number: 4010
• Book Title: Unifying theories of programming : first international symposium, UTP 2006, Walworth Castle, County Durham, UK, February 5-7, 2006 : revised selected papers.
• ISBN: 9783540347507
• DOI: https://doi.org/10.1007/11768173_6
• Public URL: https://durham-repository.worktribe.com/output/1163287