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:

Download

Collections

Theses and Dissertations