The Implementation of Automated Translator from Programming Language to Timed Automata
Date Issued
2004
Date
2004
Author(s)
Wang, Lih-der
DOI
zh-TW
Abstract
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.
Subjects
自動驗證
轉譯程式
時間自動機
Timed Automata
Automated Verification
Translator
Type
thesis
File(s)![Thumbnail Image]()
Loading...
Name
ntu-93-R91921085-1.pdf
Size
23.31 KB
Format
Adobe PDF
Checksum
(MD5):95e6dcd6702bb79b3201dbb54fa44032