报告题目：A configurable V&V framework using formal behavioral patterns for OSEK/VDX operating systems
报告人：    Prof. Yunja Choi , Kyungpook National University
主持人：    张民 副教授
报告时间：2月22日  周五9:30-11:00
报告地点：理科大楼B1002

报告摘要：
Verification and Validation (V&V) of small-scale embedded software must consider the operating system. Unlike general-purpose systems, the underlying operating system is closely coupled with the application logic, generating potentially an infinite number of different control programs depending on the application configuration and application logic. Verifying this software individually is time-consuming and costly, especially when the objective is rigorous verification. To assist in rigorous V&V activities for such embedded software, the proposed work suggests a pattern-based framework that can be used to generate configurable formal OS and test models. At the core of the framework, lies a set of predefined behavioral patterns and constraint patterns that can be composed for the auto-generation of formal models for variously configured operating systems. These configurable formal models form the basis of formal validation and verification activities such as model checking safety properties, model-based test generation, and formal application simulation. We have implemented a prototype tool, specially designed for embedded control software based on the OSEK/VDX international standard, to demonstrate the benefits of the framework in task simulation, test generation, and formal verification. A series of experiments and analysis demonstrate that the suggested pattern- based framework is more efficient in test sequence generation and more effective in identifying problems compared to existing approaches.

报告人简介：
Yunja Choi is Professor of School of Computer Science and Engineering, Kyungpook National University. Her main research interests include Software Safety Analysis, Model Checking, Formal Testing, Component-based Software Engineering. Choi got her Ph.D in Computer Science at University of Minnesota, United States. Before joining KNU, she has worked as a research scientist at Fraunhofer Institute for Experimental Software Engineering, Kaiserslautern, Germany from 2003 to 2006. She also worked as a software engineer at Samsung Data Systems in Seoul from 1993 to 1996.