A Reflective Framework for Formal Interoperability

Investigators

Carolyn Talcott, Stanford University
Jose Meseguer, SRI

Project Summary

In practice we find ourselves in constant need of moving back and forth between different formalizations capturing different aspects of a system. For example, in a large software system we typically have 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, but it can be extremely difficult to reason about their mutual interaction, and no tools exist to support such reasoning.

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. 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.

We will develop new, formal interoperability methodologies and generic meta-tools that are expected to achieve dramatic advances in software technology and formal methods:

A general methodology for defining inter-language translations, where the languages can be architectural description languages (ADLs), formal specification languages, or programming languages, and where the mappings may move across these different categories of languages.
A formal language translation meta-tool that, given formal specifications for two languages and their mapping will generate an executable translator tool transforming statements and modules in one language into their counterparts in the other language.
A do-it-yourself methodology for generating semi-automatically a reasonably efficient theorem prover implementation from a meta-logical specification of the theorem prover's inference system; and for easily combining different theorem provers defined with this method.
A general methodology for creating and checking {\em heterogeneous proof objects} that can certify the correctness of the final result of a proof effort involving different theorem provers working in a distributed way.
A heterogeneous meta-proof checker tool, that, given meta-logical specifications of several formal systems and their inter-translations will generate a proof checker for heterogeneous proofs in the combined system.
A general methodology for endowing formal specification languages and declarative programming languages with powerful and extensible module composition mechanisms in a formalism-independent way.
A module calculus meta-tool that, given a logic-based specification or programming language satisfying reasonable requirements will generate an executable language extension of it, enjoying powerful and extensible module composition operations.
A metaprogramming methodology using modules reified as data, for reflective adaptation of software modules at runtime that may depend on changes in their environment.

Other Notes

There is work related to hardware verification using our tools and methods and good potential for it in Maude:
- Goguen verification of adders and other hardware in OBJ.
- Vicky Stavridou and her team at Royal Holloway also used OBJ very extensively in hardware verification efforts.
- Maude contains OBJ as a functional sublanguage and executes much faster than OBJ. We think that Maude has great, but as yet unrealized, potential for application to hardware verification. In particular, its support for concurrent objects, which model very naturally hardware components, complements well the purely equational level (that extends OBJ). Furthermore, the theorem proving tools that we will be developing under your program will provide good support for proving inductive properties of hardware systems.
- Alex Bronstein phd thesis [under Talcott] using Boyer-Moore prover to verify synchronous circuits - including an abstract pipelined cpu
- David Cyrlik phd thesis [under Talcott] using PVS to verify hardware (for example the DLX processor) -- he developed a new temporal logic with decidable fragments well suited for hardware verification and that underlies much of the actual verification activity.

In addition to the hardware verification applications, a subset of Maude called Simple Maude has been applied as a machine-independent parallel language to program parallel machines, and its suitablility for this purpose has been demonstated for the Rewrite Rule Machine (RRM) architecture. In particular, we have:

A paper explaining Simple Maude and showing how it can be applied to program a very wide range of parallel applications
A paper on parallel compilation for Simple Maude onto SIMD and MIMD/SIMD machines
An experimental compiler that takes Simple Maude rewrite rule programs as inputs and generates parallel code in the RRM instruction set
Simulation results, giving performance estimates for an RRM system running the parallel code for different applications, documented in several papers.

The main advantages that we have found for using Simple Maude as a parallel language are:

High level declarative way of programming, yet very well suited and versatile to express efficiently a wide range of applications such as signal processing, image processing, parallel simulations, and of course symbolic computing.
Use of formal program transformations for optimizing the code is easy, because programs are logical theories
Machine-independent, yet efficient compilers can be built for many different machines, including massively parallel ones
Program verification is much more feasible than for conventional parallel languages (say HPF, or some parallel C++) because of the simple logical basis and semantics of the language.

Last updated by Carolyn Talcott clt@cs.stanford.edu 10 July 1998.