PRECISE Seminar: Constraint Specification & Test Generation for OSEK/VDX-based Operating Systems

PRECISE Seminar: Constraint Specification & Test Generation for OSEK/VDX-based Operating Systems
Mon, August 4, 2014 @ 4:00pm EDT
Levine Hall - Room 512
3330 Walnut Street
Philadelphia, PA 19104
Speaker
Yunja Choi, Ph.D.
Kyunpook National University
Abstract

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. 

Speaker Bio

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.