CAREER: Verifiable Specifications: Tools for Reliable Reactive Software Development

University Of California-Santa Barbara, Santa Barbara CA

Investigators

Abstract

9984822 Bultan, Tevfik University of California, Santa Barbara CAREER: Verifiable Specifications: Tools for Reliable Reactive System Development Developing reliable software for reactive systems is a challenging task. This project will focus on combining and extending the results from two areas which address this problem: 1) specification languages and 2) automated verification methods for reactive systems. Building on the recent results in these areas the goal of this project is to develop verifiable specification languages. This will involve research from two directions: 1) From the verification side the goal is to extend the scope of techniques such as model checking to make them applicable to a wider set of systems. 2) From the specification side the goal is to restrict the specification languages as much as possible (without reducing their ability to specify complex systems) in order to make their automated verification feasible. This project will address both theoretical issues such as complexity and efficiency of model checking techniques, and practical issues such as investigating usability of software specification languages and automated verification techniques in practice. Automated verification tools developed based on the results of this project will also be used as educational tools in both graduate and undergraduate courses on formal methods and programming languages.