Relational Methods in Software Development

在90年代中期，Pentium变得声名狼借。尽管从有缺陷的浮点单元中获得错误结果在实践中非常罕见，但它可能会影响安全关键系统，例如飞机的自动驾驶仪或核电站的控制单元。这个例子和其他例子表明，如果人类生命处于危险之中或潜在损失巨大，正确的计算机系统是必不可少的。形式化方法是解决这个问题的数学基础技术。与（半）自动定理证明器一起，这些技术用于软件和硬件组件的规范，开发和验证。这一技术的重要性是由以下事实表明的，即在EAL 6和EAL 7级的信息技术安全评估标准（ISO/IEC 15408）的通用标准的计算机系统的认证需要应用正式的方法。大多数形式化方法都是基于语言和来自一阶逻辑的演算，即，它们使用标准的逻辑运算和量词。另一方面，最近的实验表明，某些定理证明器非常成功地与代数理论，即，在公理和定理是方程，证明是类似于正则代数的计算的情况下。二元关系的各种形式的代数理论被认为与一阶逻辑一样强大，因此非常适合作为形式方法的代数方法。特别是，微积分允许基于等式理论在同一语言中处理程序和属性。拟议的研究将集中在应用程序的规格说明，开发和验证的二元关系的演算。这包括开发一种具有广泛抽象机制的面向对象编程语言，以及一种用于继承表示为二进制关系的方法属性的系统。此外，模糊关系的代数理论，特别是高阶模糊关系，将进一步研究导致模糊控制器的代数理论。最后但并非最不重要的是，关系的定性空间推理，如地理信息系统和建筑布局的应用将进行研究。

In the mid 1990s the Pentium became infamous. Even though obtaining wrong results from the flawed floating point unit was extremely rare in practice, it could have affected safety critical systems such as the autopilot of an airplane or the control unit of a nuclear plant. This and other examples show that correct computer systems are essential if human life is at risk or the potential loss is enormous. Formal methods are mathematically based techniques addressing this problem. Together with (semi)automatic theorem provers, those techniques are used for the specification, development, and verification of software and hardware components. The importance of this technique 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) at level EAL6 and EAL7 requires the application of formal methods. Most formal methods are based on languages and calculi derived from first-order logic, i.e., they use 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. The algebraic theory of binary relations in its various forms is known to be as strong as first-order logic and, therefore, very suited as an algebraic approach to formal methods. In particular, the calculus allows handling programs and properties in the same language based on an equational theory. The proposed research will focus on the application of the calculus of binary relations in program specification, development, and verification. This includes the development of an object-oriented programming language with extensive abstraction mechanisms and a system for inheriting properties of methods expressed as binary relations. Furthermore, the algebraic theory of fuzzy relations, and higher-order fuzziness in particular, will be further investigated leading to an algebraic theory of fuzzy controllers. Last but not least, applications of relations to qualitative spatial reasoning such as Geographical Information Systems and architectural layout will be studied.