COLLOQUIUM
Department of Computer Science and Engineering
University of South Carolina

 
Automatic Abstraction for Model Checking Software Specifications with
Interrelated Numeric Constraints
Yunja Choi

Department of Computer Science and Engineering 
University of Minnesota

Date: February 7, 2003 (Friday)
Time: 3:30-4:30PM
Place: Swearingen 1A03 (Faculty Lounge)


Abstract

Model checking techniques have not been effective in important classes
of software systems characterized by large (or infinite) input domains
with interrelated linear and non-linear constraints over the input
variables.  To address this issue, I have proposed the domain
reduction abstraction technique based on data equivalence and
trajectory reduction as an alternative and complement to other
abstraction techniques.  The technique applies the abstraction to the
input domain (environment) instead of the model and is applicable to
constraint-free and deterministic constrained data transition system
with a possible extension to limited non-determinism.  The abstraction
technique is implemented as an extension of the symbolic model checker
NuSMV, which is used as a back-end verification tool in our
specification-centered software development framework.  Results on
avionics systems applications show that the approach is promising.



Yunja Choi received the B.S. and M.S. degree in Mathematics from
Yonsei University in Seoul, Korea in 1991 and 1993, and the
M.S. degree in Computer Science from the University of Minnesota in
1999, where she expect to receive the Ph.D. degree in Computer Science
in May 2003.  Ms. Choi worked as a software engineer for Samsung Data
Systems in Seoul, Korea, from 1993 to 1996 and as an intern at
Medtronics, Inc. during her Ph.D. studies. Her research interests lie
in formal methods in software engineering, including tool support for
automated verification framework and adaptation of model checking
technique to software verification.