Automotive operating system is a safety-critical software that controls electrical devices installed in automobiles. It is supposed to work safely under any arbitrary interactions with application programs, which is a major difficulty in safety verification. It is important to model a sound environment that satisfies system requirements and constraints in order to ensure efficiency and effectiveness of verification.
This talk introduces my approach to address this issue using constraint patterns identified from the OSEK/VDX international standard for automotive operating systems. Constraint patterns are formalized and used to partition potentially infinite operational environment of operating systems, from which test sequences are generated using LTL model checking. The effectiveness of this approach will be discussed with a case study on an open-source automotive operating system.
Yunja Choi is an Associate Professor at Kyunpook National University (KNU), Daegu, South Korea. She received her PhD in Computer Science, University of Minnesota, USA, in 2003. Before joining KNU in 2006, she worked at the Fraunhofer Institute of Experimental Software Engineering (Fraunhofer IESE) in Germany as a scientist. Her research interests include software safety analysis, formal engineering methodology, and formal methods for component-based software development.