[3-28]Tool supported real-time system verification
Date:2008-03-24
Seminar 2
Title：Tool supported real-time system verification techniques based on abstraction/deduction and model checking
Speaker：Dr. Eun-Young Kang
The United Nations Unviersity,
International Institute for Software and Technology
Time：4:00pm, March 28, 2008（Friday）
Venue：Lecture room, Lab. of Computer Science, ISCAS
Abstract：
This talk provides an efficient formal scheme for the tool-supported real-time system verification by combination of abstraction-based deductive and model checking techniques in order to handle the limitations of the applied verification techniques. This method is based on IAR (Iterative Abstract Refinement) to compute finite state abstractions. Given a transition system and a finite set of predicates, this method determines a finite abstraction, where each state of the abstract state space is a true assignment to the abstraction predicates. A theorem prover can be used to verify that the finite abstract model is a correct abstraction of a given system by checking conformance between an abstract and a concrete model by establishing/proving that a set of verification conditions are obtained during the IAR procedure. Then the safety/liveness properties are checked over the abstract model. If the verification condition holds successfully, IAR terminates its procedure. Otherwise more analysis is applied to identify if the abstract model needs to be more precise by adding extra predicates. As abstraction form, I adopt a class of predicate diagrams and define a variant of predicate diagram PDT (Predicate Diagram for Timed systems) that can be used to verify real-time and parameterized systems.
Bio：
Kang EunYoung received her PhD in informatique (computer science) from the University of Henri-Poincare, Nancy 1, France in 2007. During her PhD, she was involved in a project, which aimed to develop a theoretical and practical verification technique for the formal analysis of real-time embedded systems, and she participated in the "cotutelle" program, which could be explained in English term as a "joint PhD program" between Delft University in Holland and INRIA-LORIA in France. She has been working as a postdoc research fellow at International Institute for Software Technology of Unite Nations University in Macao since March 2008.
Kang’s speciality is formal methods, and modeling, design, verification/validation. Her research interest is combining several different formal method techniques to handle large/complex designs either automatically, or with less manual intervention. Her research as part of PhD thesis was to combine abstraction, theorem proving and model checking by the use of several tool-supports; and her other interests are rock music, playing guitar, working-out and keeping fit.