從程式語言到時間自動機的自動化轉譯程式之建立

The Implementation of Automated Translator from Programming Language to Timed Automata

王立德(Lih-der Wang)

指導教授 ： 王凡

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

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

摘要

程式語言擁有非常強大的能力和十分複雜的結構，因此驗證一個透過程式語言所完成的軟體將會非常困難。如果程式設計師遵循一項已經驗證過的協定來寫程式，也有可能在寫程式的過程中發生錯誤，所以對最終的程式進行驗證是很重要的。根據程式的執行流程，程式可以被視為一個具有多個程序的即時系統，而原始程式中每個獨立的片段則代表一個程序。轉譯程式將依照程式語言的文法，把程式轉譯成正規驗證模型，透過對模型的驗證，可以達成驗證程式的目的。可以對個別的程式模型進行驗證，以簡化驗證的困難度。轉譯程式的自動化是為避免在轉譯的過程中發生錯誤的可能，並把產生正規模型的過程予以簡化。我們將C語言程式透過自動轉譯程式，轉譯成時間自動機的模型，而模型本身是用Red的語法來描述。

關鍵字

自動驗證 ； 轉譯程式 ； 時間自動機

並列摘要

General purpose programming languages are rich in functionalities and therefore have complicated structures. Hence verifying software programs written in such programming languages can be very difficult. Even if the technical specifications had been verified to be error-free, there may still be errors introduced by the actual implementation. It is important that the verification is performed on the final program. Based on the work flow, a program can be considered as a real-time system with many processes, where each process is represented by a fragment of the original program. According to the grammars of the specific programming language, an automated translator can be used to translate the programs into corresponding formal verification models. The whole program can then be verified by applying the standard verification techniques to each model individually. The automation of translation can simplify the task of creating a formal model and identify potential errors in the implementation. We will present our implementation of a program that translates basic C programs into timed automata described by Red.

並列關鍵字

Timed Automata ； Automated Verification ； Translator

參考文獻

1.R. Alur, C. Courcoubetis, D.L. Dill, Model Checking for Real Time Systems, IEEE LICS, 1990.

2.M. Ancona, G. Dodero, V. Gianuzzi, M. Morgavi, Efficient Construction of LR(k) States and Tables, ACM TOPLAS, VOL. 13, NO. 1, pp.150-178, 1991.

3.L.L. Beck, System Software: An Introduction to Systems Programming, 2ed, Addison-Wesley, 1990.

4.J. Bengtsson, K.G. Larsen, F. Larsson, P. Pettersson, W. Yi, UPPAAL — A Tool Suite for Automatic Verification of Real–Time Systems, in Proceedings of the DIMACS/SYCON workshop on Hybrid systems, pp. 232-243, Springer-Verlag, 1996.

5.H.K. Berg, Formal Methods of Program Verification and Specification, Prentice-Hall, 1982.