2010年上半年5月份系统分析师上午试题答案（分析与解答）之三
（20）
参考答案：B
（21）
参考答案：B
（22）
参考答案：D
（23）
参考答案：D
（24）
试题分析：
形式化方法可以分为形式化描述和建立在形式化描述基础之上的形式化开发。形式化的描述就是用形式化的语言(具有严格的语法语义定义的语言)做描述。形式化的软件开发，就是用形式化的语言来描述软件需求和特征，并且通过推理验证来保证最终的软件产品是否满足这些需求和具备这些特征。这样的验证当然得建立在严格的语法语义的基础之上的。在实际应用中，这是不容易做到的。形式化方法研究的目的就是希望能够提供更好的理论、方法和工具，扩大形式化方法的应用范围和使用价值。
形式化方法的意义在于它能帮助发现其它方法不容易发现的系统描述的不一致，不明确或不完整，有助于增加软件开发人员对系统的理解，因此形式化方法是提高软件系统，特别是safety-critical系统的安全性与可靠性的重要手段．最早的形式化方法是逻辑与逻辑推理，它的目标是使推理机械化．从广义上讲，这一目标受到许多挫折．比如说逻辑系统的不完备性(incompleteness)、逻辑系统的不可判定性(undecidability)、自动推理的难处理性(intractability)．但是在一些实际应用上，逻辑方法和自动推理还是起着非常大的作用．
形式化方法原则上就是用数学与逻辑的方法描述和验证软件。从描述上讲，一方面是系统或程序的描述，另一方面是性质的描述。这些可以用一种或多种语言来描述。这些语言包括命题逻辑，一阶逻辑，高阶逻辑，代数，状态机，并发状态机，自动机，计算树逻辑，线性时序逻辑，进程代数， π-演算， μ-演算，特殊的程序语言，以及程序语言的子集等。从验证来讲，主要有两类方法，一类是以逻辑推理为基础，另一类则以穷尽搜索为基础。逻辑推理有 natural deduction, sequent calculus, resolution 以及Hoare-logic 等方法。穷尽搜索方法统称为模型检测。这类方法与系统或程序以及系统性质的表示有很大的关系，比如说符号模型检测，其基本原理是用命题逻辑公式表示状态转换关系，用不动点算法计算状态的可达性以及这些状态是否满足某些性质。
from http://blog.sina.com.cn/u/4b700c4c010006rj
形式化方法可以分为形式化描述和建立在形式化描述基础之上的形式化开发。形式化的描述就是用形式化的语言(具有严格的语法语义定义的语言)做描述。形式化的软件开发，就是用形式化的语言来描述软件需求和特征，并且通过推理验证来保证最终的软件产品是否满足这些需求和具备这些特征。这样的验证当然得建立在严格的语法语义的基础之上的。在实际应用中，这是不容易做到的。形式化方法研究的目的就是希望能够提供更好的理论、方法和工具，扩大形式化方法的应用范围和使用价值。
形式化方法的意义在于它能帮助发现其它方法不容易发现的系统描述的不一致，不明确或不完整，有助于增加软件开发人员对系统的理解，因此形式化方法是提高软件系统，特别是safety-critical系统的安全性与可靠性的重要手段．最早的形式化方法是逻辑与逻辑推理，它的目标是使推理机械化．从广义上讲，这一目标受到许多挫折．比如说逻辑系统的不完备性(incompleteness)、逻辑系统的不可判定性(undecidability)、自动推理的难处理性(intractability)．但是在一些实际应用上，逻辑方法和自动推理还是起着非常大的作用．
早期形式化方法在软件验证的应用是串行程序的验证，后来随着软件研究和应用的发展，逐渐多样化．比如用逻辑和代数方法描述软件，用逻辑推理来验证软件（即描述软件的这些逻辑公式）的性质．又比如用进程代数描述并发软件，用模型检测方法验证这些软件的性质．近年来，由于认识到形式化方法重视的是严谨性，而这些方法与常用的软件方法差别很大，逐渐有许多结合图形化软件方法、面向对象方法和形式化方法的工作．以上所述几个方面（即程序验证，定理证明，模型检测，图形化方法和形式化方法相结合）的内容虽然不尽一样，但密切相关．定理证明与模型检测互为补充，各有所长．对于复杂的软件系统的验证，最好是能够结合多种方法的使用．这些方法对高可信软件开发方法的探索和应用都极为重要。
形式化方法与软件可靠性：
随着软件的广泛应用，特别是软件在尖端领域的应用，软件可靠性成为一个非常重要的问题。软件的可靠取决于两个方面，一个是软件产品的测试与验证，另一个是软件开发的方法与过程。对简单的软件开发，我们的经验是先有对软件的要求，然后对软件进行设计，然后是编写程序，最后是对程序进行测试，如果测试出错则对软件进行修改，然后再测试，直至对程序满意为止。对复杂的软件系统，总的过程基本还是这样，只是各个阶段也相应复杂一些。比如说，软件的要求可能需要从多方面进行描述，软件的设计需要从多方面考虑，程序的编写需要分成多个单元，对于测试来讲也就有单元测试和总体测试的分别。有些软件的要求难以一开始就完全清楚，而更改软件要求会对软件设计以及其他大量已经完成或正在进行的工作产生很大的影响，因此有些软件开发方法和过程就需要提供反复修改软件要求的便利。
形式化方法在软件开发中能够起到的作用是多方面的。首先是对软件要求的描述。软件要求的描述是软件开发的基础。比如说一般非形式化的描述很可能导致描述的不明确和不一致。如果描述的不明确和不一致导致设计，编程的错误，将来的修改所要付出的代价就非常大了。如果导致的错误没有被发现，则影响程序的可靠和使用。形式化方法则要求描述的明确性，而描述的不一致性也就相对易于发现。其次是对软件设计的描述。软件设计的描述和软件要求的描述一样重要。形式化方法的优点对于软件要求的描述同样适用于软件设计的描述。另外由于有了软件要求的形式化描述，我们可以检验软件的设计是否满足软件的要求。对于编程来讲，我们可以考虑自动代码生成。对于一些简单的系统，形式化的描述有可能直接转换成可执行程序，这就简化了软件开发过程，节约了资源和减少了出错的可能性。另外，形式化方法可以用于程序的验证，以保证程序的正确性。对于测试来讲，形式化方法可用于测试用例的自动生成，这可以节约许多时间和在一定程度上保证测试用例的覆盖率。
传统的软件工程建模、形式化方法、程序验证(正确性证明)、以及统计SQA的集成使用已经组合成一种可以导致极高质量软件的技术。
净室软件工程(Cleanroom software engineering)是一种在软件开发过程中强调在软件中建立正确性的需要的方法。代替传统的分析、设计、编码、测试和调试周期，净室方法建议一种不同的观点〔LIN94〕：
在净室软件工程后面的哲学是：通过在第一次正确地书写代码增量并在测试前验证它们的正确性来避免对成本很高的错误消除过程的依赖。它的过程模型是在代码增量积聚到系统的过程的同时进行代码增量的统计质量验证。
净室方法在很多方面将软件工程提升到另一个层次。象第24章中讨论的形式化方法技术一样，净室过程强调在规约和设计上的严格性，以及使用基于数学的正确性证明来对结果设计模型的每个元素进行形式化验证。作为对形式化方法中采用的方法的扩展，净室方法还强调统计质量控制技术，包括基于客户对软件的预期的使用的测试。
当现实世界中软件失败时，则充满了立即的和长期的危险。这些危险可能和人的安全、经济损失、或业务和社会基础设施的有效运作相关。净室软件工程是一个过程模型，它在可能产生严重的危险前消除错误。
参见《系统分析师考试全程指导》（根据2009版大纲编写）P269页
参考答案：A
（25）
参考答案：D
（26）
参考答案：C
（27）
参考答案：A
（28）
参考答案：D
（29）
参考答案：B
