https://scholars.lib.ntu.edu.tw/handle/123456789/148086
標題: | TCTL Inevitability Analysis of Dense-Time Systems: From Theory to Engineering | 作者: | Wang, Farn Huang, Geng-Dian Yu, Fang |
關鍵字: | TCTL;real-time systems;inevitability;non-Zeno;model-checking;greatest fixpoint;abstraction | 公開日期: | 七月-2006 | 出版社: | Taipei:National Taiwan University Dept Mech Engn | 卷: | VOL. 28 | 期: | NO. 7 | 起(迄)頁: | 510-526 | 來源出版物: | IEEE Transactions on Software Engineering | 摘要: | Inevitability properties in branching temporal logics are of the syntax 8} , where is an arbitrary (timed) CTL (Computation Tree Logic) formula. Such inevitability properties in dense-time logics can be analyzed with the greatest fixpoint calculation. We present algorithms to model-check inevitability properties. We discuss a technique for early decision on greatest fixpoint calculation which has shown promising performance against several benchmarks. We have experimented with various issues which may affect the performance of TCTL inevitability analysis. Specifically, our algorithms come with a parameter for the measurement of timeprogress. We report the performance of our implementation with regard to various parameter values and with or without the non-Zeno computation requirement in the evaluation of greatest fixpoints. We have also experimented with safe abstraction techniques for model-checking TCTL inevitability properties. The experiment results help us in deducing rules for setting the parameter for verification performance. Finally, we summarize suggestions for configurations of efficient TCTL inevitability evaluation procedure. |
URI: | http://ntur.lib.ntu.edu.tw//handle/246246/200611150121460 http://ntur.lib.ntu.edu.tw/bitstream/246246/200611150121460/1/555.pdf |
其他識別: | 246246/200611150121460 | DOI: | 10.1109/TSE.2006.71 |
顯示於: | 電機工程學系 |
在 IR 系統中的文件,除了特別指名其著作權條款之外,均受到著作權保護,並且保留所有的權利。