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 |