Category: Verification

This blog post is coauthored by Dionisio de Niz.

Software with timers and clocks (STACs) exchange clock values to set timers and perform computation. STACs are key elements of safety-critical systems that make up the infrastructure of our daily lives. They are particularly used to control systems that interact (and must be synchronized) with the physical world. Examples include avionics systems, medical devices, cars, cell phones, and other devices that rely on software not only to produce the right output, but also to produce it at the correct time. An airbag, for example, must deploy as intended, but just as importantly, it must deploy at the right time. Thus, when STACs fail to operate as intended in the safety-critical systems that rely on them, the result can be significant harm or loss of life. Within the Department of Defense (DoD), STACs are used widely, ranging from real-time thread schedulers to controllers for missiles, fighter planes, and aircraft carriers. This blog post presents exploratory research to formally verify safety properties of sequential and concurrent STACs at the source-code level.

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.

When we verify a software program, we increase our confidence in its trustworthiness. We can be confident that the program will behave as it should and meet the requirements it was designed to fulfill. Verification is an ongoing process because software continuously undergoes change. While software is being created, developers upgrade and patch it, add new features, and fix known bugs. When software is being compiled, it evolves from program language statements to executable code. Even during runtime, software is transformed by just-in-time compilation. Following every such transformation, we need assurance that the change has not altered program behavior in some unintended way and that important correctness and security properties are preserved. The need to re-verify a program after every change presents a major challenge to practitioners--one that is central to our research. This blog post describes solutions that we are exploring to address that challenge and to raise the level of trust that verification provides.