Environment for Symbolic Automation Verification Tool of Hybrid
Date Issued
2004-07-31
Date
2004-07-31
Author(s)
DOI
922213E002104
Abstract
With the three-year support from NSC,
we aim at developing the verification tool :
RED (Region-Encoding Diagram). At this
moment, there lacks a specification language
for distributed real-time system properties
involving states and events. There also
lacks a language for fairness assumptions in
dense-time systems. We have defined a
new temporal logic, TECTLf, for the flexible
specification of distributed real-time
systems with constraints involving events,
states, and fairness assumptions.
Then we have also designed algorithms for
model-checking TECTLf formulas.
Finally, we have endeavored to implement
and experiment the ideas in our tool, RED
5.1.
Publisher
臺北市：國立臺灣大學電機工程學系暨研究所
Type
report
File(s)![Thumbnail Image]()
Loading...
Name
922213E002104.pdf
Size
129.01 KB
Format
Adobe PDF
Checksum
(MD5):422ea5c38399cd5f87a6de4b82bd79ce