- Autonomous Systems (collaboration with NASA/Ames)
Autonomous systems, especially those in safety-critical applications, must
be extremely reliable. Unfortunately, the inherent complexity of autonomy
software, and its interaction with rich, uncertain environments, makes it
very difficult to verify such systems using traditional testing techniques.
Formal verification, particularly model-checking, has been used successfully
to formally verify complex hardware and software systems.
- Embedded and Autonomous Systems
Computers are becoming pervasive in running our machines, from
spacecraft and power plants, to cars and household appliances. Increasingly,
these systems are required to perform more complex tasks and to do so at
greater and greater levels of autonomy. Many of these systems are in
safety-critical applications, where errors can result in loss of equipment,
or even human life.
- Implicit Invocation Systems
This project is developing a formal but practical basis for reasoning
about architectural styles that employ implicit invocation
(event-multicast). Despite a decade of commercial and academic experience in
constructing systems that adopt such styles, techniques for assuring system
correctness (or even adequacy) remain ad hoc and poorly understood.
- Secure, Survivable Systems
An integral part of modeling the global view of network security is
constructing attack graphs. In practice, attack graphs are produced manually
by Red Teams. Construction by hand, however, is tedious, error-prone, and
impractical for attack graphs larger than a hundred nodes. In this paper we
present an automated technique for generating and analyzing attack graphs.
We base our technique on symbolic model checking algorithms, letting us
construct attack graphs automatically and efficiently.