Coverage at the Formal Specification Level
Title：Coverage at the Formal Specification Level
Lecturer：Professor Rolf Drechsler
Time：14：00 – 16:00,August 13(Thursday), 2015
Location: Room 201, Mathematics Building
Formal verification is a powerful and effective method to ensure correctness of electronic systems. In order to check whether enough properties have been written coverage metrics have been proposed along with methods to automatically increase the coverage by determining new properties for missed scenarios. In the invited talk we present how such coverage methods can be leveraged to higher levels in the design flow of electronic systems. We first review existing coverage metrics and demonstrate state-of-the art formal verification techniques for correctness checking at the Formal Specification Level (FSL). Based on those we describe how coverage techniques can help to automatically derive missed scenarios at the FSL, where structure and behavior are given in terms of UML class and sequence diagrams, respectively.
Rolf Drechsler received the Diploma and Dr. Phil. Nat. degrees in computer science from J.W. Goethe University Frankfurt am Main, Frankfurt am Main, Germany, in 1992 and 1995, respectively. He was with the Institute of Computer Science, Albert-Ludwigs University, Freiburg im Breisgau, Germany, from 1995 to 2000, and with the Corporate Technology Department, Siemens AG, Munich, Germany, from 2000 to 2001. Since October 2001, he has been with the University of Bremen, Bremen, Germany, where he is currently a Full Professor and the Head of the Group for Computer Architecture, Institute of Computer Science. In 2011, he additionally became the Director of the Cyber-Physical Systems group at the German Research Center for Artificial Intelligence (DFKI) in Bremen. His current research interests include the development and design of data structures and algorithms with a focus on circuit and system design. Rolf Drechsler was a member of Program Committees of numerous conferences including e.g., DAC, ICCAD, DATE, ASP-DAC, FDL, MEMOCODE, FMCAD, Symposiums Chair ISMVL 1999 and 2014, and the Topic Chair for “Formal Verification” DATE 2004, DATE 2005, DAC 2010, as well as DAC 2011. He is a co-founder of the Graduate School of Embedded Systems and he is the coordinator of the Graduate School “System Design” funded within the German Excellence Initiative. He received best paper awards at the Haifa Verification Conference (HVC) in 2006, the Forum on specification & Design Languages (FDL) in 2007 and 2010, the IEEE Symposium on Design and Diagnostics of Electronic Circuits and Systems (DDECS) in 2010 and the IEEE/ACM International Conference on Computer-Aided Design (ICCAD) in 2013. Rolf Drechsler is a Fellow of the IEEE.