Relational Methods in Software Development

上世纪90年代中期，奔腾处理器声名狼藉。尽管从有缺陷的浮点单元中得到错误的结果在实践中极为罕见，但它可能会影响到安全关键系统，如飞机的自动驾驶仪或核电站的控制单元。这个和其他的例子表明，如果人的生命处于危险之中或潜在的损失是巨大的，正确的计算机系统是必不可少的。形式方法是解决这个问题的基于数学的技术。与（半）自动化定理证明器一起，这些技术用于软件和硬件组件的规范、开发和验证。在EAL6和EAL7级别上遵循信息技术安全评估标准（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.