嵌入式系統驗證函式庫之建立:以電子寵物商店進行實驗

Library Construction for Embedded System Verification: An Experiment with JPetStore

蔡麟讚(Lin-Zan Cai)

指導教授 ： 王凡

國立臺灣大學/電機資訊學院/電機工程學研究所/碩士(2005年)

https://doi.org/10.6342/NTU.2005.01766

摘要

RED整合CRD的技術和HRD的技術而成為能處理時間自動機和線性混合自動機之圖像式TCTL樹狀時態邏輯檢證/模擬工具。為了要將RED能處理稠密時間系統及線性混合系統的圖像式驗證技術分享出去，並發展出RED更多的應用方式，以及提供一個更有彈性且更具效率的正規模型建構途徑，我們著手開發RED的函式庫介面：REDLIB。並且在這篇論文中，以用JAVA寫成之全新的電子寵物商店範例JPetStore為例進行實驗，展示如何以REDLIB來建構出正規模型和發展出更多之應用可能。

關鍵字

驗證 ； 模型檢驗 ； 正規模型 ； 函式庫 ； 嵌入式系統 ； 電子寵物商店

並列摘要

RED(Region-Encoding Diagram) is an integrated symbolic TCTL model-checker/simulator for timed automata with CRD (Clock-Restriction Diagram) technology and linear hybrid automata with HRD (Hybrid-Restriction Diagram) technology. In order to share the symbolic verification technology of RED for dense-time systems and linear hybrid systems, develop more other applications on RED, and provide a more flexible and efficient way of formal method construction.
We construct the library interface of RED, REDLIB, and do an experiment with JPetStore which is a completely new implementation of Pet Store demo application written in Java. This experiment demonstrates how to use REDLIB to construct verification applications.

並列關鍵字

verification ； model checking ； formal model ； library ； embedded system ； JPetStore

參考文獻

[2]R. Alur, C. Courcoubetis, D.L. Dill. Model Checking for Real-Time Systems.IEEE LICS, 1990.

[3]R. Alur, C.Courcoubetis, T.A. Henzinger, P.-H. Ho. Hybrid Automata: an Algorithmic Approach to the Specification and Verification of Hybrid Systems. Proceedings of HYBRID'93, LNCS 736, Springer-Verlag, 1993.

[5]F. Balarin. Approximate Reachability Analysis of Timed Automata. IEEE RTSS, 1996.

[6]J.R. Burch, E.M. Clarke, K.L. McMillan, D.L.Dill, L.J. Hwang. Symbolic Model Checking: 10^{20} States and Beyond.IEEE LICS, 1990.

Efficient Timed Reachability Analysis Using Clock Difference Diagrams. CAV'99, July, Trento, Italy, LNCS 1633, Springer-Verlag.