An approach to translate LUSTRE code to ACL2

Date
2005-01-01
Authors
Dhingra, Ruchi
Major Professor
Advisor
Committee Member
Journal Title
Journal ISSN
Volume Title
Publisher
Altmetrics
Authors
Research Projects
Organizational Units
Journal Issue
Series
Department
Abstract

In this thesis, we propose an approach to translate LUSTRE code to ACL2 code. The languages are very different and the translation is non-trivial. We have also validated our approach by translating and comparing results for many non-trivial test cases. There is more than one way to perform the translation. Although, the proposed approach has performance inefficiencies - these do not matter because the main reason for the translation is to prove properties of the model. The proving operation does not require execution of the programs. The proposed approach has some key benefits such as it can be verified by execution - and that the resulting ACL2 code structure matches the input LUSTRE code structure. This makes it easier to use the theorem prover to prove properties of the program. This translation work is important in the real-world. For example, it will allow Rockwell Collins to verify the correctness of models developed in Simulink, SCADE and LUSTRE using ACL2. The aforementioned tools are widely used in the aviation industry - in particular by Airbus and Boeing.

Comments
Description
Keywords
Citation
DOI
Source