Static Analysis of Autocoded Software forAerospace SystemsEric FeronSchool of Aerospace EngineeringGeorgia Institute of Technology, Atlanta, GA [email protected]: (404) 894-3062Arnaud VenetKestrel Technology LLC4984 El Camino Real #230, Los Altos, CA [email protected]: (650) 967-4408I. OVERVIEW OF OUR APPROACHEmbedded software-based control systems are commonlyconstructed using model-based design environments such asMATLAB/SimulinkTMfrom MathWorks. These environmentsallow the system designer to establish critical properties ensur-ing the reliability of the system (stability, disturbance rejection,etc.) directly at the model level, using a rich mathematicaltoolset. However, the software implementation substantiallytransforms the mathematical model by introducing numerousprogramming artifacts (aggregate data structures, pointers)and altering the numerical representation (platform-dependentfloating/fixed-point arithmetic, and, in the most extreme cases,conversion from continuous-time dynamics to discrete-timedynamics). Verifying that the reliability properties of thesystem are preserved by the implementation is extremelychallenging, yet in many cases critically important. Model-based design environments usually come with an autocoderi.e., a code generation tool that automatically synthesizes animplementation of the embedded controller from the specifi-cation of its model. Autocoders are getting increasingly usedin practical applications for they greatly simplify the imple-mentation process. In aerospace industry however, autocodingis essentially precluded because its properties are consideredto be not adequately trustworthy.Static program analysis tools have recently proven successfulin tackling the certification of embedded software-based con-trol systems. ASTREE [1], developed by P. Cousot’s team inFrance, can automatically verify the consistency of floating-point arithmetic in the electric-command control system ofthe A380, Airbus’ super-jumbo carrier. C Global Surveyor [2],developed by Kestrel Technology LLC, can verify the absenceof pointer manipulation errors in the mission-control softwareof NASA’s Mars Exploration Rovers. However, the scopeof static analysis has been essentially limited to robustnessproperties, i.e., ensuring the absence of runtime errors duringthe execution of the program. Verifying functional propertiesby static analysis for a system to be used in the field requires(1) translating a reliability property of the model into theimplementation setting, using the appropriate data structuresand numerical libraries, and (2) tracking the evolution of thisproperty over all execution paths using abstract interpretationtechniques. This process requires a tight coupling between themodel description and its implementation. While such tightcoupling is rarely achieved in practice, it can exist at leastwhen the implementation is automatically generated from themodel. Autocoders, like Real-Time StudioTMfor SimulinkTM,are increasingly being used in industry for the developmentof embedded control software. This means that static analysistechniques specialized for codes automatically generated fromhigh-level models can be developed to meet market needs.The approach we are investigating consists of translating theformal proof of reliability properties of an embedded logic intoa dedicated static analyzer that automatically carries out thecorresponding proof on the code generated from the model.Whereas today’s commercial (and even known academic)static analyzers for embedded mission- and safety-criticalsoftware are handcrafted, we propose to use our prior researchto construct the dedicated static analyzer automatically. Ulti-mately, the system designer would be provided with a fullyautomated engine that performs verification of the generatedcode without requiring any additional information other thanthe high-level model specification.II. CHALLENGESThere are two major challenges in developing a tool for theautomated verification of reliability properties of embeddedcontrol software automatically generated from a high-levelmodel:1) How do we translate a property of the high-level modelinto a property of the code generated from that model?What are the features of the autocoder we must knowto effectively build this translator?2) How do we specify the basic components of the staticanalyzer required to verify the desired property? Howdo we specialize the analyzer to the code generated bya given autocoder?We discuss these challenges in the following subsections.A. Property TranslatorThe autocoder of the model-based design environment gener-ates code from the model in a predictable way. Therefore, weexpect to be able to map a property of the model’s variablesinto a property of the data structures used in the model’s im-plementation. Commercial model-based design environmentsoffer rich libraries of basic components for building systemsand the properties of interest may greatly vary depending onthe nature of the system designed. The family of systemswe have been investigating is that of closed-loop dynamicalsystems, represented on the one hand by a family of differ-ential equations that capture the system’s physics, and on theother hand the closed-loop control algorithm and its associatedcode. The functional properties we are interested in includeclosed-loop systems stability, closed-loop system performance(eg tracking performance), and reachability analyses. We arecurrently interested in describing how to map that property tothe implementation by conducting an extensive study of thecode generated from a benchmark of systems in that family.B. Static Analysis Specification FrameworkChecking the transposed property of the model on the codemay require a specific analysis algorithm that takes intoaccount the underlying computational model (floating/fixed-point) and the nature of the reliability property (linear orellipsoidal invariants). Moreover, the code generated by themodel-based design environment may use programming lan-guage constructs (like pointers or union types in C) thatpose a difficulty for the static analyzer. These constructsmay require dedicated analysis algorithms (pointer analysis,type analysis) specially tailored for the particular structureof code produced by the autocoder. These static analyzersare strongly specialized toward the family of models andproperties considered. This does not require rewriting theanalyses from scratch