Please use this identifier to cite or link to this item: https://doi.org/10.1145/1734229.1734232
DC FieldValue
dc.titleA verification system for interval-based specification languages
dc.contributor.authorChen, C.
dc.contributor.authorDong, J.S.
dc.contributor.authorSun, J.
dc.contributor.authorMartin, A.
dc.date.accessioned2013-07-04T07:30:31Z
dc.date.available2013-07-04T07:30:31Z
dc.date.issued2010
dc.identifier.citationChen, C., Dong, J.S., Sun, J., Martin, A. (2010). A verification system for interval-based specification languages. ACM Transactions on Software Engineering and Methodology 19 (4). ScholarBank@NUS Repository. https://doi.org/10.1145/1734229.1734232
dc.identifier.issn1049331X
dc.identifier.urihttp://scholarbank.nus.edu.sg/handle/10635/38948
dc.description.abstractInterval-based specification languages have been used to formally model and rigorously reason about real-time computing systems. This usually involves logical reasoning and mathematical computation with respect to continuous or discrete time. When these systems are complex, analyzing their models by hand becomes error-prone and difficult. In this article, we develop a verification system to facilitate the formal analysis of interval-based specification languages with machine-assisted proof support. The verification system is developed using a generic theorem prover, Prototype Verification System (PVS). Our system elaborately encodes a highly expressive set-based notation, Timed Interval Calculus (TIC), and can rigorously carry out the verification of TIC models at an interval level. We validated all TIC reasoning rules and discovered subtle flaws in the original rules. We also apply TIC to model Duration Calculus (DC), which is a popular interval-based specification language, and thus expand the capacity of the verification system. We can check the correctness of DC axioms, and execute DC proofs in a manner similar to the corresponding pencil-and-paper DC arguments. © 2010 ACM.
dc.description.urihttp://libproxy1.nus.edu.sg/login?url=http://dx.doi.org/10.1145/1734229.1734232
dc.sourceScopus
dc.subjectFormal specification languages
dc.subjectReal-time systems
dc.subjectTheorem proving
dc.typeArticle
dc.contributor.departmentCOMPUTER SCIENCE
dc.description.doi10.1145/1734229.1734232
dc.description.sourcetitleACM Transactions on Software Engineering and Methodology
dc.description.volume19
dc.description.issue4
dc.description.codenATSME
dc.identifier.isiut000277058100003
Appears in Collections:Staff Publications

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

SCOPUSTM   
Citations

8
checked on Aug 14, 2019

WEB OF SCIENCETM
Citations

1
checked on Aug 7, 2019

Page view(s)

82
checked on Aug 19, 2019

Google ScholarTM

Check

Altmetric


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