Property-based Code Slicing for Efficient Verification of OSEK/VDX Operating Systems

Mingyu Park, Taejoon Byun, Yunja Choi

Research output: Contribution to journalConference articlepeer-review

5 Scopus citations


Testing is a de-facto verification technique in industry, but insufficient for identifying subtle issues due to its optimistic incompleteness. On the other hand, model checking is a powerful technique that supports comprehensiveness, and is thus suitable for the verification of safety-critical systems. However, it generally requires more knowledge and cost more than testing. This work attempts to take advantage of both techniques to achieve integrated and efficient verification of OSEK/VDX-based automotive operating systems. We propose property-based environment generation and model extraction techniques using static code analysis, which can be applied to both model checking and testing. The technique is automated and applied to an OSEK/VDX-based automotive operating system, Trampoline. Comparative experiments using random testing and model checking for the verification of assertions in the Trampoline kernel code show how our environment generation and abstraction approach can be utilized for efficient fault-detection.

Original languageEnglish
Pages (from-to)69-84
Number of pages16
JournalElectronic Proceedings in Theoretical Computer Science, EPTCS
StatePublished - 29 Dec 2012
Event1st International Workshop on Formal Techniques for Safety-Critical Systems, FTSCS 2012 - Kyoto, Japan
Duration: 12 Nov 2012 → …


Dive into the research topics of 'Property-based Code Slicing for Efficient Verification of OSEK/VDX Operating Systems'. Together they form a unique fingerprint.

Cite this