Model checking embedded control software using OS-in-the-loop CEGAR
Verification of multitasking embedded software requires taking into account its underlying operating system w.r.t. its scheduling policy and handling of task priorities in order to achieve a higher degree of accuracy. However, such comprehensive verification of multitasking embedded software together with its underlying operating system is very costly and impractical. To reduce the verification cost while achieving the desired accuracy, we propose a variant of CEGAR, named OiL-CEGAR (OS-in-the-Loop Counterexample-Guided Abstraction Refinement), where a composition of a formal OS model and an abstracted application program is used for comprehensive verification and is successively refined using the counterexamples generated from the composition model. The refinement process utilizes the scheduling information in the counterexample, which acts as a mini-OS to check the executability of the counterexample trace on the concrete program. Our experiments using a prototype implementation of OiL-CEGAR show that OiL-CEGAR greatly improves the accuracy and efficiency of property checking in this domain. It automatically removed all false alarms and accomplished property checking within an average of 476 seconds over a set of multitasking programs, whereas model checking using existing approaches over the same set of programs either showed an accuracy of under 11.1% or was unable to finish the verification due to timeout.
Wed 13 Nov
13:40 - 15:20: Papers - Verification and Bug Detection at Cortez 1 Chair(s): Raghavan KomondoorIndian Institute of Science, Bangalore | ||||||||||||||||||||||||||||||||||||||||||
13:40 - 14:00 Talk | Mutation Analysis for Coq Ahmet CelikThe University of Texas at Austin, Karl PalmskogUniversity of Texas at Austin, Marinela ParovicThe University of Texas at Austin, Emilio Jesús Gallego AriasMINES ParisTech, Milos GligoricThe University of Texas at Austin | |||||||||||||||||||||||||||||||||||||||||
14:00 - 14:20 Talk | Verifying Arithmetic in Cryptographic C Programs Jiaxiang LiuShenzhen University, Xiaomu ShiShenzhen University, Ming-Hsien TsaiAcademia Sinica, Taiwan, Bow-Yaw WangAcademia Sinica, Bo-Yin YangAcademia Sinica Pre-print | |||||||||||||||||||||||||||||||||||||||||
14:20 - 14:40 Talk | Model checking embedded control software using OS-in-the-loop CEGAR Pre-print | |||||||||||||||||||||||||||||||||||||||||
14:40 - 15:00 Talk | Get rid of inline assembly through verification-oriented lifting Frédéric RecoulesCEA LIST, Sebastien BardinCEA LIST, Richard BonichonCEA LIST, Laurent MounierUniversité Grenoble Alpes, Marie-Laure PotetUniversité Grenoble Alpes DOI Pre-print | |||||||||||||||||||||||||||||||||||||||||
15:00 - 15:10 Demonstration | VeriAbs : Verification by Abstraction and Test Generation Mohammad AfzalTata Cosultancy Services, A AsiaTata Cosultancy Services, Avriti ChauhanTata Cosultancy Services, Bharti ChimdyalwarTata Consultancy Services, Priyanka DarkeTata Consultancy Services, Advaita DatarTata Consultancy Services Ltd, Shrawan KumarTata Cosultancy Services, R VenkateshTata Research Development and Design Centre | |||||||||||||||||||||||||||||||||||||||||
15:10 - 15:20 Demonstration | SGUARD: A Feature-based Clustering Tool for Effective Spreadsheet Defect Detection Da LiState Key Lab. for Novel Software Tech. and Dept. of Comp. Sci. and Tech., Nanjing University, Nanjing, China, Huiyan WangState Key Lab. for Novel Software Tech. and Dept. of Comp. Sci. and Tech., Nanjing University, Nanjing, China, Chang XuNanjing University, Ruiqing ZhangSearch Tech. Center Asia, Microsoft, Suzhou, China, Shing-Chi CheungDepartment of Computer Science and Engineering, The Hong Kong University of Science and Technology, Xiaoxing MaState Key Lab. for Novel Software Tech. and Dept. of Comp. Sci. and Tech., Nanjing University |