Posted on by Autonomy and Counter-Autonomyin
by James Edmondson
Senior Member of the Technical Staff
Software Solutions Division
This post was co-authored by Sagar Chaki
In 2011, the U.S. Government maintained a fleet of approximately 8,000 unmanned aerial systems (UAS), commonly referred to as "drones," a number that continues to grow. "No weapon system has had a more profound impact on the United States' ability to provide persistence on the battlefield than the UAVs," according to a report from the 2012 Defense Science Board. Making sure government and privately owned drones share international air space safely and effectively is a top priority for government officials. Distributed Adaptive Real-Time (DART) systems are key to many areas of Department of Defense (DoD) capability, including the safe execution of autonomous, multi-UAS missions having civilian benefits. DART systems promise to revolutionize several such areas of mutual civilian-DoD interest, such as robotics, transportation, energy, and health care. To fully realize the potential of DART systems, however, the software controlling them must be engineered for high-assurance and certified to operate safely and effectively. In short, these systems must satisfy guaranteed and highly-critical safety requirements (e.g., collision avoidance) while adapting smartly to achieve application requirements, such as protection coverage, while operating in dynamic and uncertain environments. This blog post describes our architecture and approach to engineering high-assurance software for DART systems.
The Challenges of Autonomy
A major concern of the Federal Aviation Administration (FAA) and other government agencies is incorporating drones safely into national air space (NAS). Government agencies want a system to provide high assurance that adding UAVs to the NAS won't cause problems.
The DoD has drone-related concerns of its own. The DoD worries that UAVs cannot be brought into the formal acquisition cycle, and therefore it must field them as prototypes. While this restriction causes acquisition problems, it also places limits on what the DoD can do with autonomous systems.
DART systems are groups of physically separated cyber-physical systems (CPS) that operate in an environment, intelligently adapt their behavior, and communicate and collaborate to achieve some overall group objective.
There are many challenges to achieving high-assurance DART software:
Our group--in addition to Sagar and myself, the team of researchers included Dionisio de Niz, Bjorn Andersson, Mark Klein, Jeffery Hansen, David Kyle, Gabriel Moreno, Scott Hissam, Charles Hammons, and Arie Gurfinkel--aims to engineer and objectively analyze high-assurance software for DART systems.
Foundations of Our Work
In recent years, we have focused on developing open-sourced middleware that is:
These priorities became the basis for several SEI research initiatives:
Our work on DART builds on the exploratory research we began with MCDA, but we added more verification, more emphasis on middleware technologies, and thread scheduling to make an approach that we can verify and transition to our stakeholders and the public. With this latest work, we also added self-adaptive behaviors (i.e., agents behave intelligently to change their behavior to adapt to changing external situations.)
In DART, we moved beyond mere code analysis to produce C++ code that will run on an actual drone platform. This code uses GAMS for communication among agents, and MADARA to interact with the (simulated) physical platform (i.e., robots).
The DART Approach
To precisely program DART systems and specify properties, we use a domain-specific language, DMPL (DART Modeling and Programming Language), and the SEI's Architecture Analysis and Design Language (AADL) notation.
Built for programming distributed systems, DMPL resembles C and C++, but it has the concepts of nodes, communication, and shared variables. DMPL is an extension of a language called DASL, which we developed for MCDA. The DMPL language is a higher level of abstraction, so we can analyze it more tractably. Once we have conducted this analysis, we then generate code in C++ that uses GAMS and MADARA, as mentioned earlier.
AADL helped us define the architecture and environment and extend integration of DASL to lend structure to the interacting elements that are going to execute. DMPL interfaces with the AADL architecture, resulting in a better fidelity model for verification. The use of AADL provided a nice synergy because while AADL is an architecture description language, it is also extensible.
For example, the designers of AADL understood that AADL by itself is not going to specify the system in complete detail. They therefore allowed an extension mechanism, called an annex mechanism, by which one could add a new domain-specific language to AADL as a "sub-language". The annex allowed us to incorporate DMPL into AADL as a sub-language (i.e., we are developing a DMPL annex for AADL.)
Our end vision is that architects can design the system using this AADL-DMPL combination. Since system components are well specified (i.e., structure, semantics, and communication mechanisms), and code is generated automatically from them, users can have high confidence that the analysis results apply to the real system.
Verifying the DART System
We are using the following techniques to verify DART systems:
We are using all of these techniques to analyze DART systems at a higher level of abstraction.
From Ground to Space
We have not solved all the problems, or even all of the important problems, concerning DART assurance. Our work continues in the following areas, with particular focus on transition to production systems:
Making Verification of Distributed Artificial Intelligence Available
Our aim with this work was to give the public access to, and encourage collaboration on, artificial intelligence development, including an infrastructure for building and verifying distributed systems. We know that our approach has the potential to scale to hundreds of robots, which, if successful, would be unique among similar systems currently in use.
Our approach, conversely, is more rigorous and defines a very precise behavior. We innovate, not just in terms of features but also in terms of how easy it is to put together. Our approach also seeks predictability, so when you program you know what you are supposed to get.
In our experience working with government and industry projects, we continually see complex production systems go over budget as a result of unexpected behaviors. Our driving focus has therefore been to make an approach that is well defined and predictable because it is easy to get lost in all the emergent behaviors that occur as soon as a complex system is developed and deployed.
We welcome your feedback on this work in the comments section below.
All of our tools developed through our work on verifying distributed systems are BSD-Licensed (i.e., available via open source with minimal restrictions).
GAMS is available on GitHub.
Madara, Middleware for Distributed Applications, is available on SourceForge.
DART Software: https://github.com/cps-sei/dart
DART Website: http://cps-sei.github.io/dart