An approach to translate LUSTRE code to ACL2 Dhingra, Ruchi 2019-07-10T01:44:19.000 2020-06-30T08:11:17Z 2020-06-30T08:11:17Z Sat Jan 01 00:00:00 UTC 2005 2005-01-01
dc.description.abstract <p>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.</p>
dc.format.mimetype application/pdf
dc.identifier archive/
dc.identifier.articleid 19876
dc.identifier.contextkey 14540677
dc.identifier.s3bucket isulib-bepress-aws-west
dc.identifier.submissionpath rtd/18876
dc.language.iso en
dc.source.bitstream archive/|||Fri Jan 14 21:47:15 UTC 2022
dc.subject.keywords Computer Science
dc.title An approach to translate LUSTRE code to ACL2
dc.type article
dc.type.genre thesis
dspace.entity.type Publication Computer Science thesis Master of Science
Original bundle
Now showing 1 - 1 of 1
913.75 KB
Adobe Portable Document Format