Presentation 1997/7/16
Formal Verification of Fairness for non-Zeno Real-Time Systems by Abstract Interpretation
Satoshi Yamane,
PDF Download Page PDF download Page Link
Abstract(in Japanese) (See Japanese page)
Abstract(in English) It is difficult to verify fairness in timed automata, because in some cases, timed automata can not behave infinitely often even if there is some closed cyle. On the other hand, effective formal verification based on abstract interpretation has been developed. But we can not verify fairness in timed automata by existing methods. In this paper, we proposed formal verification of fairness in timed automata based on abstract interpretation, which combine BDDs with DBMs.
Keyword(in Japanese) (See Japanese page)
Keyword(in English) Timed Automata / Abstract Interpretation / BDDs / Formal Verification
Paper # SS97-17
Date of Issue

Conference Information
Committee SS
Conference Date 1997/7/16(1days)
Place (in Japanese) (See Japanese page)
Place (in English)
Topics (in Japanese) (See Japanese page)
Topics (in English)
Chair
Vice Chair
Secretary
Assistant

Paper Information
Registration To Software Science (SS)
Language JPN
Title (in Japanese) (See Japanese page)
Sub Title (in Japanese) (See Japanese page)
Title (in English) Formal Verification of Fairness for non-Zeno Real-Time Systems by Abstract Interpretation
Sub Title (in English)
Keyword(1) Timed Automata
Keyword(2) Abstract Interpretation
Keyword(3) BDDs
Keyword(4) Formal Verification
1st Author's Name Satoshi Yamane
1st Author's Affiliation Dept. of Mathematics and Computer Science, Shimane University()
Date 1997/7/16
Paper # SS97-17
Volume (vol) vol.97
Number (no) 164
Page pp.pp.-
#Pages 8
Date of Issue