Archive
Verifying the Liskov Substitution Principle in C++ code: Part 1
When RTCA released DO-178C – the long-awaited update to the DO-178B standard for airborne software – they added a number of supplements to cover specific software development techniques. One of those techniques is object-oriented software development, covered by supplement DO-332. This supplement mentions the Liskov Substitution principle (hereafter abbreviated LSP) in FAQ #14 “Why is the Liskov Substitution Principle (LSP) important?” and gives more detail in FAQ #15 and #16. So, what is the LSP, and how can we make sure that a software design adheres to it? Read more…
Escher C Verifier released!
We are pleased to announce that Escher C Verifier is now a released product. This first release is later than planned, but goes beyond our original goal. We found that some of our pilot users had constructs such as function pointers and limited use of ‘goto’ in their software, so we decided to support these constructs in the first release after all.
Alongside eCv we have released an update to our established product Perfect Developer. PD facilitates the development and verification of software specifications, their refinement to a design, and optional code generation in a choice of programming languages.
Both the commercial editions and the capacity-limited free editions of the two tools are also available as a single combined product, Escher Verification Studio. See the Escher Technologies web site for more information.
Verifying programs that use function pointers
In safety-critical software, function pointers should be used sparingly or not at all. They complicate program flow and can make it very hard to understand what the program is doing. However, when used carefully in the right circumstances, they can actually simplify a program.
Typically, function pointers are used in C programs for two different purposes. The first is to connect a generic framework or function to the particular code that is needed in a specific application. The second is to allow a common piece of client code to handle different objects that have a common interface. Both of these can be accomplished in a much more structured way using virtual functions in an object-oriented language (such as C++). But if you’re restricted to C, function pointers offer the only comparable solution available.
Just as pointer arithmetic can be verified if you make some extra effort writing the specifications (see Verifying pointer arithmetic), so can well-designed code using function pointers. In this post I’ll show how you can do this with eCv. Read more…
eCv beta 1 released!
I’m pleased to announce that we’ve just released Escher C Verifier beta 1. We’re intending to keep the beta phase quite short, so barring major problems, full release of eCv should take place in January 2011. Read more…
Verifying programs that use ‘sizeof’
Consider the following code snippet (based on a real example of critical embedded software), whose purpose is to serialize some data and send it to another piece of hardware: Read more…
ArC is now eCv!
We’re now nearing the beta release of our C verification product. We’ve decided to call the product Escher C Verifier, or eCv for short. While we liked the name ArC (Automated Reasoning about C), there are just too many pieces of software already out there with ARC in the name. Read more…
Dynamic Memory Allocation in Critical Embedded Systems
Today I’m going to talk about why dynamic memory allocation is rarely used in critical embedded systems, and whether using only static allocation is a necessary restriction. I’m going to assume that maintaining system availability is critical, that there are hard real-time deadlines to be met, and that the system is long-running. Read more…
Verifying pointer arithmetic
Today I’ll look at whether code that uses pointer arithmetic is any harder to verify than equivalent code that does not use pointer arithmetic.
Consider this function for copying an array (or part of an array) into another array (or part of another array):
void arrayCopy(const int* src, int* dst, size_t num) {
size_t i;
for (i = 0; i < num; ++i) {
dst[i] = src[i];
}
}
Run-time checks: Are they worth it?
One of the criticisms levelled against the use of C in safety-critical software is that the C language does not provide run-time checks automatically. For example, when indexing into an array, there is no check that the index is in bounds. Likewise, when doing integer arithmetic in C, there is no check for arithmetic overflow. Read more…
Aliasing and how to control it
Today I’ll start by writing a simple function that determines the maximum and minimum of two integers. We want to return two values, and C doesn’t make that easy unless we declare a struct to hold them. So I’ll pass two pointers to where I want the results stored instead. Here goes:
#include "arc.h" void minMax(int a, int b, out int *min, out int *max) post(*min <= a; *min <= b; *min == a || *min == b) post(*max >= a; *max >= b; *max == a || *max == b) { *min = a < b ? a : b; *max = a > b ? a : b; }
I’ve highlighted the ArC annotations in green. Read more…
Need help with using C or C++ in critical systems? Click on my picture above.
David Crocker's Verification Blog 