The software industry has proved the design value of modular component technology. Modern programs are composed of objects and modules that capture generic software features. This model is valuable for the verification technology as well, and we build our own tools using the modular mechanisms.
In order to apply formal tools to large software systems, verfication technology needs a logical interpretation of modules. We propose a LPE where modules are viewed as logical theories, and modular software verification is accomplished through reflection. Just as modular software design provides lightwieght flexible lightweight programs, the modular theory design provides lightweight formal design. We are currently applying these mechanisms to provide run-time opotimization of Ensemble, a structly modular communication system.
The technology we describe here solves some of the key problems in the task of building frameworks for interoperable representations.