Constructing Property-Oriented Models for Verification

Jifeng He, Shengchao Qin, Adnan Sherif

Research output: Chapter in Book/Report/Conference proceedingConference contribution

80 Downloads (Pure)

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.
Original languageEnglish
Title of host publicationUnifying theories of programming
Pages85-100
DOIs
Publication statusPublished - 2006
Event1st International Symposium on Unifying Theories of Programming - Walworth Castle, United Kingdom
Duration: 5 Feb 20067 Feb 2006
Conference number: 1

Publication series

NameUnifying Theories of Programming
Volume4010
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference1st International Symposium on Unifying Theories of Programming
CountryUnited Kingdom
Period5/02/067/02/06

Bibliographical note

Author can archive post-print (ie final draft post-refereeing).

Cite this