Constructing Property-Oriented Models for Verification

Jifeng He; Shengchao Qin; Adnan Sherif

doi:10.1007/11768173_6

Constructing Property-Oriented Models for Verification

Jifeng He, Shengchao Qin, Adnan Sherif

SCEDT School Executive Team

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

117 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 language	English
Title of host publication	Unifying theories of programming
Pages	85-100
DOIs	https://doi.org/10.1007/11768173_6
Publication status	Published - 2006
Event	1st International Symposium on Unifying Theories of Programming - Walworth Castle, United Kingdom Duration: 5 Feb 2006 → 7 Feb 2006 Conference number: 1

Publication series

Name	Unifying Theories of Programming
Volume	4010
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	1st International Symposium on Unifying Theories of Programming
Country/Territory	United Kingdom
Period	5/02/06 → 7/02/06

Bibliographical note

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

Access to Document

10.1007/11768173_6

Full textFinal published version, 108 KBLicence: CC BY-NC-ND

http://link.springer.com/10.1007/11768173_6

Cite this

@inproceedings{750f5242b29d4dc88b240f52305f045d,

title = "Constructing Property-Oriented Models for Verification",

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.",

author = "Jifeng He and Shengchao Qin and Adnan Sherif",

note = "Author can archive post-print (ie final draft post-refereeing). ; 1st International Symposium on Unifying Theories of Programming ; Conference date: 05-02-2006 Through 07-02-2006",

year = "2006",

doi = "10.1007/11768173_6",

language = "English",

series = "Unifying Theories of Programming",

pages = "85--100",

booktitle = "Unifying theories of programming",

}

TY - GEN

T1 - Constructing Property-Oriented Models for Verification

AU - He, Jifeng

AU - Qin, Shengchao

AU - Sherif, Adnan

N1 - Conference code: 1

PY - 2006

Y1 - 2006

N2 - 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.

AB - 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.

U2 - 10.1007/11768173_6

DO - 10.1007/11768173_6

M3 - Conference contribution

T3 - Unifying Theories of Programming

SP - 85

EP - 100

BT - Unifying theories of programming

T2 - 1st International Symposium on Unifying Theories of Programming

Y2 - 5 February 2006 through 7 February 2006

ER -

Constructing Property-Oriented Models for Verification

Abstract

Publication series

Conference

Bibliographical note

Access to Document

Fingerprint

Cite this