Modularity is the key to designing dependable software systems and achieving scalability in automated verification. The question is: How can modularity at the design level be better integrated with the verification techniques that depend on it? I believe the answer is effective use of behavioral interfaces. Using behavioral interfaces specified at design time, one can isolate the behavior of interest at verification time, enabling modular verification. We applied this approach to verification of synchronization behavior in concurrent programs and to verification of interaction behavior among Web services, using behavioral interfaces specified as state machines. . More recently we developed an interface specification language based on grammars to support modular verification. An interface grammar specifies the allowable interactions between two components by identifying the acceptable method call/return sequences between them. Given two components and an interface grammar specifying their interactions, our interface compiler generates a stub for either component, enabling verification of the other component in isolation.
Tevfik Bultan is an Associate Professor and the Vice Chair of the Department of Computer Science at the University of California, Santa Barbara. His current research interests are: service oriented computing, concurrency, model checking, static analysis, and software engineering. Tevfik Bultan received his B.S. in electrical and electronics engineering in 1989 from the Middle East Technical University, and his M.S. in computer engineering and information science in 1992 from the Bilkent University, both in Ankara, Turkey. He received his Ph.D. in computer science in 1998 from the University of Maryland, College Park. He joined the Department of Computer Science at the University of California, Santa Barbara in 1998. Tevfik Bultan received a NATO Science Fellowship from the Scientific and Technical Research Council of Turkey (TUBITAK) in 1993, a Regents' Junior Faculty Fellowship from the University of California, Santa Barbara in 1999, and a Faculty Early Career Development (CAREER) Award from the National Science Foundation in 2000.