Achieving Formal Interoperability Jose Meseguer (SRI) and Carolyn Talcott (Stanford University) (Position paper for SEKE Formal Methods Panel, 18 June 1998) In a large software system we are typically concerned with a range of very different requirements, such as functional correctness, performance, real-time behavior, concurrency, security, and fault tolerance, which correspond to different views of the system and that are typically expressed in different formal systems. Often these requirements affect each other, and in practice we find ourselves in constant need of moving back and forth between different notations and formalisms capturing different aspects of a system. It can be extremely difficult to reason about the mutual interactions of these different aspects and it is crucial to have tools to support such reasoning. Furthermore, to manage the complexity and evolution of complex systems it is important to have formal representations at different levels of abstraction such as architectural descriptions, formal specifications, finite state models, and code structure. Again it is important to be able to move rigorously across levels and to understand precisely what constraints are imposed by descriptions at the different levels upon one another. At present, formal methods for software specification and verification are monolithic, in the sense that in each approach only one formal system or specification language is used to formalize the desired system properties. For this reason, although formal approaches are very useful at their appropriate level of abstraction, their formal systems, and the tools based on them, are as it were autistic, because they lack the theoretical basis for being related to other formalisms and to their supporting tools. As a consequence, it is at present extremely difficult to integrate in a rigorous way different formal descriptions, and to reason across such descriptions. This situation is very unsatisfactory, and presents one of the biggest obstacles to the use of formal methods in software engineering because, given the complexity of large software systems, it is a fact of life that no single perspective, no single formalization or level of abstraction suffices to represent a system and reason about its behavior. To manage complexity and provide more effective environments for building software, it is essential to develop methodology and notations for truly plug and play components; both at the application level and at the level of tools for formal specification and analysis. Thus our formalisms and tools must support descriptions of components (applications, tools, notations ...) that provides a basis for ``off-the-shelf'' selection and semantically meaningful interoperation. Such descriptions must specify information such as: -what a component does; -how to interact with the component; and -the requirements and limitations of the component in a language that in meaningful to potenial users. Since no single notation or formalism will be best for all purposes, and new problems arise with each new kind of application, it is essential that our formal tools are highly extensible and naturally allow definition an use of new notations and concepts. Since the most basic need appears at the level of relating and integrating different mathematical formalisms, the foundations required must be ``metamathematical'' in nature. That is, they must provide rigorous foundational answers to the questions: (*) What is a logical formalism? (*) How can different formalisms be related? Answers to such questions can provide a rigorous basis on which to build very powerful and widely applicable ``meta-tools'' to support the formal interoperation of different formalisms and their associated tools. We need (meta-)formal methods and tools to achieve Formal Interoperability that is, the capacity to move in a mathematically rigorous way across the different formalizations of a system, and to use in a rigorously integrated way the different tools supporting these formalizations. Meta-tools of this kind may include: (*) Meta-logical frameworks, in which many different formalisms --- logics, specification languages, architecture description languages, diagrammatic notations, programming languages --- can be defined, executed, and interoperated. (*) Meta-logical translators, in which rigorous, semantically meaningful translations between any given pair of formalisms can be defined and automated. This can be extremely useful to vastly increase the applicability of tools, for example, to use a theorem prover for one logic to prove theorems in a different logic. (*) Meta-logical module calculus tools, which given specifications in an arbitrary formalism, or in several several formalisms, can support powerful parameterization and module composition operations to combine those specifications in a highly modular and reusable way. Reflection is a system's ability to represent and control its own metalevel. In this way, very powerful techniques to extend, adapt, and modify a system become available. Many researchers have recognized the great importance and usefulness of reflection in programming languages, in theorem-proving, in concurrent and distributed computation, and in many other areas such as compilation, programming environments, operating systems, fault-tolerance, and databases. In particular, reflective methods are enormously useful to achieve formal interoperability. They provide for extensibility, for the definition and execution of meta-tools which in turn can be used to generate special purpose tools. They also provide a powerful basis and analysis of formal specifications and system designs. Rewriting logic [1,2] is a highly promising basis for a meta-logical formalism which is reflective [3], and in which many languages and logics have already been formalized [4]. The use of the Maude tool [5,6] based on rewriting logic, as a meta-logical framework tool is currently being actively investigated. Maude specifications are executable and Maude implements the reflective capability of rewriting logic. Examples of executable specifications that have been developed include: interoperation of architecture descriptions [7], translations between logics [4,13], theorem provers [9,10], and security protocols [8]. Reflection is heavily used in translations between logics and in theorem proving tools to manipulate and transform theories as data, and also to define proof tactics; in the work on secure protocols, the reflective capabilities have been used to explore the space of possible executions and to discover potential attacks. The OMRS framework for interoperation of mechanized reasoning systems [11] is being mapped to rewriting logic [12] as a basis for implementation of this framework. [1] Jose Meseguer Conditional Rewriting Logic as a Unified Model of Concurrency, Theoretical Computer Science, 96,(1), pp. 73-155, 1992. [2] Jose Meseguer, Rewriting Logic as a Semantic Framework for Concurrency: a Progress Report, in Concur96, 1996. [3] Clavel, M. and Meseguer, J., Reflection in Rewriting Logic, in Proceedings of Rewriting Logic Workshop'96, Electronic Notes in Theoretical Computer Science, 4, 1996. [4] Narciso Marti-Oliet and Jose Meseguer, Rewriting Logic as a Logical and Semantic Framework, in Handbook of Philosophical Logic (D. Gabbay ed.), Kluwer Academic Publishers, 1997. [5] Jose Meseguer, A Logical Theory of Concurrent Objects and its realization in the Maude Language, in Research Directions in Concurrent Object-Oriented Programming, (G. Agha, P. Wegner and A. Yonezawa editors), pp. 314-390, MIT Press, 1993. [6] M. Clavel, S. Eker, P. Lincoln, and J. Meseguer. Principles of Maude. In Rewriting Logic Workshop'96, Electronic Notes in Theoretical Computer Science, 4, 1996. [7] Meseguer, J. and Talcott, C., Semantic Interoperation of Dynamic Heterogeneous Architectures, Technical presentations at EDCS Architecture Cluster Meetings 1997, (available via http://www-formal.stanford.edu/clt/ArpaNsf/adl-interop.html). [8] G. Denker, J. Meseguer, and C. Talcott. Protocol Specification and Analysis in Maude. In Workshop on Formal Methods and Security Protocols (to appear) 1998. [9] Clavel, M. and Meseguer, J., Internal Strategies in a Reflective Logic. In Workshop on Strategies in Automated Deduction, CADE-14, Townsville, Australia, 1997. [10] Manuel Clavel, Francisco Duran, Steven Eker, and Jose Meseguer. Design and implementation of the Cafe prover and Church-Rosser checker tools. Technical report, SRI International, December 1997. [11] Giunchiglia, F. and Pecchiari, P. and Talcott, C., Reasoning Theories: Towards an Architecture for Open Mechanized Reasoning Systems. in Workshop on Frontiers of Combining Systems FROCOS'96, 1996. [12] Meseguer, J. and Talcott, C., Reasoning Theories and Rewriting Logic, (in preparation). [13] Manuel Clavel, Reflection in General Logics and in Rewriting Logic with Applications to the Maude Language, Doctoral Dissertation, University of Navarre, 1998.