Posted on by Verificationin
By Sagar Chaki
Software Solutions Division
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.
The Challenges of Formal Verification
The operating system (OS), which manages different resources, different threads, and different processes, is at the heart of all software. The OS relies on a scheduler for allocating the appropriate amount of processor time to all these threads (i.e., tasks). We are concerned here with real-time threads, i.e., those with periodically executing jobs that have hard deadlines. Processor time is a scarce resource that must be allocated properly so that every job completes by its deadline.
For real-time systems, the thread scheduler is critical and must be correct, not only in scheduling the threads correctly but also in ensuring that they are scheduled at the right time. In particular, these tasks are relegated to a class of thread schedulers that are also doing time enforcement, which is also known as budget enforcement. These thread schedulers ensure that a certain thread does not receive more processor time than needed, a critical function. For example, in an automobile, if the thread scheduler in a vehicle's system allocates too much processor time to the cruise control software, the electronic stability control software might fail to prevent the car from understeering (not turning fast enough) in a curve.
The goal of this research is to verify real-time enforcers, or timing enforcers, exhaustively in a mathematically formal way. More importantly, we want to do this verification at the source code level. For example, given C source code for a scheduler or enforcer, we want to prove that it schedules the threads correctly (e.g., respecting priorities) but also that it performs timing budget enforcement at the right time (i.e., stopping a thread just before it exceeds its allotted processor time).
As outlined in our recently published paper, Contract-Based Verification of Timing Enforcers, several factors complicate STACs verification:
While there have been previous efforts, these efforts have been restricted mainly to models (e.g., using timed automata and associated model checkers, such as UPPAAL.) Our goal with this research is to verify STAC systems at the source-code level, thereby reducing the semantic gap between what is verified and what is executed.
To verify systems at the source-code level, the scheduler essentially relies on timers. In single-processor systems, when the application threads are running, the OS by default cannot run. A separate timer mechanism in hardware must ensure that the thread is stopped, and the OS is given back control.
Through our research, we are working to ensure that these timers are being used correctly, which can be complicated for many reasons:
When attempting to write software programs, specifically software for safety-critical embedded systems, developers must take these challenges into account.
Applying Theorem Proving to Software
To verify STACs at the code-base level, we rely on deductive verification and essentially applying theorem proving to software. We are using a tool called Frama-C, which is a publicly available source-code analysis tool, for deductive verification for C source code.
Even though Frama-C is a source-code analysis tool, we still needed to manually specify function contracts and loop variants using the ACSL language. Frama-C checks automatically that these contracts and invariants are valid by constructing verification conditions and discharging them using backend satifiability modulo theory (SMT) solvers. Thus, by automating the tedious parts of the process, Frama-C makes deductive verification applicable to software of realistic complexity.
Verifying Zero Slack Rate Monotonic Scheduling
To verify a specific time real-time enforcer, we target the scheduler for zero slack rate monotonic (ZSRM), a type of fixed priority thread-scheduling technique for mixed-criticality systems. To put it more simply, ZSRM schedules the threads that execute a specific function periodically.
Given a set of threads with different levels of criticality (e.g., in an automobile, an engine control thread will have high criticality, while an audio player thread will have low criticality) ZSRM ensures that under overload conditions, preference is given to threads with higher criticality over those with lower criticality. Under nominal (i.e., non-overload) conditions, ZSRM uses rate-monotonic scheduling.
We plan to verify the following three qualities:
When a new thread goes to sleep, it does so because it has already executed and does not need to run anymore.
When the thread wakes up again and must execute, it will be added to the list.
A Foundation in Deductive Verification
We are basing our approach on deductive verification, which was introduced by Robert Floyd and Tony Hoare, as a way of reasoning about a program's correctness based on logical assertions. A central tenet of Hoare's logic is the Hoare triple:
To check if the above claim is valid, it is necessary to construct a logical formula called verification condition.
Floyd, also from Carnegie Mellon University, focused on creating verification conditions for programs without loops (i.e., straight code). Hoare, who thought of programming languages without pointers and aliasing, extended Floyd's approach to reason about programs, with loops and function calls, an extension known as Floyd-Hoare logic.
Although the premise remains the same, in the last 30 years the ideas introduced by Floyd and Hoare have matured into tools, such as Frama-C. Now, to verify ZSRM, pre/post conditions are written for code, often across function calls. Essentially, for a function, the precondition specifies that the state (values of arguments and global variables) under which it must be invoked, while the post-condition specifies the state (values of global variables and the return value, if any) under which it terminates.
We also specify a loop invariant for each loop, which is a condition that must be true just prior to the execution of the loop body. Given the pre/post conditions of functions, and the looping variants, Frama-C produces all the verification conditions and proves them using SMT solvers. It also interprets the results from the SMT solvers to provide diagnostic feedback in case a verification condition is found to be invalid.
Wrapping Up and Looking Ahead
Through our work, we have learned a lot about the limitations and powers of Frama-C. Initially, we implemented a simpler version of ZSRM, and verified the first two qualities: that the threads are in the correct order according to priority and that budgets are computed correctly.
More recently, we focused on transitioning to the fuller version ZSRM implemented as a Linux kernel module, and adding back some of the missing components in the source code. Our aim is to make it easier for us to transition this work to the public (a kernel module is the standard for contributing to the Linux community). We are working toward a public release of the ZSRM source code with full ACSL annotations.
By demonstrating higher assurance about well-defined pieces of software infrastructure, users will have overall higher confidence that the system will perform as designed. Our approach is also reproducible. The function contracts and loop variants are specified in the C code via ACSL annotations. Syntactically, all ACSL annotations are "comments" from the point of view of C. Thus, while these comments are ignored by a C compiler, and do not affect the meaning of the program, users of the code can read and understand the annotations, and re-verify them using Frama-C.
Another benefit that we have noted as a result of the verification is that if software developers understand that their code will be verified using Frama-C or another deductive verifier, they will structure it in such a way so that it becomes more understandable and verifiable. Instead of writing very complex "spaghetti code," developers provide a more elegant structure with well-designed loops and functions.
Once the proof is complete, these loop variants and pre/post conditions will let users know exactly
Providing this type of feedback is one of the aims of formal verification, to make programs clean and modular and understandable and well documented. In some sense, the Frama-C contracts are the best kind of documents because there is no ambiguity, and they offer a single interpretation that proves very powerful. We are also using ZSRM in a separate research project looking at Distributed Adaptive Real-Time Systems, so the results of this research benefit that project as well.
We welcome your feedback on this research in the comments section below.
Read the paper Contract-Based Verification of Timing Enforcers, which was presented at ACM SIGAda's High Integrity Language Technology International Workshop on Model-Based Development and Contract-Based Programming (HILT), October 6-7, 2016, Pittsburgh, PA, USA.
For more information on ZSRM, view the 2009 paper On the Scheduling of Mixed-Criticality Real-Time Tasksets by Dionisio de Niz, Karthik Lakshmanan, and Raj Rajkumar.