CAREER: Verifiable Specifications: Tools for Reliable Reactive Software Development

9984822Bultan， tevfik加州大学圣巴巴拉分校职业：可验证的规范：可靠的反应系统开发工具为反应系统开发可靠的软件是一项具有挑战性的任务。这个项目将集中于组合和扩展两个领域的结果，这两个领域解决了这个问题：1)规范语言和2)响应式系统的自动验证方法。在这些领域的最新成果的基础上，这个项目的目标是开发可验证的规范语言。这将涉及两个方向的研究：1)从验证方面来看，目标是扩展技术的范围，如模型检查，使其适用于更广泛的系统。2)从规范方面来看，目标是尽可能地限制规范语言（不降低它们指定复杂系统的能力），以便使它们的自动化验证可行。该项目将解决理论问题，如模型检查技术的复杂性和效率，以及实际问题，如调查软件规范语言的可用性和实践中的自动验证技术。基于这个项目的结果开发的自动化验证工具也将被用作正式方法和编程语言的研究生和本科生课程的教育工具。

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.