Generating customized verifiers for automatically generated code

ABSTRACT

Program verification using Hoare-style techniques requires many logical annotations. We have previously developed a generic annotation inference algorithm that weaves in all annotations required to certify safety properties for automatically generated code. It uses patterns to capture generator- and property-specific code idioms and property-specific meta-program fragments to construct the annotations. The algorithm is customized by specifying the code patterns and integrating them with the meta-program fragments for annotation construction. However, this is difficult since it involves tedious and error-prone low-level term manipulations.

Here, we describe an approach that automates this customization task using generative techniques. It uses a small annotation schema compiler that takes a collection of high-level declarative annotation schemas tailored towards a specific code generator and safety property, and generates all customized analysis functions and glue code required for interfacing with the generic algorithm core, thus effectively creating a customized annotation inference algorithm. The compiler raises the level of abstraction and simplifies schema development and maintenance. It also takes care of some more routine aspects of formulating patterns and schemas, in particular handling of irrelevant program fragments and irrelevant variance in the program structure, which reduces the size, complexity, and number of different patterns and annotation schemas required. The improvements described here make it easier and faster to customize the system to a new safety property or a new generator, and we demonstrate this by customizing it to certify frame safety of space flight navigation code that was automatically generated from Simulink models by MathWorks' Real-Time Workshop.

REFERENCES

• 1: www.mathworks.com/products/rtw/.
• 2: www.mathworks.com/products/polyspace/.
• 3: XML Path Language (XPath) Version 1.0, 1999. www.w3.org/TR/xpath.
• 4: Michal Antkiewicz , Thiago Tonelli Bartolomei , Krzysztof Czarnecki, Automatic extraction of framework-specific models from framework-based application code, Proceedings of the twenty-second IEEE/ACM international conference on Automated software engineering, November 05-09, 2007, Atlanta, Georgia, USA [doi>10.1145/1321631.1321664]
• 5: Nurlida Basir , Ewen Denney , Bernd Fischer, Constructing a Safety Case for Automatically Generated Code from Formal Program Verification Information, Proceedings of the 27th international conference on Computer Safety, Reliability, and Security, September 22-25, 2008, Newcastle upon Tyne, UK [doi>10.1007/978-3-540-87698-4_22]
• 6: J. Brunel et al. A Foundation for Flow-Based Program Matching Using Temporal Logic and Model Checking. Technical Report 08/2/INFO, Ecole des Mines de Nantes, 2008.
• 7: P. Cousot et al. The Astreé analyzer. In ESOP'05, LNCS 3444, pp. 21---30. Springer, 2005.
• 8: E. Denney and B. Fischer. Correctness of source-level safety policies. In FM'03, LNCS 2805, pp. 894--913. Springer, 2003.
• 9: E. Denney and B. Fischer. Certifiable program generation. In GPCE'05, LNCS 3676, pp. 17--28. Springer, 2005.
• 10: Ewen Denney , Bernd Fischer, A generic annotation inference algorithm for the safety certification of automatically generated code, Proceedings of the 5th international conference on Generative programming and component engineering, October 22-26, 2006, Portland, Oregon, USA [doi>10.1145/1173706.1173725]
• 11: Nachum Dershowitz , Zohar Manna, Inference rules for program annotation, Proceedings of the 3rd international conference on Software engineering, p.158-167, May 10-12, 1978, Atlanta, Georgia, United States
• 12: Michael D. Ernst , Jake Cockrell , William G. Griswold , David Notkin, Dynamically Discovering Likely Program Invariants to Support Program Evolution, IEEE Transactions on Software Engineering, v.27 n.2, p.99-123, February 2001 [doi>10.1109/32.908957]
• 13: Bernd Fischer , Johann Schumann, AutoBayes: a system for generating data analysis programs from statistical models, Journal of Functional Programming, v.13 n.3, p.483-508, May 2003 [doi>10.1017/S0956796802004562]
• 14: Cormac Flanagan , K. Rustan M. Leino, Houdini, an Annotation Assistant for ESC/Java, Proceedings of the International Symposium of Formal Methods Europe on Formal Methods for Increasing Software Productivity, p.500-517, March 12-16, 2001
• 15: M. J. Harrold and G. Rothermel. Syntax-directed construction of program dependence graphs. Technical Report OSU-CISRC-5/96-TR32, The Ohio State University, 1996.
• 16: L. Kovács and T. Jebelean. Finding Polynomial Invariants for Imperative Loops in the Theorema System. In Proc. IJCAR'06 Workshop Verify'06, pp. 52--67, 2006.
• 17: O. Lee, H. Yang, and K. Yi. Automatic Verification of Pointer Programs Using Grammar-Based Shape Analysis. In ESOP'05, LNCS 3444, pp. 124--240. Springer, 2005.
• 18: Michael Lowry , Thomas Pressburger , Grigore Rosu, Certifying Domain-Specific Policies, Proceedings of the 16th IEEE international conference on Automated software engineering, p.81, November 26-29, 2001
• 19: Clint Morgan , Kris De Volder , Eric Wohlstadter, A static aspect language for checking design rules, Proceedings of the 6th international conference on Aspect-oriented software development, March 12-16, 2007, Vancouver, British Columbia, Canada [doi>10.1145/1218563.1218571]
• 20: J. W. Nimmer and M. D. Ernst. Static verification of dynamically detected invariants: Integrating Daikon and ESC/Java. In First Workshop on Runtime Verification, Elec. Notes in Theoretical Computer Science, 55(2). Elsevier, 2001.
• 21: Stephan Schulz, E - a brainiac theorem prover, AI Communications, v.15 n.2, p.111-126, September 2002
• 22: Geoff Sutcliffe , Darryl Seyfang, Smart Selective Competition Parallelism ATP, Proceedings of the Twelfth International Florida Artificial Intelligence Research Society Conference, p.341-345, May 01-05, 1999
• 23: D. A. Vallado. Fundamentals of Astrodynamics and Applications. Space Technology Library. Microcosm Press and Kluwer Academic Publishers, second edition, 2001.
• 24: Ben Wegbreit, The synthesis of loop predicates, Communications of the ACM, v.17 n.2, p.102-113, Feb. 1974 [doi>10.1145/360827.360850]
• 25: Christoph Weidenbach , Uwe Brahm , Thomas Hillenbrand , Enno Keen , Christian Theobald , Dalibor Topic, S PASS Version 2.0, Proceedings of the 18th International Conference on Automated Deduction, p.275-279, July 27-30, 2002
• 26: Michael W. Whalen , Johann Schumann , Bernd Fischer, Synthesizing Certified Code, Proceedings of the International Symposium of Formal Methods Europe on Formal Methods - Getting IT Right, p.431-450, July 22-24, 2002
• 27: Jon Whittle , Johann Schumann, Automating the implementation of Kalman filter algorithms, ACM Transactions on Mathematical Software (TOMS), v.30 n.4, p.434-453, December 2004 [doi>10.1145/1039813.1039816]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

Additional Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.2 Automatic Programming
      I.2.3 Deduction and Theorem Proving

General Terms:
Algorithms, Verification

Keywords:
automated code generation, automated theorem proving, hoare logic, logical annotations, program verification, software certification