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.

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.

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.

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.