Show simple item record

dc.contributor.advisorFeron, Eric M.
dc.contributor.authorWang, Timothy
dc.date.accessioned2015-09-21T14:27:19Z
dc.date.available2015-09-21T14:27:19Z
dc.date.created2015-08
dc.date.issued2015-07-27
dc.date.submittedAugust 2015
dc.identifier.urihttp://hdl.handle.net/1853/53954
dc.description.abstractFormal methods is a discipline of using a collection of mathematical techniques and formalisms to model and analyze software systems. Motivated by the new formal methods-based certification recommendations for safety-critical embedded software and the significant increase in the cost of verification and validation (V\&V), this research is about creating a software development process for control systems that can provide mathematical guarantees of high-level functional properties on the code. The process, dubbed credible autocoding, leverages control theory in the automatic generation of control software documented with proofs of their stability and performance. The main output of this research is an automated, credible autocoding prototype that transforms the Simulink model of the controller into C code documented with a code-level proof of the stability of the controller. The code-level proof, expressed using a formal specification language, are embedded into the code as annotations. The annotations guarantee that the auto-generated code conforms to the input model to the extent that key properties are satisfied. They also provide sufficient information to enable an independent, automatic, formal verification of the auto-generated controller software.
dc.format.mimetypeapplication/pdf
dc.language.isoen_US
dc.publisherGeorgia Institute of Technology
dc.subjectFormal methods
dc.subjectControl
dc.subjectLyapunov
dc.subjectSafety-critical software
dc.subjectModel-based development
dc.subjectVerification & validation
dc.titleCredible autocoding of control software
dc.typeDissertation
dc.description.degreePh.D.
dc.contributor.departmentAerospace Engineering
thesis.degree.levelDoctoral
dc.contributor.committeeMemberHolzinger, Marcus
dc.contributor.committeeMemberTsiotras, Panagiotis
dc.contributor.committeeMemberGaroche, Pierre-Loic
dc.contributor.committeeMemberPantel, Marc
dc.date.updated2015-09-21T14:27:19Z


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record