CAREER: Verifiable Specifications: Tools for Reliable Reactive Software Development

点击翻译按钮获取中文摘要

9984822Bultan, TevfikUniversity of California, Santa BarbaraCAREER: Verifiable Specifications: Tools for Reliable ReactiveSystem DevelopmentDeveloping reliable software for reactive systems is achallenging task. This project will focus on combiningand extending the results from two areas which addressthis problem: 1) specification languages and 2) automatedverification methods for reactive systems. Building on therecent results in these areas the goal of this projectis to develop verifiable specification languages. Thiswill involve research from two directions: 1) From theverification side the goal is to extend the scope oftechniques such as model checking to make them applicableto a wider set of systems. 2) From the specification sidethe goal is to restrict the specification languages as muchas possible (without reducing their ability to specifycomplex systems) in order to make their automated verificationfeasible. This project will address both theoretical issuessuch as complexity and efficiency of model checkingtechniques, and practical issues such as investigatingusability of software specification languages and automatedverification techniques in practice. Automated verificationtools developed based on the results of this project willalso be used as educational tools in both graduate andundergraduate courses on formal methods and programminglanguages.