Abstract:
Verification and Validation of small-scale embedded software must consider its operating system as
it is closely coupled with the application logic, generating potentially an infinite number of different control programs depending on the configuration and application logic. Verifying such software individually is time-consuming and costly, especially when the objective is rigorous verification.
This talk introduces a configurable framework for safety checking such embedded software using formal behavioral patterns and model checking techniques, whose efficiency and effectiveness is demonstrated through an application of the framework on automotive control software. The notion of software safety and various safety checking techniques will also be discussed as a background of this work.

Short Bio:
Yunja Choi is an Associate Professor at the School of Computer Science and Engineering, Kyungpook National University. She received her Ph.D from University of Minnesota, USA, specialized in formal methods in software engineering. Her major work was formal specification and verification of flight control software. Afterword, she worked at the Fraunhofer Institute of Experimental Software Engineering at Kaiserslautern, Germany, as a research scientist, working on industry-oriented formal verification approaches. Since she joined Kyungpook National University in 2006, her research has been focused on light-weight formal methods and automated verification framework for embedded software.