The Wayback Machine - https://web.archive.org/web/20221028230818/https://baike.sogou.com/kexue/d10145.htm

形式规范

编辑

在计算机科学中，形式规范是基于数学的技术，其目的是帮助实现系统和软件。它是一个分析行为，并通过严格有效的推理工具验证感兴趣的关键属性来帮助完成设计的系统。[1][2]这些规范由于有特定的语法而显得是非常正式的，它的语义属于一个能够被用来推断有用信息的领域。[3]

1 动机编辑

在过去的十年中，计算机系统变得越来越强大，因此对社会的影响也越来越大。因而需要更好的技术来帮助设计和实现一些可靠的软件。已建立的工程学科使用数学分析作为创建和验证产品设计的基础。正如曾经预测的那样，形式规范是实现软件工程可靠性的一种方式。而测试等其他方法更常用于提高代码的质量。[1]

2 使用编辑

有了这样一个规范，就可以使用正式的验证技术来证明系统设计相对于其规范的正确性。这使得不正确的系统设计可以在任何重大投资投入实际实施之前进行修改。另一种方法是使用可能正确的细化步骤将规范转换成设计，最终通过构造转换成正确的实现。

需要注意的是，形式规范不是一个实现，而是可以用来开发一个实现。形式规范描述了系统应该做什么，而不是系统应该如何做。

一个好的规范必须具有以下一些属性:充分的、内部一致的、明确的、完整的、满意的、最小的[3]

一个好的规范应该有:[3]

  • 可施工性、可管理性和可进化性
  • 可用性
  • 可移植性
  • 强大而高效的分析

人们对形式规范感兴趣的主要原因之一是，它们将提供软件实现的执行能力。[2]这些证明可以用来验证一个规范，验证设计的正确性，或者证明一个程序满足一个规范。[2]

3 限制编辑

一个设计(或实现)本身永远不能被声明为“正确的”。它只能是“相对于给定的规范是正确的”。形式规范是否正确描述了要解决的问题是一个独立的问题。这也是一个很难解决的问题，因为它最终涉及到的是构建非正式的具体问题域的抽象形式来表示的问题，并且这种抽象步骤不适合于形式证明。然而，通过证明规范所预期展示的相关特性的“挑战”定理来验证规范是可能的。如果正确，这些定理强化了说明符对规范及其与底层问题域之间关系的理解。如果没有，规范可能需要修改，以更好地反映那些涉及到生产(和实现)规范的领域理解。

软件开发的形式化方法在工业中没有被广泛使用。大多数公司认为在软件开发过程中应用它们不划算。[4]这可能有多种原因，其中一些原因是:

  • 时间
    • 初始启动成本高，可衡量回报低
  • 灵活性
    • 许多软件公司使用注重灵活性的敏捷方法。预先完成整个系统的形式规范通常被认为是灵活的对立面。然而，存在一些关于在“敏捷”开发中使用的形式规范的好处的研究[5]
  • 复杂性
    • 需要高水平的数学专业知识和分析技能来有效地理解和应用它们[5]
    • 解决这一问题的办法是开发工具和模型，允许除了隐藏的底层数学之外的这些技术得以实现[2][5]
  • 有限范围[3]
    • 没有捕获项目[3]中所有利益相关者感兴趣的属性[3]
    • 在指定用户界面和用户交互方面做得不好[4]
  • 低性价比
    • 这并不完全正确，因为仅限制在已证明具有成本效益的关键系统的核心部分中使用[4]

其他限制:[3]

  • 隔离
  • 低级本体
  • 缺乏指导
  • 关注点分离不佳
  • 工具反馈不佳

4 范例编辑

形式规范技术已经存在于不同领域和不同规模相当长一段时间了。[6]正式规范的实现会有所不同，这取决于他们试图建模的系统类型、如何应用以及在软件生命周期的哪个阶段引入了它们。[2]这些类型的模型可以分为以下规范范例:

  • 基于历史的规范
    • 基于系统历史的行为
    • 断言会随着时间的推移而被解释
  • 基于状态的规范[3]
    • 基于系统状态的行为
    • 一系列连续的步骤(如金融交易)
    • 诸如Z、VDM或B这样的语言依赖于这种范式[3]
  • 基于过程的规范[3]
    • 基于系统状态到状态转换行为
    • 最好与反应系统一起使用
    • Statechart、PROMELA、STeP-SPL、RSML或SCR等语言都依赖于这种范式[3]
  • 功能规范[3]
    • 将系统指定为数学函数的结构
    • OBJ、ASL美国手语、PLUSS语、Larch落叶松语、HOL语或PVS语都依赖这种范式[3]
  • 操作规范[3]
    • 早期的语言，如佩斯利（Paisley）、GIST、Petri网或过程代数，都依赖于这个范例[3]

除了上述范例之外，还有一些方法可以应用某些启发式来帮助改进这些规范的创建。这里引用的文章很完善地讨论了设计规范时使用的启发式方法。[6]并采用分治的方法来实现这一目标。

5 软件工具编辑

Z符号是一种领先的形式规范语言的例子。其他包括维也纳开发方法的规范语言（VDM-SL）和B方法的抽象机器符号（AMN）。在网络服务领域，形式规范通常用于描述[7]网络服务的服务质量等非功能属性。[7]

一些工具是:[4]

  • 代数的
    1. Larch
    2. OBJ
    3. Lotos
  • 基于模型
    1. Z
    2. B
    3. VDM
    4. CSP
    5. Petri网
    6. TLA+

参考文献

  • [1]

    ^Hierons, R. M.; Krause, P.; Lüttgen, G.; Simons, A. J. H.; Vilkomir, S.; Woodward, M. R.; Zedan, H.; Bogdanov, K.; Bowen, J. P.; Cleaveland, R.; Derrick, J.; Dick, J.; Gheorghe, M.; Harman, M.; Kapoor, K. (2009). "Using formal specifications to support testing". ACM Computing Surveys. 41 (2): 1. CiteSeerX 10.1.1.144.3320. doi:10.1145/1459352.1459354..

  • [2]

    ^Gaudel, M. -C. (1994). "Formal specification techniques". Proceedings of 16th International Conference on Software Engineering. pp. 223–227. doi:10.1109/ICSE.1994.296781. ISBN 978-0-8186-5855-6..

  • [3]

    ^Lamsweerde, A. V. (2000). "Formal specification". Proceedings of the conference on the future of Software engineering - ICSE '00. pp. 147–159. doi:10.1145/336512.336546. ISBN 978-1581132533..

  • [4]

    ^Sommerville, Ian (2009). "Formal Specification" (PDF). Software Engineering. Retrieved 3 February 2013..

  • [5]

    ^Nummenmaa, Timo; Tiensuu, Aleksi; Berki, Eleni; Mikkonen, Tommi; Kuittinen, Jussi; Kultima, Annakaisa (4 August 2011). "Supporting agile development by facilitating natural user interaction with executable formal specifications". ACM SIGSOFT Software Engineering Notes. 36 (4): 1–10. doi:10.1145/1988997.2003643..

  • [6]

    ^van der Poll, John A.; Paula Kotze (2002). "What design heuristics may enhance the utility of a formal specification?". Proceedings of the 2002 Annual Research Conference of the South African Institute of Computer Scientists and Information Technologists on Enablement Through Technology. SAICSIT '02: 179–194..

  • [7]

    ^S-Cube Knowledge Model: Formal Specification.

阅读 26
版本记录

  • 暂无