Symbolic Model Checking of Software Specifications
(R. Anderson, Beame, Notkin)
Errors in software specifications cost money and, in some cases, threaten lives. Symbolic model checking based on binary decision diagrams (BDDs) is an efficient automatic verification technique that has been applied successfully to many hardware designs but only in a very limited way to software specifications. We apply this technique to large safety-critical software specifications. We show how to provide effective input encodings to symbolic model checkers and tune their algorithms to handle specifications given as communicating hierarchical state machines. Although BDD-based symbolic model checking typically is efficient, it can bog down when dealing with non-linear arithmetic that is prevalent in some software specifications. We develop extensions of standard model-checking techniques that hold the promise of circumventing this non-linear arithmetic bottleneck.

Constraint-Based Systems
(Borning)
A constraint describes some relation that we would like to keep maintained, for example, that a column in a table in a web page is at least 20 pixels wide, that the background color in a document becomes more yellow with age, or that window w1 is twice as high as window w2. In recent research we developed a number of fast and expressive constraint solvers for interactive graphical applications. We are now applying these solvers to web page layout, including html extensions to allow the page author to express constraints, and to interactive graphical editors. For more information please see the web pages for Constraint-Based Systems.

Program Restructuring
(Notkin)
Software maintenance tends to become more difficult as a system evolves, in part because the structure of the system degrades. Restructuring the system to overcome such entropy is one approach to reducing maintenance costs. However, restructuring does not make visible "progress" and it is itself error-prone. We are investigating an alternative approach, meaning-preserving restructuring. In this approach, the software engineer applies structural changes and a tool then finds a set of global, compensating changes that (together with the engineer's explicit change) will guarantee that the meaning of the program remains unchanged.

Reflection Models
(Notkin)
Given an existing software system and a task to accomplish, software engineers decide whether and how to proceed based on experience, judgment, and system-specific knowledge. For even modest-sized software systems, there is a substantial risk of making poor decisions, because it is difficult (if not impossible) for software engineers to maintain adequate knowledge of the source. To manage this risk, engineers often use high-level models to focus on particular aspects of the system relevant to the task. These models help the engineer reduce risk only if they are sufficiently accurate representations of the actual system. We have developed an approach that may help engineers determine whether their task-specific models are "good enough" to make informed decisions. An engineer defines a high-level structural model appropriate for the task at hand and also specifies how the model maps to the source. A tool then computes a reflexion model that shows the engineer where the high-level model is consistent with and differs from the source. Analyzing the reflection model and applying personal experience and judgment, an engineer can then assess the risk of proceeding with the task.

Object-Oriented Frameworks
(Notkin)
Frameworks are one of several approaches to exploiting the commonalities of a family of software systems. They have been used successfully in user interfaces, network management, and operating systems. Applying framework operations, such as instantiating a framework to a specific application, can be error-prone. This is, in part, because any errors in the operation are not found until the application itself is executed. We are exploring approaches to reducing these problems (and thus increasing the benefits of using frameworks) through the use of static typing in object-oriented languages and tools to help execute these framework operations.

Implicit Invocation Mechanisms
(Notkin)
Implicit invocation (also known as event-based) mechanisms allow software components to announce interesting events that cause the invocation of other components that have registered interest in those events. When carefully applied, implicit invocation can be used to structure software systems that are more easily integrated and that are more easy to evolve. We are exploring effective design approaches using implicit invocation, as well as the design space for implicit invocation mechanisms (including language-based and domain-specific mechanisms).

Source Model Extraction
(Notkin)
Reverse engineers depend on the automatic extraction of information from source code. Some useful kinds of information -- source models -- are well-known: call graphs, file dependences, etc. Predicting every kind of source model that a reverse engineer may need is impossible. We have developed a lightweight approach for generating flexible and tolerant source model extractors from lexical specifications. We have also performed an empirical study of a set of C call graph extractors. These extractors return different, often significantly different, call graphs when applied to the same programs.

Real-Time Systems
(Shaw)
Our research has been concerned with models, techniques, and tools for specifying, analyzing, and generating software for real-time applications. The emphasis is on requirements and design specifications; fast prototyping; real-time operating systems; real-time programming; and methods for describing, predicting, and verifying the timing behavior of programming languages and systems. Current research includes: using execution-time bounds and assertional logic to state and prove timing properties of higher-level language programs; building software tools that predict the deterministic execution times of programs; refining, implementing, and testing a specification method, called communicating real-time state machines; and studying the use of time-stamped event histories in real-time programming. Two themes of the research are the incorporation of time as a first-class specification and programming object, and the analysis and exploitation of concurrency.