Please use this identifier to cite or link to this item:
|Title:||A verification system for interval-based specification languages|
|Authors:||Chen, C. |
|Keywords:||Formal specification languages|
|Citation:||Chen, 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|
|Abstract:||Interval-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.|
|Source Title:||ACM Transactions on Software Engineering and Methodology|
|Appears in Collections:||Staff Publications|
Show full item record
Files in This Item:
There are no files associated with this item.
checked on Nov 16, 2018
WEB OF SCIENCETM
checked on Nov 22, 2017
checked on Sep 29, 2018
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.