CODES: Compositional DSLs for Enhancing Software
The goal of this project is to study how domain-specific languages (DSLs) can be used to represent components of legacy systems and to use the DSLs to enhance those components. The project involves formal methods, compilers, and program analysis, such as symbolic execution.
The abundance of legacy components continues to hinder systems owned and operated by the government. In some cases, a legacy component is a unit of software for which there is an updated implementation that is faster or more secure. In other cases, a legacy component is an entire software subsystem, such as a device driver stack, that has become difficult to maintain. Rewriting an entire system, such as flight control software for an unmanned aerial vehicle, to address the deficiencies of a legacy component is prohibitively expensive, from financial, engineering, and risk perspectives. Thus, the capability to enhance or replace individual legacy components is needed. The challenge is the difficulty in ensuring that the new software safely composes with the rest of the system. This means that the new software has to be not only functionally correct, but also compatible with the rest of the system.
Our research addresses the challenges above in the TA2 technical area of the V-SPELLS program. Our goal is to deliver an integrated environment for specifying software components using DSLs and verifying that these DSLs safely compose with a legacy system. Our work uses mathematically precise specifications and symbolic reasoning to compose and verify DSLs of large legacy systems.
Our primary approach builds on FORMULA, a language and tool originally developed at Microsoft Research for specifying domain-specific languages (DSLs) and verifying properties of those DSLs. We use FORMULA to formalize the semantics of DSLs and their compositions, thus giving us confidence that the abstractions we develop satisfy the properties we wish to verify.
As a result of this project, we have implemented a symbolic model finding procedure for FORMULA that allows us to "complete" partial models. In a nutshell, a partial model is one in which there are unknowns (variables) in certain places. Our model finding procedure allows us to fill in the blanks in a way that satisfies the rules of that model's DSL.
