Software development for safety-critical or security systems cannot tolerate the risk of failure or malfunctioning. Formal methods provide mathematical techniques that are used for the specification, development and the verification of complex systems in order to increase their reliability and robustness. By now, there is a vast collection of formal specification languages, theorem provers and model checkers, which serve as development tools in formal methods. These are usually
domain-specific tools that differ in their underlying logical foundations. The complex structure of real-world systems often requires a collaboration of these tools, which has not been systematically achieved so far due to their foundational diversity.

We propose a PhD topic, which will be concerned with the integration of formal methods tools via a semantic interrelation of their foundations, and with the scalability of these tools to industry. The work has three main objectives, which will provide us with the first steps towards a systematic integration of tools as well as their adaptation to less formal settings.

Firstly, we propose to develop a comprehensive framework in which logics can be represented and related to each other. The framework will adapt the application of theory graphs in [5], where logics will be represented as theories and interrelations between them will be established by theory morphisms. The representation of logics will cover both proof-theoretical and model-theoretical aspects as represented in the logical frameworks LF [2] and institutions [1], respectively. We will specify concrete logics and translations between them within the framework. We will use the specific translations to generalize the representation of logic translations in the framework.

Secondly, the framework will support the heterogeneity of all aspects of logics. More precisely,
we will introduce the notion of heterogeneous proofs and models. Heterogeneous proofs will be the proof-theoretical counterpart of heterogeneous specifications [4]. A heterogenous proof will consist of subproofs in different logics or even in informal languages like natural language. Logic translations will be used between subproofs as proof steps. Heterogeneous models will be the model counterpart for heterogeneous proofs. We will use heterogeneity for the collaboration of proof systems in verification tasks in order to distribute proof obligations among them.

Thirdly, we will extend the notion of heterogeneity of specifications and proofs to introduce the notion of flexible degrees of formality in theories. This means that a theory can be formal, semi-formal, informal as well as a combination of these forms. We will investigate how to establish theory morphisms between flexibly formal theories. Flexible degrees of formality will extend the mathematical content format OMDoc [3]. We will use these apply knowledge management services in specification and verification. We envision that these will contribute to the scaling of formal methods to large-scale industrial projects.

References

[1] J. Goguen and R. Burstall. Institutions: Abstract model theory for specification and programming. Journal of the Association for Computing Machinery, 39(1):95–146, 1992.

[2] R. Harper, F. Honsell, and G. Plotkin. A framework for defining logics. Journal of the Association for Computing Machinery, 40(1):143–184, 1993.

[3] Michael Kohlhase. OMDoc – An Open Markup format for Mathematical Documents [Version 1.2]. Number 4180 in LNAI. Springer Verlag, 2006.

[4] Till Mossakowski. Heterogeneous specification and the heterogeneous tool set. Habilitation thesis, University of Bremen, 2005.

[5] Florian Rabe and Michael Kohlhase. A Web-Scalable Module System for Mathematical Theories. Manuscript, to be submitted to the Journal of Symbolic Computation, 2008.