Relational Methods in Software Development

上世纪90年代中期，奔腾变得臭名昭著。尽管在实践中，从有缺陷的浮点单元中获得错误结果的情况非常罕见，但它可能会影响到安全关键系统，如飞机的自动驾驶仪或核电站的控制单元。这个例子和其他例子表明，如果人类生命受到威胁或潜在损失巨大，正确的计算机系统是必不可少的。形式化方法是解决这个问题的基于数学的技术。这些技术与(半自动)定理证明器一起用于软件和硬件组件的规范、开发和验证。这项技术的重要性体现在这样一个事实上，即遵循信息技术安全评估共同标准(国际标准化组织/国际电工委员会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.