形式化方法基础
前言
优秀架构师在一些设计决策的过程中或多或少都会凭借自身的直觉或者经验，细细品味这句话：归根结底还是靠经验积累(直觉是基于大量前期经验从而快速找到解决方案的能力)。现实中无论多么完备的方法论在“by experience”面前都得靠边站。然而在某些关键时刻，由于时间、状态的变化，经验势必也可能不那么靠谱，经验主义错误也就此诞生。如何让自己做出的架构或者设计更加科学，就是形式化方法所能带给我们的，说服别人更要说服自己。让我们开始一趟从“艺术”到“科学”的形式化之旅吧^_^
背景
针对60年代出现“软件危机”，业界提出两种解决方法：
- 采用工程方法来组织、管理软件的开发过程；
- 深入探讨程序和程序开发过程的规律，建立严密的理论，以期能用来指导软件开发实践。
前者导致“软件工程”的出现和发展，后者则推动了形式化方法的深入研究。
可靠性
软件的可靠性取决于两方面：
- 软件开发的方法与过程
- 软件产品的测试与验证
第一点也就是前面所提到的“软件工程”。而大神E.W.Dijkstra曾提出一个著名论断：
程序测试只能证明错误的存在，但不能证明错误不存在。
使得采用形式化方法对系统进行验证和分析，成为构造安全可信软件的一个重要途径。
形式化方法能在系统开发的早期发现系统中的不一致、歧义、不完全和错误，已被证明是一种行之有效的减少设计错误、提高软件系统可信性的重要途径。
定义
维基百科：
形式化方法是基于数学的特种技术，适合于软件和硬件系统的描述、开发和验证。将形式化方法用于软件和硬件设计，是期望能够像其它工程学科一样，使用适当的数学分析以提高设计的可靠性和鲁棒性。但是，由于采用形式化方法的成本高意味着它们通常只用于开发注重安全性的高度整合的系统。
从这里可以得到以下信息：
- 形式化方法基于数学。这代表了形式化方法的最大特点：科学性；
- 适用于软硬件系统。是的，从地铁到算法都是形式化方法的用武之地；
- 成本高。从前想在形式化方法有所建树至少得时个PHD才行，门槛高的很，这也是为什么它比起“软件工程”和“软件测试”来可谓闻所未闻。
给个更精炼的定义：
形式化方法是一种有严格数学基础的软件和系统开发方法，支持计算机系统及软件的规约、设计、验证与演化等活动。
与传统方法对比
- 传统的软件设计方法：
– 基于自然语言思考、设计和描述 – 语义含糊，可能有歧义，依赖于使用者的理解 – 无法进行严格的检查，只能通过人的交流活动进行分析
- 半形式化的方法（例如基于 UML 等）
– 有较清晰定义的形式和部分的语义定义 – 一些描述的语义较清晰，可能开发工具进行检查和分析
- 形式化方法：
– 基于严格定义的数学概念和语言 – 语义清晰，无歧义。可以开发自动化工具进行检查和分析
目前情况：软件的开发正在从朴素的、非形式的设计方法，向着更加严格、更加形式化的方向转变（特别是在大型/复杂/关键系统方面）
组成
其基本组成包括：
- 系统建模。通过构造系统S的模型M来描述系统及其行为模式;
- 形式规约。通过定义系统S必须满足的一些属性ψ，如：安全性、活性等来描述系统约束;
-
形式验证。证明描述系统S行为的模型M确实满足系统形式规约ψ（即验证M =ψ）。
系统建模
系统从其运行方式上分为：串行系统和并发系统两大类。
串行系统：从初始态到终止态的系统。 其特征为：顺序性、封闭性、可再现性。
并发系统：系统内发生的两个事件间没有因果关系或可以按任意次序发生，则称这两个事件是并发的，存在并发事件的系统称为并发系统。 其特征为：不确定性、并发性。
在具体建立并发模型时，需捕获到系统与正确性有关的行为特征，对被检测系统进行简化和缩小，验证不能过于复杂，模型抽象时应去掉一些不影响正确性的属性。
由于串行系统的确定性，所以对一般的串行系统使用形式化方法的意义不大，因此形式化方法更适用于不确定、更为复杂的并发系统。
形式规约
形式规约用来确定“做什么”，而非“怎么做”。 类似需求规范以一种以清晰、简明、一致且无歧义的方式，刻画客户或用户所需系统中所有重要方面的一组陈述 规约是客户或用户与软件开发人员之间的接口，可看作一种契约合同； 规约也是设计和编写程序的出发点和验证程序是否正确的依据。
形式验证
形式验证分为两类：
- 以逻辑推理为基础的演绎验证。 用逻辑公式描述系统性质，通过一些公理或推理规则来证明系统具有某些性质。其优点是既可验证有穷状态系统，也可使用归纳法来处理无限状态问题。 缺点是不能做到完全自动化验证。
- 以穷尽搜索为基础的模型检测。 通过搜索待验证系统模型的有穷状态空间来检验该系统的行为是否具备预期属性的一种自动验证技术。
一些术语
Specification（规范）：采用具有严格定义的形式和语义的记法形式，描 述软件设计（和实现）
Reasoning and Analysis（推理和分析）：对形式化规范进行分析和推理， 确定它们的各种静态和动态性质 – 规范是否具有一致性和完整性，其中有没有矛盾，有没有遗漏？ – 运行中不会出现某些不能容忍的状态（死锁、活锁等） – 找出其中的错误和缺陷等
Refinement（精化）：从抽象的高层描述出发，严格保语义地推导出更接 近实现的包含更多细节的规范，最终得到正确实现了高层规范的可运行程 序（逐步求精技术的严格化，另一些软件技术也可以看作精化）
结束语
本文主要介绍形式化方法的基本概念，后续会对TLA+方法和工具进行介绍，尽请期待~
参考文献
《形式化方法导论》
- 版权声明： 本博客所有文章除特别声明外，均采用 CC BY-NC-SA 3.0 许可协议。转载请注明出处！
