Relational and Algebraic Methods in Software Developement

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

*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.