UM  > 科技學院
Verifying Duration Properties of Timed Transition Systems
Liu, Zhiming1; Ravn, Anders2; Li, Xiaoshan3
1998
Source PublicationProgramming Concepts and Methods PROCOMET ’98
Author of SourceEdited by David Gries, Willem-Paul de Roever
PublisherSpringer, Boston, MA
Pages327-345
Abstract

This paper proposes a method for formal real-time systems development: Requirements and high level design decisions are time interval properties and are therefore specified in the Duration Calculus (DC), while implementations are described by timed transition systems (TTS). A link from implementation properties to the requirement and design properties is given by interpreting a DC formula in a model of the executions of a TTS and then providing rules for lifting properties proved by structural induction for a TTS to DC formulas. The method is illustrated by the Gas Burner case study.

KeywordReal-time Systems Duration Calculus Timed Transition Systems Specification Verification
DOI10.1007/978-0-387-35358-6_22
URLView the original
Language英语
Fulltext Access
Citation statistics
Document TypeBook chapter
CollectionFaculty of Science and Technology
DEPARTMENT OF COMPUTER AND INFORMATION SCIENCE
Affiliation1.University of Leicester
2.Technical University of Denmark
3.University of Macau
Recommended Citation
GB/T 7714
Liu, Zhiming,Ravn, Anders,Li, Xiaoshan. Verifying Duration Properties of Timed Transition Systems:Springer, Boston, MA,1998:327-345.
Related Services
Recommend this item
Bookmark
Usage statistics
Export to Endnote
Google Scholar
Similar articles in Google Scholar
[Liu, Zhiming]'s Articles
[Ravn, Anders]'s Articles
[Li, Xiaoshan]'s Articles
Baidu academic
Similar articles in Baidu academic
[Liu, Zhiming]'s Articles
[Ravn, Anders]'s Articles
[Li, Xiaoshan]'s Articles
Bing Scholar
Similar articles in Bing Scholar
[Liu, Zhiming]'s Articles
[Ravn, Anders]'s Articles
[Li, Xiaoshan]'s Articles
Terms of Use
No data!
Social Bookmark/Share
All comments (0)
No comment.
 

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