An approach to translate LUSTRE code to ACL2

dc.contributor.author Dhingra, Ruchi
dc.date 2019-07-10T01:44:19.000
dc.date.accessioned 2020-06-30T08:11:17Z
dc.date.available 2020-06-30T08:11:17Z
dc.date.copyright Sat Jan 01 00:00:00 UTC 2005
dc.date.issued 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/lib.dr.iastate.edu/rtd/18876/
dc.identifier.articleid 19876
dc.identifier.contextkey 14540677
dc.identifier.s3bucket isulib-bepress-aws-west
dc.identifier.submissionpath rtd/18876
dc.identifier.uri https://dr.lib.iastate.edu/handle/20.500.12876/72823
dc.language.iso en
dc.source.bitstream archive/lib.dr.iastate.edu/rtd/18876/Dhingra_ISU_2005_D52.pdf|||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
thesis.degree.discipline Computer Science
thesis.degree.level thesis
thesis.degree.name Master of Science
File
Original bundle
Now showing 1 - 1 of 1
Name:
Dhingra_ISU_2005_D52.pdf
Size:
913.75 KB
Format:
Adobe Portable Document Format
Description: