Research at VLab
Our research in VLab focuses on automated verification techniques and their application to software. Automated verification has become a very active research area in recent years. As computer systems become more pervasive, their dependability becomes increasingly important. As a result, there is an ongoing shift in focus, both in academia and industry, from performance to dependability. The size and complexity of the software systems nowadays inevitably result in errors during both design and implementation phases. The goal of our research at VLab is to develop verification techniques that will help developers in identifying errors in software. Our work spans three areas: infinite state systems, design for verification and Web services.
Infinite State Systems: One direction of research at VLab addresses fundamental limitations of automated verification which hinder its applicability to software. One such limitation is the fact that software systems have data-types which have arbitrarily large domains and well known theoretical results show that automated verification of such systems is impossible. Our research on verification techniques for infinite state systems lead to heuristic solutions to this problem which identify the errors that are encountered in practice. The main idea is to search an infinite state space using conservative approximations which over or under-approximate the behaviors of a system and can be used both to guarantee the absence of bugs (via over-approximation) and to identify the existing bugs (via under-approximation). We developed a tool called Action Language Verifier (ALV) which implements these heuristics and we applied ALV to verification of various software systems.
Design for Verification: A promising approach in attacking the dependability problem is to find ways of constructing software that facilitate automated verification. We developed a design for verification approach by introducing a set of design patterns which support a modular verification strategy. Our approach builds on the following principles: 1) use of stateful, behavioral interfaces which isolate the behavior and enable modular verification, 2) an assume-guarantee style verification strategy which separates verification of the behavior from the verification of the conformance to the interface specifications, 3) a general model checking technique for interface verification, and 4) domain specific and specialized verification techniques for behavior verification. So far, we applied this approach to verification of concurrent and distributed systems which are especially challenging to get right. The case studies we conducted show that, using our design for verification approach, it is possible to achieve scalable software verification in these application domains.
Web Services: A new and exciting part of our research is the specification and verification of web services. Web-based software applications which enable user interaction through web browsers have been extremely successful. Web services provide a promising extension to this framework in which Web accessible software applications (services) interact with each other using the Internet. A fundamental problem in developing reliable web services is analyzing their interactions. This a challenging problem due to the distributed nature of web services. We developed a framework for modeling, specifying and analyzing interactions of web services. We addressed some fundamental problems in this area such as realizability of top-down specifications and synchronizability of asynchronously communicating web services. We developed a tool called Web Service Analysis Tool (WSAT) which verifies properties about interactions of web services and checks sufficient conditions for realizability and synchronizability.