权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

DTacs - Program Verifier Tactics : Reducing the Development Time for Program Verifiers with re-usable Verification Strategies

DTacs - 程序验证器策略：通过可重复使用的验证策略减少程序验证器的开发时间

基本信息

批准号：
EP/M018407/1
负责人：
Gudmund Grov
金额：
$ 12.77万
依托单位：
Heriot-Watt University
依托单位国家：
英国
项目类别：
Research Grant
财政年份：
2015
资助国家：
英国
起止时间：
2015 至无数据
项目状态：
已结题

来源：
https://gtr.ukri.org/projects?ref=EP%2FM018407%2F1
关键词：
DTacs Program Verifier Tactics Reducing

项目摘要

Software is woven into just about everything digital that we touch or depend upon: from communications, entertainment and consumer electronics - to railway, air-control, automotive, finance, defence, national infrastructure and health-care systems. The dependability of such software remains a major challenge. In 2002 it was estimated that software mistakes cost the US economy $59 Billion; more recent estimates have suggested an annual cost of more than $300 Billion worldwide. Dependability is therefore a key differentiator in commercial products. Whoever can cost-effectively crack the dependability challenge will have a major advantage.Conventional techniques used to ensure dependability are based around testing; and this can amount to half of the development time. Still, a fundamental problem of testing is that all combinations of inputs and conditions are not feasible. Formal approaches to software engineering use mathematics to ensure dependability. These have the advantage over conventional testing techniques that the software can be proven correct for all combinations of inputs and conditions. This is a result of using mathematics, and increases both the dependability and product quality. However, common bottlenecks of these approaches are limited availability of theorem proving skills and lack of automation provided by tools. Therefore they have often suffered from increased development time and costs when applied beyond niche markets such as safety and mission critical systems.Program verification is a formal software engineering technique where the source code is combined with a formal specification of desired behaviour. Mathematics is used to prove that the program satisfies its specification. Recently, there has been a wave of new program verifiers, where the underlying mathematics is hidden. Skills familiar to programmers are used to guide the proof in the program text rather than theorem proving skills; removing the "skill-barrier" associated with theorem provers and creating a more accessible discipline for a software engineer. Still, an open challenge is to reduce the amount of guidance that is required to complete the verification of a program - a challenge that has to be solved before program verification becomes a viable cost-effective mainstream software engineering discipline. This proposal addresses the automation challenge by enabling software engineers to encode patterns used to guide proofs directly in the program text as special programs. As a result, low-level and repetitive details, often resulting from a trial-and-error process, can be replaced by a higher-level underlying pattern. These can be re-used for similar tasks, liberating users from low-level and repetitive search tasks. As a pattern only needs to be developed once, less guidance will be needed - increasing automation and reducing development time and cost.The language used to write programs and guide proofs within a program verifier will be extended to enable software engineers to also encode their verification patterns. The extension should be as minimal as possible, to avoid reducing accessibility with new skill-barriers that have to be overcome. The development of such language requires a new understanding of how users guide program verifiers. We will focus on the Dafny program verifier; re-engineering the development process used in a selection of the available Dafny case studies; and developing and verifying new programs from scratch. In both cases, each step of the verification process will be captured, creating a catalogue of verification patterns. Based on this catalogue the language used within Dafny will be extended with a new special method called a `DTac' (Dafny Tactic). A verification pattern will be encoded as a DTac. Automation will be achieved by developing a new tool called Tacny that can read DTacs and apply them to other Dafny programs to automate the verification.

软件几乎融入了我们接触或依赖的所有数字化领域：从通信、娱乐和消费电子产品到铁路、空气控制、汽车、金融、国防、国家基础设施和医疗保健系统。这种软件的可靠性仍然是一个重大挑战。2002年，据估计软件错误给美国经济造成了590亿美元的损失;最近的估计表明，全球每年造成的损失超过3000亿美元。因此，可靠性是商业产品的关键区别。谁能经济有效地解决可靠性挑战，谁就将拥有巨大的优势。用于确保可靠性的传统技术是基于测试的;这可能占开发时间的一半。然而，测试的一个基本问题是，输入和条件的所有组合都是不可行的。软件工程的形式化方法使用数学来确保可靠性。与传统的测试技术相比，这些技术的优势在于可以证明软件对于所有输入和条件的组合都是正确的。这是使用数学的结果，并提高了可靠性和产品质量。然而，这些方法的共同瓶颈是有限的可用性定理证明技能和缺乏自动化提供的工具。因此，当应用于安全和使命关键系统等利基市场之外时，它们往往会增加开发时间和成本。程序验证是一种正式的软件工程技术，其中源代码与所需行为的正式规范相结合。数学是用来证明程序满足其规格。最近，出现了一波新的程序验证器，其中隐藏了底层的数学。程序员熟悉的技能被用来指导程序文本中的证明，而不是定理证明技能;消除了与定理证明器相关的“技能障碍”，为软件工程师创建了一个更容易理解的学科。尽管如此，一个开放的挑战是减少完成程序验证所需的指导量-在程序验证成为可行的成本效益主流软件工程学科之前必须解决的挑战。该提案通过使软件工程师能够将用于指导证明的模式直接编码在程序文本中作为特殊程序来解决自动化挑战。因此，通常由试错过程产生的低级别和重复的细节可以被更高级别的基础模式所取代。这些可以重复用于类似的任务，将用户从低级和重复的搜索任务中解放出来。由于一个模式只需要开发一次，因此需要的指导更少--提高了自动化程度，减少了开发时间和成本。用于编写程序和在程序验证器中指导证明的语言将得到扩展，使软件工程师能够对他们的验证模式进行编码。这种扩展应尽可能小，以避免因必须克服的新技能障碍而降低可获得性。这种语言的发展需要对用户如何引导程序验证器有一个新的理解。我们将专注于Dafny程序验证器;重新设计在选择可用的Dafny案例研究中使用的开发过程;从头开始开发和验证新程序。在这两种情况下，核查过程的每一步都将被记录下来，从而创建核查模式目录。在此目录的基础上，Dafny中使用的语言将被扩展为一种新的特殊方法，称为“DTac”（Dafny战术）。验证模式将被编码为DTac。自动化将通过开发一种名为Tacny的新工具来实现，该工具可以读取DTac并将其应用于其他Dafny程序以自动化验证。