12月22日：谢飞 - 学术报告 - 华东师范大学计算机科学与银河集团9873.cσm
（附带研究室招生咨询）
报告题目：Automata-Theoretic Approach to Hardware/Software Co-verification
报告人：谢飞 教授（Department of Computer Science，Portland State University，American）
主持人：蔡海滨
报告时间：2016年12月22日（周三） 14:00-15:00
报告地点：中北校区数学馆201
报告人简介：
Fei Xie is a professor in the Department of Computer Science, Portland State University. His interests are primarily in the areas of software engineering, embedded systems, and formal methods, particularly development of formal method based techniques and tools for building safe, secure, and reliable software and embedded systems.
报告摘要：
In this talk, we present an automata-theoretic approach to hardware/software (HW/SW) co-verification. We have designed a co-specification framework to formally specify HW/SW interface protocols; we have synthesized a hybrid Buchi Automaton Pushdown System, namely Buchi Pushdown System (BPDS), as the unifying formal model for HW/SW interfaces; and we have developed a co-verification tool, CoVer, that not only implements our model checking algorithms but also realizes our reduction algorithms for BPDS. Application of our approach to the Windows device/driver framework has resulted in the detection of fifteen specification issues. Furthermore, utilizing CoVer, we have discovered twelve real bugs in five production drivers.
12月23日：谢飞 - 学术报告 - 华东师范大学计算机科学与银河集团9873.cσm
（附带研究室招生咨询）
报告题目：Automatic Fault Injection for Driver Robustness Testing
报告人：谢飞 教授（Department of Computer Science，Portland State University，American）
主持人：蔡海滨
报告时间：2016年12月23日（周四) 14:00-15:00
报告地点：中北校区数学馆201
报告人简介：
Fei Xie is a professor in the Department of Computer Science, Portland State University. His interests are primarily in the areas of software engineering, embedded systems, and formal methods, particularly development of formal method based techniques and tools for building safe, secure, and reliable software and embedded systems.
报告摘要：
Robustness testing is a crucial stage in the device driver development cycle. To accelerate driver robustness testing,effective fault scenarios need to be generated and injected without requiring much time and human effort. In this talk,we present a practical approach to automatic runtime generation and injection of fault scenarios for driver robustness testing. We identify target functions that can fail from runtime execution traces, generate effective fault scenarios on these target functions using a bounded trace-based iterative strategy, and inject the generated fault scenarios at runtime to test driver robustness using a permutation-based injection mechanism. We have evaluated our approach on 12 Linux device drivers and found 28 severe bugs. All these bugs have been further validated via manual fault injection.The results demonstrate that our approach is useful and efficient in generating fault scenarios for driver robustness testing with little manual effort.
