Polygon Processing for Safety-Critical Embedded Systems

Modern industrial embedded systems in the automotive industry integrate a steadily growing functional range. In the past years, all these systems were restricted to only monitor components of the own car as done e.g. by fuel injection and anti-lock braking systems. Current and future embedded systems, however, are also aware of the environment of the car. Radar and optical sensors are already available in many cars to observe the objects in the environment of the car. These systems can now be used to analyse the situation, to assist the driver and even to actively take over some of his tasks, similar to the adaptive cruise control (ACC), which has now been well-established for a long time.

Whenever the spatial behaviour of vehicles has to be taken into account, physical objects and situations are naturally modelled as geometric objects and properties. In many cases, it is thereby sufficient to model the environment as a two-dimensional plane, and the objects can be approximated by polygons on that plane. A lot of algorithms for dynamic motion planning or collision detection follow this approach. For the manipulation of these objects, well-known geometry algorithms are used. In particular, algorithms for manipulating polygons, i.e. to triangulate a polygon, to determine its convex hull, and to compute the intersection, union or difference of a given set of polygons are fundamental algorithms to solve difficult motion planning and collision detection problems.

Although these algorithms are not new, their use in upcoming safety-critical embedded systems, used e.g.~in automobiles, calls for a more rigorous treatment to guarantee the correctness for all possible inputs. To this end, formal definitions of geometric objects and primitives are required to specify and verify fundamental algorithms of computational geometry. At a first glance, the definition of geometric primitives appears to be easy, since they can be depicted in a natural and intuitive way. As a consequence, geometric algorithms are often only informally given by means of pictures. However, at a second glance, even simple definitions turn out to be more complicated than expected: For example, what is the intersection point of two lines, if both are identical? For this reason, most algorithms work under certain precondition like all points are pairwise distinct or no three points are collinear.

In order to guarantee that all possible cases are consistently handled and that the used algorithms work as expected in all possible cases, we recommend the use of interactive theorem provers to reason about required definitions and algorithms. However, finding consistent definitions that also hold for degenerate input data is surprisingly difficult. In fact, we found that for many predicates, no definition reflects the intuitive understanding in all cases. For example, to decide whether a point on the edge of a polygon belongs to the interior or not, yields essential problems when used in one or the other algorithm. This makes it inherently difficult to develop a software library for safety-critical embedded systems that process geometric data.

We implemented a software library for the class of algorithms. In contrast to other software libraries like CGAL, our software library was designed to meet the following requirements, which come from the embedded systems area:

• Verification. Since most applications are safety-critical, great care has to be taken when designing the systems. In particular, degenerate cases impose many tricky and unforeseen problems that challenge the robust design of these systems. For this reason, formal verification is routinely performed as a complementary technique to testing and simulation in order to ensure the correctness of the system. We use three-valued logics to specify geometric primitives and to build a verified kernel library. To this end, we employ the interactive theorem prover HOL4 for checking the formalised algorithms with respect to their specifications.
• Conservative Computations. In general, the limited precision of the arithmetic operations of microprocessors leads to a loss of information. The use of arbitrarily precise arithmetics or interval arithmetic yields algorithms that are too complex for small embedded devices. Relying on the usual rounding methods as provided by the IEEE 754 standard for floating point numbers, however, may lead to wrong results in geometric computations. Hence, we conclude that there is a need for explicit rounding functions that approximate the results in a conservative manner according to the specific needs of the particular algorithms.
• Limited Resources. Due to economic constraints, only very limited resources are usually available on embedded systems. On the other hand, the response time of a system must often fulfil given real-time constraints. Hence, an application-specific memory management is required for embedded systems. In particular, this component includes mechanisms to limit the size of the current model and the time needed for computations.

Further Reading

• J. Brandt and K. Schneider: Using Three-Valued Logic to Specify and Verify Algorithms of Computational Geometry
• J. Brandt and K. Schneider: A Verified Polygon-Processing Library for Safety-Critical Embedded Systems