1 Background

We have conducted research on practical automated support for formal methods and on building domain-specific reuse frameworks for the past five years.

Our formal methods research focuses on developing and evaluating automated static analysis techniques, e.g., flow analyses and model checking, for verifying explicitly stated correctness properties of concurrent and distributed software systems. Our work is set in the context of event-based and propositional specification formalisms applied to safely approximating finite-state models of system behavior.

The primary barrier to practical application of these techniques is the well-known state-explosion problem, where the number of possible global system states grows exponentially in the number of system processes. Our work [DC94,DC97,DC96a,DCH97,DS97] uses abstraction techniques to enable reduction in the cost of analysis while preserving the ability to conclusively verify system properties. Of particular relevance to the analysis of component-based systems is our work on analyzing partial software systems [Dwy97]. In this work, we analyze portions of systems that are provided as designs or code along with partial specifications of the remaining system components. This offers a number advantages over traditional whole-system analysis techniques. It enables reduction in the time required to perform the analysis, by orders of magnitude in many cases. Perhaps more importantly, it allows developers to apply static analysis techniques earlier in the software development process. As soon as architectural descriptions, interface specifications or portions of implementations are available the verification and validation efforts can proceed. These interface specifications can be used both as the goals of unit-level formal verification and as components of sub-system and system level analyses.

Since a primary goal of our work is to evaluate the practicality of using formal specifications and verification techniques, we have spent significant effort in developing automated tools that support analysis approaches, for example the FLAVERS [Dwy95] and TPN [DC96a] toolsets. By applying theses tools to the analysis of formal specifications derived from requirements of realistic software systems we can begin to understand the pragmatic issues of scalability and performance that are crucial to wide-spread acceptance of automated formal methods.

An understanding of the potential for practicing engineers to adopt such methods cannot, however, be gained by measuring tool performance alone. We must also consider the non-trivial costs of learning specification formalisms and of gaining an understanding of the processes and strategies that allow one to read and write "realistic" specifications. During the course of our analysis work we have gathered experience with reading and writing specifications in both automata and logic-based notations. As a means of transferring the knowledge of experienced specifiers to potential users of formal methods, we have developed a pattern system for specifications of reactive systems [DAC97]. The hope is that just as design patterns have been effective in encoding and leveraging design knowledge, so too will specification patterns be effective for knowledge of formal specifications.

Our industrial experience in developing a family of optimizing compiler and debugger products established our appreciation for modular, component-based systems. We have continued to apply those principles in our research. We have analyzed and exploited information about three distinct software domains: flow analysis [DC96b], discrete-time grid simulations [DW97b,DW97a], and graphical user interfaces [DCH97]. In the first two of these we have defined and constructed parameterized frameworks that support construction of software systems in those domains. In our simulation framework, called PAGS, we have found the need for a broad collection of framework components that can be composed to fulfill commonly occurring application needs. Issues of performance as well as functionality are important in this domains. For these reasons our framework provides an open-implementation.

Our formal methods and software framework research are not completely independent. We have used our automated analysis techniques to verify properties of our frameworks and we are working on research that uses our simulation framework to implement parallel versions of analysis algorithms.