Relational and Algebraic Methods in Software Developement

软件开发中的关系和代数方法

• 批准号: RGPIN-2017-05374
• 负责人: Winter, Horst
• 金额: $ 1.68万
• 依托单位: Brock University
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2022
• 资助国家: 加拿大
• 起止时间: 2022-01-01 至 2023-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=749949
• 关键词: Relational; Algebraic; Methods; Software; Developement

We have all experienced errors or bugs in software products. An error causing some text processing software to malfunction can be very annoying but it is normally not critical with serious consequences. On the other hand, if an error in a system affects a safety critical system such as the autopilot of an airplane or the control unit of a nuclear plant, failure is not acceptable. Software engineers usually develop good testing strategies allowing them to detect most errors hidden in programs, but testing can never guarantee that the program is free of errors. Formal methods are the study and application of mathematically-based techniques addressing this problem. They are used for the specification, development, and verification of software and hardware components. This is normally done by providing a condition that should be satisfied before executing a particular piece of code, another condition that will hold after executing the code and a proof of this fact. The verification process is usually complicated and very time consuming so that quite often (semi)automatic theorem provers are used in order to automate at least parts of the task. The importance of Formal Methods is indicated by the fact that a certification of a computer system following the Common Criteria for Information Technology Security Evaluation standard (ISO/IEC 15408) starting at level EAL5 requires the use of (semi)formal tools. Most approaches to formal methods are based on languages and calculi derived from first-order logic, i.e., they use the standard logical operations and quantifiers. On the other hand, recent experiments have shown that certain theorem provers work very successfully with algebraic theories, i.e., in situations where axioms and theorems are equations and proofs are calculations similar to those in regular algebra. This research will use the equational theory of binary relations in program specification, development, and verification by focusing on three major aspects. Firstly, the research will expand the mathematical theory and the calculus of binary relations into areas currently not yet developed such a parallel programming. Secondly, a library containing all aspects of the theory of relations and their implementation will be developed for the interactive programming language and theorem prover Coq. Since Coq is also a programming language we will be able to handle theory, proofs and implementation in one system. The library will be a base for all practical applications of the theory, i.e., any concrete development of verified software. Last but not least, these aspects and tools will be applied in order to develop correct software ranging from conceptual examples to real world applications.

我们都经历过软件产品中的错误或bug。导致某些文本处理软件故障的错误可能非常烦人，但通常不会造成严重后果。另一方面，如果系统中的错误影响安全关键系统，例如飞机的自动驾驶仪或核电站的控制单元，则故障是不可接受的。软件工程师通常会开发出良好的测试策略，使他们能够检测出程序中隐藏的大多数错误，但测试永远不能保证程序没有错误。形式化方法是对解决这一问题的基于几何的技术的研究和应用。它们用于软件和硬件组件的规范、开发和验证。这通常通过提供在执行特定代码段之前应该满足的条件、在执行代码之后将保持的另一个条件以及该事实的证明来完成。验证过程通常是复杂和非常耗时的，因此经常使用（半）自动定理证明器来自动化至少部分任务。正式方法的重要性是由以下事实表明的，即在EAL 5级开始的信息技术安全评估标准（ISO/IEC 15408）的通用标准的计算机系统的认证需要使用（半）正式工具。大多数形式化方法都是基于语言和来自一阶逻辑的演算，即，它们使用标准的逻辑运算和量词。另一方面，最近的实验表明，某些定理证明器非常成功地与代数理论，即，在公理和定理是方程，证明是类似于正则代数的计算的情况下。本研究将使用二元关系的等式理论在程序规格说明，开发和验证，重点放在三个主要方面。首先，本研究将数学理论与二元关系演算拓展到目前尚未发展出并行程序设计的领域。其次，一个包含关系理论及其实现的所有方面的库将为交互式编程语言和定理证明器Coq开发。由于Coq也是一种编程语言，我们将能够在一个系统中处理理论，证明和实现。该图书馆将成为该理论的所有实际应用的基础，即，任何经过验证的软件的具体开发。最后但并非最不重要的是，这些方面和工具将被应用，以开发正确的软件，从概念的例子到真实的世界的应用程序。