本文是嵌入式软件Series:使用ADA合同执行编码
Safety and reliability have moved to the top of the list of critical criteria in software development. There are many ways to achieve improved safety and reliability, and one of the best is to employ formal methods.
我与之交谈Adacore的Spark产品经理Yannick Moy，介绍了如何正式验证软件可以帮助开发零缺陷软件的开发。
黄：What is formal program verification?
Moy:计划验证是一个适当的信心证明，即一个程序是正确的（即它符合其指定要求）。通常，这是通过测试和评论的结合来实现的，尽管也越来越多地使用了工具支持的分析。正式的程序验证依赖于通过工具来支持其结论对程序的数学分析。
黄：How is it different from static analysis?
Moy:正式的程序验证是一种特殊的静态分析，其目的是为所分析的程序提供基于数学的保证。例如，可以使用正式的程序验证来显示程序中完全没有运行时错误（例如零和缓冲区溢出），或者将实现的符合性符合其预期规范。
This requires an analysis that is "sound," i.e., the verification tool can never say that there is no error when the program in fact has an error (of the kind targeted by the analysis). This is quite different from the typical use of static analysis for finding bugs, which usually takes shortcuts with program semantics in order to run faster and find only sure errors.
黄：Formal program verification requires writing function contracts such as pre- and post-conditions, right? Do you expect programmers to be able to write these contracts?
Moy:Indeed, function contracts are at the foundation of formal program verification. There are two reasons for that. First, to verify that the implementation respects an intended specification, we need a way to precisely express this specification. Function contracts meet this requirement. Second, to apply the powerful verification techniques that can prove non-trivial properties of software, we need to focus the verification on small parts of the code. Function contracts allow the programmer to focus the verification on individual functions, one at a time.
You can write multiple contracts on a function, depending on your verification objective. If your objective is simply to verify correct data accesses, initialization, and dependencies, simple contracts are needed, such as the following:
Procedure Stabilize ( Mode : in Mode_T; Success : out Boolean) With Global => (Input => (Accel, Giro), In_Out => Rotors ); 全球合同指出，全局变量加速和GIRO是该过程稳定的输入，并且全局变量转子既是相同过程的输入和输出。我在这里使用Spark语法，但是其他语言具有类似的功能。
如果您的目标是验证缺乏运行时错误，特定属性或功能正确性，则需要更复杂的合同，例如以下内容：
Procedure Stabilize ( Mode : in Mode_T; Success : out Boolean) With Pre => Mode /= Off, Post => (if Success then Delta_Change (RotorsâOld, Rotors)); 这pre-condition introduced by Pre states that procedure Stabilize should only be called when Mode is not Off. The post-condition introduced by Post states that on exit from procedure Stabilize, if Success is true, then a given relation Delta_Change relates the input and output values of the global variable Rotors. I'm again using SPARK syntax here, but other languages have similar capabilities.
As you can see from these two examples, it is well within the capabilities of programmers to write such contracts. The first one is simply an extension of the function signature, and the second one is an extension of assertions, both of which are familiar programming language features.
黄：即使程序员可以签订合同，也有与此额外开发活动相关的成本。您如何弥补总体上从这种方法中获得的这些费用？
Moy:这re are two possible reasons for using formal program verification, one related to quality and the other related to costs. And in most cases, people do it for both. The quality argument is that formal program verification can deliver a very small defect density in your software, at a reasonable cost. The cost argument is that it can deliver the same quality as extensive testing and reviews, at a smaller cost.
正式的计划验证可以以两种不同的方式降低成本。首先，正式计划验证提供的保证意味着您可以减少甚至完全消除其他活动，例如一些测试和评论。例如，如果您使用正式程序验证证明没有运行时错误和类似属性，则无需编写测试或执行针对鲁棒性的评论。
Second, the quality obtained by formal program verification means that you detect errors earlier in the development cycle, when they are cheaper to correct. For example, you get a lower pre-test defect density with formal program verification than with traditional testing-based methods, and this measure is strongly correlated with overall project cost.
黄：今天哪些公司使用这些技术？
Moy:这些技术主要用于域中，在这些域中，软件错误可能非常昂贵，例如航空电子，空中交通管制，核反应堆，安全和防御。例如，洛克希德·马丁（Lockheed Martin）在1997年使用Spark用于C130J军用飞机的控制软件，此后，英国皇家空军和BAE系统加强了使用Spark在维护过程中证明C130J控制软件的关键属性。
另外一个例子,空客verific使用警告ation system for C in 2002 to prove compliance with low-level requirements on the Airbus A380 civilian airplane, instead of unit testing. Their use of formal program verification was included as an example in the Formal Methods Supplement of the DO-178C avionics certification standard.
In the security world,Rockwell Collinsadopted SPARK for its Turnstile/SecureOne cross-domain switch, and secunet uses mostly SPARK in its multilevel workstation and Muen separation kernel. In both cases, SPARK is used to prove the absence of run-time errors (as these could lead to security attacks) and also critical security properties (such as the proper use of keys and encryption).
除了传统的高保证软件领域外，汽车，机器人和医疗设备等新领域还将正式的程序验证视为以合理的成本获取高质量软件的一种方式。
黄：How about tools that provide formal program verification?
Moy:两种工具集为C和ADA的工业用户提供了正式的计划验证。C程序的Frama-C工具集由CEA, and TrustInSoft commercializes a variant based on the same technology. The SPARK toolset for Ada programs is co-developed and commercialized byAltran UKand AdaCore. Other academic toolsets exist around the Eiffel, Java, and C# languages.
黄：So, there are tools for different programming languages in this list. Are they equivalent, or are there real differences between them?
Moy:All of these tools share some algorithms to create mathematical formulas from programs, and they rely on some of the same underlying automatic provers to prove the formulas. Yet, they are very different in terms of interaction and automation, which are two critical aspects of the tools’ usability. For example, an important feature for interaction is the ability of the toolset to generate counterexamples for unproved properties, and an important feature for automation is the ability to generate missing contracts for internal functions.
Another difference is the support in the programming language for specifications. For example, the fact that SPARK is based on Ada means that users benefit in SPARK from all of the features for precise type specifications, compared to users of C. This means that there is less work for users of SPARK to specify their programs in function contracts, since many simple specifications like ranges of values are already embodied in the syntax for types.
Read more from the嵌入式软件Series:使用ADA合同执行编码
Yannick Moy is the SPARK product manager at AdaCore. He has led the development of the SPARK language and tools since 2010, and he supervised the major technology revision resulting in SPARK 2014. Yannick has presented SPARK in numerous articles and conferences, as well as online (in particularwww.spark-2014.org). Previously, he worked on software source-code analyzers CodePeer, Frama-C and PolySpace Verifier C++.
References:
A comparison of SPARK with MISRA C and Frama-C.
这free SPARK Courseon AdaCore U e-learning website.
这onlineSPARK User's Guide.
