嵌入式系統在正規化模型語法上的增進與提升

隨著軟硬體設計複雜度快速地增加，傳統的驗證技術已不敷使用。許多人把焦點進而轉向了正規驗證，希望能利用正規驗證的技術來達成更有效率及可靠的驗證。正規驗證的技術可以幫助我們輕易且自動化地找出潛藏的設計錯誤。然而正規驗證的技術並不是完全毫無缺點，與其他驗證技術相比，其中一項較為弱勢的地方在於描述待驗證系統的正規語言。正規語言為了配合數學模型，其本身的語法通常較為精簡，換句話說在描述較複雜的系統時，也相對的較為困難。因此，我們欲開發一個正規模型函式庫，來改善正規語言的不足。利用自動轉譯成原有語法的方式，使得我們可以在不改變原有驗證系統核心的情況下，輕易地使用較高階的語法來描述待驗證系統，以縮短建立正規化模型的時間。目前正規模型函式庫包含了channel, array, memory allocation, procedure call及timer。

關鍵字

正規方法；正規驗證；正規化模型；函式庫；語法

並列摘要

With the rapidly increasing design complexity, traditional techniques for validness such as simulation and testing are not su cient. The formal methods for verification have become the limelight. The corner cases might be detected easily and automatically by these formal techniques. In spite of the fact that formal verification is such powerful, the formal methods have still been limited to some issues. One subject is that the formal languages are too simple to describe the design systems. Hence we construct a model library which contains channel, array, memory allocation, procedure call, and timer currently to improve the work of building model.

並列關鍵字

formal methods ； formal verification ； formal model ； library ； syntax

參考文獻

[2] E. M. Clarke and E. A. Emerson, Design and synthesis of synchronization skeletons using branching-time temporal logic. Lecture Notes in Computer Science, Logic of Programs. Heidelberg, Germany: Springer-Verlag, 1981, vol.

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

[5] E.A. Emerson, C.-L. Lei. Modalities for Model Checking: Branching Time Logic Strikes Back, Science of Computer Programming 8 (1987), pp.275-306, Elsevier Science Publishers B.V. (North-Holland).

Santa Barbara, CA, USA.

[8] F. Wang. E cient Data-Structure for Fully Symbolic Verification of Real-Time Software Systems. TACAS’2000, March, Berlin, Germany. in LNCS 1785, Springer-Verlag.

國際替代計量

嵌入式系統在正規化模型語法上的增進與提升

主題瀏覽