{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,3]],"date-time":"2026-04-03T22:55:20Z","timestamp":1775256920954,"version":"3.50.1"},"reference-count":83,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"4","license":[{"start":{"date-parts":[[2018,12,1]],"date-time":"2018-12-01T00:00:00Z","timestamp":1543622400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"}],"funder":[{"name":"Brazilian agencies FAPEAM","award":["062.00719\/2016"],"award-info":[{"award-number":["062.00719\/2016"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Rel."],"published-print":{"date-parts":[[2018,12]]},"DOI":"10.1109\/tr.2018.2873260","type":"journal-article","created":{"date-parts":[[2018,10,24]],"date-time":"2018-10-24T14:53:24Z","timestamp":1540392804000},"page":"1420-1441","source":"Crossref","is-referenced-by-count":16,"title":["DSVerifier-Aided Verification Applied to Attitude Control Software in Unmanned Aerial Vehicles"],"prefix":"10.1109","volume":"67","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4097-2851","authenticated-orcid":false,"given":"Lennon","family":"Chaves","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6603-3476","authenticated-orcid":false,"given":"Iury V.","family":"Bessa","sequence":"additional","affiliation":[]},{"given":"Hussama","family":"Ismail","sequence":"additional","affiliation":[]},{"given":"Adriano Bruno","family":"dos Santos Frutuoso","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6235-4272","authenticated-orcid":false,"given":"Lucas","family":"Cordeiro","sequence":"additional","affiliation":[]},{"given":"Eddie Batista","family":"de Lima Filho","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref73","doi-asserted-by":"publisher","DOI":"10.1177\/0278364911434236"},{"key":"ref72","author":"mathworks","year":"2004","journal-title":"Matlab & Simulink Student Version"},{"key":"ref71","doi-asserted-by":"publisher","DOI":"10.1109\/ROBOT.2004.1302409"},{"key":"ref70","doi-asserted-by":"publisher","DOI":"10.1142\/S0218127406016252"},{"key":"ref76","first-page":"232","article-title":"Invariant synthesis for incomplete verification engines","author":"neider","year":"2018","journal-title":"Proc Int Conf Tools and Algorithms Constr and Anal Syst"},{"key":"ref77","first-page":"360","article-title":"Depthk: A k-induction verifier based on invariant inference for C programs - (competition contribution)","author":"rocha","year":"2017","journal-title":"Proc Int Conf Tools and Algorithms Constr and Anal Syst"},{"key":"ref74","first-page":"69","article-title":"ICE: A robust framework for learning invariants","author":"garg","year":"2014","journal-title":"Proc 26th Int Conf Comput Aided Verif"},{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1016\/j.nahs.2017.08.005"},{"key":"ref75","doi-asserted-by":"crossref","first-page":"499","DOI":"10.1145\/2837614.2837664","article-title":"Learning invariants using decision trees and implication counterexamples","author":"garg","year":"2016","journal-title":"Proc 43rd Annu ACM SIGPLAN-SIGACT Symp Princ Program Lang"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1109\/ACC.2008.4586906"},{"key":"ref78","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679412"},{"key":"ref79","first-page":"1","article-title":"Interpolation and SAT-based model checking","author":"mcmillan","year":"2003","journal-title":"Proc 15th Int Conf Comput Aided Verif"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1007\/s10472-011-9270-x"},{"key":"ref32","first-page":"5081","article-title":"Verification and validation of UAV mission planning for human automation collaboration","author":"kim","year":"2014","journal-title":"Proc IIE Annu Conf Expo"},{"key":"ref31","author":"holzmann","year":"1991","journal-title":"Design and Validation of Computer Protocols Prentice-Hall Software Series"},{"key":"ref30","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1007\/978-3-319-08422-0_35","article-title":"A formal approach for identifying assurance deficits in unmanned aerial vehicle software","author":"groza","year":"2015","journal-title":"Progress in Systems Engineering"},{"key":"ref37","first-page":"99","article-title":"Software verification: Testing vs. model checking. A comparative evaluation of the state of the art","author":"beyer","year":"2017","journal-title":"Hardware and Software Verification and Testing - 13th International Haifa Verification Conference (Lecture Notes in Computer Science 10629)"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-12241-0_9"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2009.32"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1007\/s10472-014-9408-8"},{"key":"ref60","author":"\u00e5str\u00f6m","year":"1997","journal-title":"Computer-Controlled Systems Theory and Design (Prentice Hall Information and System Sciences Series)"},{"key":"ref62","first-page":"887","article-title":"Reliable and reproducible competition results with BenchExec and witnesses (report on SV-comp 2016)","author":"beyer","year":"2016","journal-title":"Proc Int Conf Tools and Algorithms Constr and Anal Syst"},{"key":"ref61","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139164580"},{"key":"ref63","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1007\/s10009-015-0407-9","article-title":"Handling loops in bounded model checking of C programs via k-induction","volume":"19","author":"gadelha","year":"2017","journal-title":"Int J Softw Tools Technol Transfer"},{"key":"ref28","first-page":"389","article-title":"CBMC - C bounded model checker (competition contribution)","volume":"8413","author":"kroening","year":"2014","journal-title":"Proc TACAS"},{"key":"ref64","first-page":"108","article-title":"Checking safety properties using induction and a sat-solver","author":"sheeran","year":"2000","journal-title":"Proc 3rd Int Conf Formal Methods Comput -Aided Des"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2011.59"},{"key":"ref65","first-page":"174","article-title":"Boolector: An efficient SMT solver for bit-vectors and arrays","author":"brummayer","year":"2009","journal-title":"Proc TACAS"},{"key":"ref66","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.20906\/CPS\/COB-2015-0401"},{"key":"ref67","doi-asserted-by":"publisher","DOI":"10.1145\/3178126.3178151"},{"key":"ref68","first-page":"851","article-title":"The implementation of recursive digital filters for high-fidelity audio","volume":"36","author":"dattorro","year":"1988","journal-title":"J Audio Eng Soc"},{"key":"ref69","doi-asserted-by":"publisher","DOI":"10.1109\/TAU.1968.1162002"},{"key":"ref2","doi-asserted-by":"crossref","DOI":"10.1016\/S1479-3601(05)07008-6","article-title":"Human factors implications of unmanned aircraft accidents: Flight-control problems","author":"williams","year":"2006"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1007\/s11460-009-0065-3"},{"key":"ref20","first-page":"1","article-title":"Verification and controller synthesis for resource-constrained real-time systems: Case study of an autonomous truck","author":"li","year":"2010","journal-title":"Proc 15th IEEE Int Conf Emerg Technol Factory Autom"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1145\/1879021.1879024"},{"key":"ref21","first-page":"636","article-title":"Self-triggered controllers and hard real-time guarantees","author":"aminifar","year":"2016","journal-title":"Proc Eur Conf Exhib Design Autom Test"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.3390\/robotics3040330"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1109\/ACC.2012.6314852"},{"key":"ref26","first-page":"126","article-title":"DSVerifier: A bounded model checking tool for digital systems","volume":"9232","author":"ismail","year":"2015","journal-title":"Proc SPIN"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1007\/s10617-016-9173-5"},{"key":"ref50","author":"yang","year":"2010","journal-title":"Reliable Control and Filtering of Linear Systems with Adaptive Mechanisms (Automation and Control Engineering)"},{"key":"ref51","doi-asserted-by":"publisher","DOI":"10.1002\/rnc.618"},{"key":"ref59","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-031-02533-4","author":"padgett","year":"2009","journal-title":"Fixed-Point Signal Processing (Synthesis Lectures on Signal Processing)"},{"key":"ref58","first-page":"1","article-title":"Simulink design verifier – Applying automated formal methods to simulink and stateflow","author":"hamon","year":"2008","journal-title":"Proc 3rd Workshop Autom Formal Methods"},{"key":"ref57","author":"munier","year":"2013","journal-title":"Polyspace"},{"key":"ref56","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1007\/11513988_21","article-title":"Compositional analysis of floating-point linear numerical filters","author":"monniaux","year":"2005","journal-title":"Comput Aided Verif"},{"key":"ref55","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1007\/s10009-012-0249-7","article-title":"Program sketching","volume":"15","author":"solar-lezama","year":"2013","journal-title":"Int J Softw Tools Technol Transfer"},{"key":"ref54","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2016.2593947"},{"key":"ref53","doi-asserted-by":"crossref","first-page":"462","DOI":"10.1007\/978-3-319-63387-9_23","article-title":"Automated formal synthesis of digital controllers for state-space physical plants","author":"abate","year":"2017","journal-title":"Comput Aided Verif"},{"key":"ref52","first-page":"1","article-title":"Sound and automated synthesis of digital stabilizing controllers for continuous plants","author":"abate","year":"2017","journal-title":"Proc 20th ACM Int Conf Hybrid Syst Comput Control"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1109\/REAL.1995.495196"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1145\/2038642.2038685"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1145\/775832.775998"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.422"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050046"},{"key":"ref82","doi-asserted-by":"publisher","DOI":"10.1109\/78.97995"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1145\/1810295.1810314"},{"key":"ref81","doi-asserted-by":"publisher","DOI":"10.1201\/b14766"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1109\/DASC.2002.1067982"},{"key":"ref18","first-page":"68","article-title":"Integration of formal analysis into a model-based software development process","volume":"4916","author":"whalen","year":"2008","journal-title":"Proc FMICS"},{"key":"ref83","doi-asserted-by":"publisher","DOI":"10.1109\/78.539026"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1109\/CMPASS.1996.507877"},{"key":"ref80","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679405"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.2514\/6.2011-1472"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.2514\/1.5588"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1016\/j.actaastro.2008.07.019"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.2514\/6.2012-4723"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1990.113766"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1016\/j.ijproman.2009.01.004"},{"key":"ref49","doi-asserted-by":"publisher","DOI":"10.1016\/j.ijepes.2014.07.054"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-40007-3_22"},{"key":"ref46","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1007\/978-3-662-54577-5_9","article-title":"Automatic verification of finite precision implementations of linear controllers","author":"park","year":"2017","journal-title":"Lecture Notes in Computer Science"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1109\/CACSD.2008.4627366"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2016.2601328"},{"key":"ref47","first-page":"662","article-title":"Scalable verification of linear controller software","author":"park","year":"2016","journal-title":"Proc Int Conf Tools and Algorithms Constr and Anal Syst"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.23919\/ECC.2007.7068839"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1080\/00207170903160747"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1109\/MCS.2010.938196"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1109\/ACSSC.2015.7421231"}],"container-title":["IEEE Transactions on Reliability"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/24\/8552524\/08506399.pdf?arnumber=8506399","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,3]],"date-time":"2026-04-03T21:32:13Z","timestamp":1775251933000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/8506399\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,12]]},"references-count":83,"journal-issue":{"issue":"4"},"URL":"https:\/\/doi.org\/10.1109\/tr.2018.2873260","relation":{},"ISSN":["0018-9529","1558-1721"],"issn-type":[{"value":"0018-9529","type":"print"},{"value":"1558-1721","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,12]]}}}