Grant: Discovery Grants Program - Individual

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.