User story: TU Munich, Institute of Flight System Dynamics

The Institute of Flight System Dynamics at the Technical University of Munich oper­ates a Diamond DA42 NG as a flying testbed. Its purpose is to test the institute’s re­search in the area of flight control and navigation algorithms in a real environ­ment.

The aircraft is modified and equipped with an electro-mechanical fly-by-wire flight control system. To ensure safe operation under all conditions, the safety pilot on board can at any time decouple the fly-by-wire system from the orig­i­nal mechanical flight control system.

This modification enables the Institute to perform flight tests of newly devel­oped autopilot and flight management functions — or even carry out fully automated flights — without passing a complete certification of the system.

Nevertheless, the processes applied for the development of flight control laws and software of the flight control computer (FCC) are oriented towards the applic­able rules and standards for certification, like the ARP 4754A or the DO-178C.

The Institute developed the flight control laws of the FCC using a model-based ap­proach with Matlab Simulink/Stateflow. The devel­oped algorithms are automa­ti­cally translated into C source code using Embedded Coder. The code is then em­bedded into a frame­work that provides a run­time environ­ment, handling the inter­face data and issuing a cyclic call to the execution of the control laws.

Right now the FCC software has some 125k lines of code, of which 92% are auto-generated.

During the development of the control laws, assumptions about the maximum delay of the control loop are made. This entails hard real-time requirements for the FCC.

Verified compilation with CompCert

At first, GCC was used to generate the executable object code for the FCC without any optimizations. However, as more functionality was added, it became difficult to stay within safe execution-time bounds with GCC -O0.

Additionally, the need to comply with MathWorks’ DO Qualification Workflow and the wish to run automatic verification tools like Simulink Code Inspector restricted the optimization capabilities of Embedded Coder.

This made the Institute consider a move to the optimizing C compiler CompCert.

For the migration, no changes had to be made to the auto-generated source code. In the manually developed framework, changes had to be made to parts that used bit fields or relied on the exact memory mapping of structures:

Currently, the executable object code generated using CompCert is under test in a hardware-in-the-loop simulation. In comparison to the executable object code of GCC without optimization, the execution time was reduced by approximately 50%.

Stack usage analysis with StackAnalyzer

StackAnalyzer is used in order to ensure that the memory consumption by the stacks stays within the given bounds.

As no full software testing takes place, it is impossible to derive the memory bounds for the stack through measurements alone.

Thus, StackAnalyzer provides a quick way of proving that the space reserved for the stack is sufficient and no unexpected behavior will occur due to an overlap of the stack with other memory sections.

Timing verification with aiT

To verify that the timing requirements allocated to the FCC are fulfilled, the software is analyzed using aiT WCET Analyzer, which computes a safe upper bound for the execution time.

The calculation of the flight control laws is carried out on an MPC 8349. This processor integrates an e300 core with data and instruction caches and a four-stage pipeline. In order to obtain the desired perfor­mance, both the instruction and the data cache are enabled. Therefore, the execution time of an instruction depends on the history of instructions executed before it. This makes it impossible to determine the WCET by measurements only.

As the analysis is performed on the fully linked executable, the tool cannot always automatically determine the bounds of loops. In such cases, the bounds have to be annotated by the user.

However, as far as the auto-generated code is concerned, very few annotations are actually necessary.

At the moment, only the functions generated for the calculation of values inter­polated from lookup tables need to be annotated. These functions are part of the so-called shared utilities of Embedded Coder. They have canonical names and are always the same if a certain type of a lookup table is contained in the model from which the code is generated. The bound of the loop searching through the indexes of the table is dependent on the function arguments. With an AIS2 annotation, it is possible to define the loop bound depending on these arguments. Thus the anno­tation can be kept universal and does not need to be adapted if the parameters or the width of a lookup table are changed.

Embedded Coder does not provide its own implementation of the math functions like square root or sinus, and therefore calls the library functions of the applicable system. Currently Newlib is used for the calculation of math func­tions, a free C library intended for use on embedded systems. Most math functions consist of a range reduction al­gorithm and an algo­rithm calculating the function value for a limited array. The loop bounds of the range reduction algorithms sometimes cannot be automatically determined and need to be annotated.

Since functions in Newlib do not fulfill the requirements for software that shall be certified, the libraries are currently analyzed and will be replaced by a custom imple­mentation fulfilling certain needs in the future. Then, the WCET of the math functions will have to be con­sid­ered as well. Should the new functions still contain loops that cannot be auto­matic­ally analyzed, the Institute will make use of aiT’s support for anno­tations provided as comments directly in the source code. This way, the infor­mation will have to be main­tained in just one place.

The verdict

With CompCert it is possible to decrease the execution time of the flight control al­go­rithm by a sig­nif­icant amount. The reduction of the execution time can be used for additional func­tion­ality. With the WCET analysis of aiT and the StackAnalyzer it is possible to do a fast verification of the soft­ware. For the given CPU architecture a static analysis is the only practical way to determine a safe upper bound for the execution time, while the stack analysis ensures that the space reserved for the stack pointer is sufficient without a complete software test.”

K. Nürnberger, TU Munich, Institute of Flight System Dynamics

Further information