Please use this identifier to cite or link to this item: https://doi.org/10.1145/1368088.1368126
DC FieldValue
dc.titleA verification system for timed interval calculus
dc.contributor.authorChen, C.
dc.contributor.authorDong, J.S.
dc.contributor.authorSun, J.
dc.date.accessioned2013-07-04T07:55:21Z
dc.date.available2013-07-04T07:55:21Z
dc.date.issued2008
dc.identifier.citationChen, C., Dong, J.S., Sun, J. (2008). A verification system for timed interval calculus. Proceedings - International Conference on Software Engineering : 271-280. ScholarBank@NUS Repository. https://doi.org/10.1145/1368088.1368126
dc.identifier.isbn9781605580791
dc.identifier.issn02705257
dc.identifier.urihttp://scholarbank.nus.edu.sg/handle/10635/40042
dc.description.abstractTimed Interval Calculus (TIC) is a highly expressive set-based notation for specifying and reasoning about embedded real-time systems. However, it lacks mechanical proving support, as its verification usually involves infinite time intervals and continuous dynamics. In this paper, we develop a system based on a generic theorem prover, Prototype Verification System (PVS), to assist formal verification of TIC at a high grade of automation. TIC semantics has been constructed by the PVS typed higher-order logic. Based on the encoding, we have checked all TIC reasoning rules and discovered subtle flaws. A translator has been implemented in Java to automatically transform TIC models into PVS specifications. A collection of supplementary rules and PVS strategies has been defined to facilitate the rigorous reasoning of TIC models with functional and non-functional (for example, real-time) requirements at the interval level. Our approach is generic and can be applied further to support other real-time notations. Copyright 2008 ACM.
dc.description.urihttp://libproxy1.nus.edu.sg/login?url=http://dx.doi.org/10.1145/1368088.1368126
dc.sourceScopus
dc.subjectPVS
dc.subjectReal-Time Systems
dc.subjectSpecification Language
dc.subjectTheorem Proving
dc.typeConference Paper
dc.contributor.departmentCOMPUTER SCIENCE
dc.description.doi10.1145/1368088.1368126
dc.description.sourcetitleProceedings - International Conference on Software Engineering
dc.description.page271-280
dc.description.codenPCSED
dc.identifier.isiut000259592000051
Appears in Collections:Staff Publications

Show simple item record
Files in This Item:
There are no files associated with this item.

SCOPUSTM   
Citations

5
checked on Nov 18, 2019

WEB OF SCIENCETM
Citations

5
checked on Nov 18, 2019

Page view(s)

87
checked on Oct 28, 2019

Google ScholarTM

Check

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.