Show simple item record

Automatic Verification of Finite Precision Implementations of Linear Controllers

dc.contributor.authorJunkil Park
dc.contributor.authorMiroslav Pajic
dc.contributor.authorOleg Sokolsky
dc.contributor.authorInsup Lee
dc.date.accessioned2017-06-01T15:25:42Z
dc.date.available2017-06-01T15:25:42Z
dc.date.issued2017-04-30
dc.identifier.urihttp://hdl.handle.net/11540/6963
dc.description.abstractWe consider the problem of verifying finite precision implementation of linear time-invariant controllers against mathematical specifications. A specification may have multiple correct implementations which are different from each other in controller state representation, but equivalent from a perspective of input-output behavior (e.g., due to optimization in a code generator). The implementations may use finite precision computations (e.g. floating-point arithmetic) which cause quantization (i.e., roundoff) errors. To address these challenges, we first extract a controller's mathematical model from the implementation via symbolic execution and floating-point error analysis, and then check approximate input-output equivalence between the extracted model and the specification by similarity checking. We show how to automatically verify the correctness of floating-point controller implementation in C language using the combination of techniques such as symbolic execution and convex optimization problem solving. We demonstrate the scalability of our approach through evaluation with randomly generated controller specifications of realistic size.
dc.languageEnglish
dc.publisherThink Tanks and Civil Societies Program
dc.titleAutomatic Verification of Finite Precision Implementations of Linear Controllers
dc.typeReports
dc.subject.expertProject impact
dc.subject.expertDevelopment projects
dc.subject.expertProgram management
dc.subject.expertPerformance appraisal
dc.subject.expertProject appraisal
dc.subject.expertTechnology assessment
dc.subject.adbResults-Based Monitoring And Evaluation
dc.subject.adbProject Evaluation & Review Technique
dc.subject.adbProject Evaluation
dc.subject.adbProgram Evaluation
dc.subject.adbPerformance Evaluation
dc.subject.adbOperations Evaluation
dc.subject.adbEvaluation Methods
dc.subject.adbEvaluation
dc.subject.naturalCumulative effects assessment
dc.subject.naturalGrievance procedures
dc.subject.naturalParticipatory monitoring and evaluation
dc.title.seriesCIS Paper
dc.title.volume822
dc.contributor.imprintThink Tanks and Civil Societies Program
oar.themeEvaluation
oar.adminregionAsia and the Pacific Region
oar.countryBangladesh
oar.countryBhutan
oar.countryIndia
oar.countryMaldives
oar.countryNepal
oar.countrySri Lanka
oar.countryBrunei Darussalam
oar.countryCambodia
oar.countryIndonesia
oar.countryLao People's Democratic
oar.countryMalaysia
oar.countryMyanmar
oar.countryPhilippines
oar.countrySingapore
oar.countryThailand
oar.countryViet Nam
oar.countryCook Islands
oar.countryFiji Islands
oar.countryKiribati
oar.countryMarshall Islands
oar.countryFederated States of Micronesia
oar.countryNauru
oar.countryPalau
oar.countryPapua New Guinea
oar.countrySamoa
oar.countrySolomon Islands
oar.countryTimor-Leste
oar.countryTonga
oar.countryTuvalu
oar.countryVanuatu
oar.countryAfghanistan
oar.countryArmenia
oar.countryAzerbaijan
oar.countryGeorgia
oar.countryKazakhstan
oar.countryKyrgyz Republic
oar.countryPakistan
oar.countryTajikistan
oar.countryTurkmenistan
oar.countryUzbekistan
oar.countryPeople's Republic of China
oar.countryHong Kong
oar.countryChina
oar.countryRepublic of Korea
oar.countryMongolia
oar.countryTaipei,China
oar.identifierOAR-006616
oar.authorPark, Junkil
oar.authorPajic, Miroslav
oar.authorSokolsky, Oleg
oar.authorLee, Insup
oar.importTRUE
oar.googlescholar.linkpresenttrue


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record