Formal Modeling and Analysis of Requirements and Policy Documents (NSF) - Project page

Regulations, laws, and policies that affect many aspects of our lives are represented predominantly as documents in natural language. For example, the Food and Drug Administration's Code of Federal Regulations (FDA CFR) governs the operations of American bloodbanks. The CFR is framed by experts in the field of medicine, and regulates the tests that need to be performed on donations of blood before they are used. In such safety-critical scenarios, it is desirable to assess formally whether: 1) The regulation (CFR) is consistent, and 2) An organization (bloodbank) conforms to the CFR The proposed research is to develop natural language processing (NLP) techniques for extracting formal representations from regulatory documents. These representations are then analyzed for consistency and used to determine an organization's conformance to the regulation. This is a collaborative effort between researchers in NLP and formal methods and aims at producing an environment in which policy can co-exist in natural and formal languages.

Run-time Monitoring and Checking (NSF) - Project page

As the size of software grows, it becomes more difficult to test or verify the correctness of a system. Continuously monitoring of a running system is a complementary approach to increase the assurance of correct execution. We have developed a Monitoring and Checking (MaC) framework to monitor and check running systems against a formal requirement specification. We have also implemented a prototype of the MaC framework for monitoring and checking Java and C programs.

Model-Based Development: Code Generation (ONR MURI, NSF) - Project page

Model-based implementation of embedded software is a promising approach to improving reliability and development cost of embedded systems. Code generation is the last and the most challenging task of automatic synthesis of implementation from formal specification. We are studying various issues of transforming hybrid system models to digital programs, including platform-dependent adaptation and optimization, real time scheduling, and precise event detection. As a case study, we are implementing a CHARON-to-C++ code generator targeted to Sony’s quadruped robot dog, AIBO. Current implementation demonstrates that a simple CHARON specification in the form of a small set of differential equations is enough to describe complex behavior of robots such as getting up and down that would otherwise require tedious C++ programming to describe small amount of movement of every joint at every time step.

Model-Based Test Generation (NSF) - Project page

The goal of this project is to generate tests that can be used to validate an implementation confirms to a specification. For the model-based test generation, the goal is to automatically generate a test suite that meets particular coverage criteria from specification in EFSM or hybrid systems. The approach to integrate random test-trace generator with targeted test-trace generator based on model checking. We use model-checking approaches to make test generation more flexible, efficient, and effective. An enhanced model checker will work as a generic test generator: it takes the coverage criteria encoded in some temporal logic and the specification system as the input, and produces the test suite achieving the coverage. Essentially the combination of the generic test generator and the criteria given as temporal properties will function as a special test generator dedicated for such criteria. This is done without having to implement a different test generator for each coverage criteria. The approach also exploits well-developed model-checking techniques to make test generation more efficient. Moreover, the richness of temporal properties allows us to express both generic and system-specific coverage criteria.

Wireless Sensor Networks and Mobile Systems (NSF) - Project page

Our research involves three main tasks: (1) the design of a new programming paradigm for sensor networks that uses geographic abstractions to simplify programming tasks, (2) analyze and design new metrics for security for sensor networks, and (3) analysis and improvement of performance of 3G wireless networks. Our past work includes research on real-time communications over 802.11.

Hybrid Systems: CHARON (DARPA MoBIES) - Project page

CHARON is a language for modular specification of interacting hybrid systems based on the notions of agent and mode. For hierarchical description of the system architecture, CHARON provides the operations of instantiation, hiding, and parallel composition on agents, which can be used to build a complex agent from other agents. The discrete and continuous behaviors of an agent are described using modes. For hierarchical description of the behavior of an agent, CHARON supports the operations of instantiation and nesting of modes. Furthermore, features such as weak preemption, history retention, and externally defined Java functions, facilitate the description of complex discrete behavior. Continuous behavior can be specified using differential as well as algebraic constraints, and invariants restricting the flow spaces, all of which can be declared at various levels of the hierarchy. The modular structure of the language is not merely syntactic, but also reflected in the semantics so that it can be exploited during analysis.

Model based integration of embedded software (DARPA MoBIES) - Project page

The objective of this project is to develop a methodology and toolkit for design of embedded software for multi-agent communicating hybrid systems. The methodology will cover various design stages, including modeling, simulation, analysis, implementation, and monitoring. The methodology will be based on formal modular and hierarchical semantics of multi-agent hybrid systems. The methodology will improve the process for hybrid systems design by decreasing development costs through high-level modeling, by improving reusability by means of modular designs, and by developing more reliable designs with the help of analysis and runtime valiadation.

Embedded and Hybrid System Design and Implementation: High Assurance Systems Tools and Environment (HASTEN) (ARC) - Project page

The goal of the proposed research is to develop a framework for the integrated use of a suite of methods and tools for the specification, analysis, development, testing, prototyping, simulation and monitoring of embedded software. The framework is called HASTEN (High Assurance Systems Tools and Environments) and will be based on systems that the proposers have been studying separately for some time and can also include systems that are developed elsewhere. The primary methods of interest are: formal specifications, test generation from specifications, automated verification, prototyping and simulation, and run-time monitoring and checking. Each of the methods has its own strengths. Taken within the context of an `end-to-end' view of the software life cycle they can achieve together more than any one of them could do. However, these methods apply to different representations of the system at different points in its development and deployment. Furthermore, some of these methods need be enhanced to handle the resource limitation and constraint characteristics of embedded systems. The significant effort of the proposed work will be to enchance individual methods to support embedded systems.

Real-Time Systems: Specification and Analysis of Real-Time Systems (ACSR, VERSA, TREAT)

Process algebras without a notion of time have been used widely in specifying and verifying concurrent systems. A process algebra consists of a concise language, a precisely defined semantics and a notion of equivalence. The language is based on a small set of operators and a few syntactic rules for constructing a complex process from simpler components. The semantics describes the possible execution steps a process can take.
We have developed the Algebra of Communicating Shared Resources (ACSR) [Lee et al. 94, Lee et al. 96]. ACSR supports the notions of resources and priorities which make it a unifying framework that combines the areas of process algebra and real-time scheduling. The ACSR computation model is based on the view that the components of a real-time system execute synchronously time and resource consuming actions and communicate through instantaneous events. The events occur asynchronously, except when two components synchronize through matching events. For finite state ACSR processes, we have developed a sound and complete set of algebraic laws that can be used to prove two ACSR processes are equivalent, i.e., strongly bisimilar in our prioritized transition system.

Real-Time Programming Languages and Concepts (Publications)

Most programming languages are not suitable for real-time programming, in that they lack the ability to effectively express time. This deficiency makes it difficult to write real-time programs, and nearly impossible to reason about their timing behavior. We have explored several ways to express timing constraints within a program, and have developed three concepts with corresponding language constructs: temporal scope [Lee and Gehlot 85], timed synchronous communication [Lee and Davidson 87] and timed atomic commitment [Davidson et al 91]. Temporal scope allows timing constraints to be expressed in a block structured manner. A program written using temporal scope has predictable timing behavior, since either its timing constraints are satisfied or exceptions are raised. Furthermore, the specified timing information may be used by a run-time support system to schedule processes based on their timing constraints.
Timed atomic commitment is similar to its un-timed counterpart, in that both maintain the functional consistency of distributed activities. The difference is that traditional atomic commitment enforces eventual agreement between processes. However, timed atomic commitment requires that agreement be reached within a specific deadline, and the agreed-upon actions be executed in a deadline-driven fashion.