Abstract
Arguments for and against the deployment of formal methods in system design are rarely supported by evidence derived from experiments that compare a particular formal approach with conventional methods [2]. We illustrate an approach to the use of formal methods for secure code synthesis in safety-critical Avionics applications. The technique makes use of code components and uses sound introduction rules for the components to ensure constraints on their use are enforced. The approach we describe is the subject of a controlled experiment where it is running in parallel with the conventional approach. We describe the experiment and report some preliminary findings.
Partially supported by the EU ESSI programme projects, no. 23743, Proof by Construct using Formal Methods and no.27825, Implementing Design Execution using Ada.
Lucas Aerospace is a TRW company.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Adelard. ASCAD-Adelard Safety Case Development Manual. Adelard, 1998. ISBN 0 9533771 0 5.
Geoff Barrett. Formal methods applied to a floating-point number systems. IEEE Transactions on Software Engineering, 15(5):611–621, May 1989.
B. A. Carre, D. L. Clutterbuck, C. W. Debney, and I. M. O'Neill. SPADE-the thampton Program Analysis and Development Environment. In Software Engineering Environments, pages 129–134. Peter Peregrinus, 1986.
P. Caseley, C. O'Halloran, and A. Smith. Explaining code with pictures-a case study. Technical Report DERA/CIS/CIS3/TR990083/1.0 (DRAFT), DERA, 1997.
S. Easterbrook, R Lutz, R. Covington, J. Kelly, Y. Ampo, and D. Hamilton. Experiences using lightweight formal methods for requirements modeling. IEEE Transactions on Software Engineering, 24(1), Jan 1998.
E.M. Mayger and M.P. Fourman. Integration of formal methods with system design. In A. Halaas and P.B. Denyer, editors, International Conference on Very Large Scale Integration, pages 59–70, Edinburgh, Scotland, August 1991. IFIP Transactions, North-Holland.
M. P. Fourman. Formal System Design, chapter 5, pages 191–236. North-Holland, 1990.
P. Garbett, J. Parkes, M. Shackleton, and S. Anderson. A case study in innovative process improvement: Code synthesis from formal specifications. In Avionics 98, 1998.
R. Lutz. Targeting safety-related errors during software requirements analysis. The Journal of Systems and Software, 34:223–230, Sept 1996.
Robin Milner, Mads Tofte, and Robert Harper. The Definition of Standard ML. MIT Press, Cambridge, MA, 1989.
M.P. Fourman and E.M. Mayger. Formally Based System Design-Interactive hardware scheduling. In G. Musgrave and U. Lauther, editors, Very Large Scale Integration, pages 101–112, Munich, Federal Republic of Germany, August 1989. IFIP TC 10/WG10.5 International Conference, North-Holland.
I.M. O'Neill, D.L. Clutterbuck, P.F. Farrow, P.G. Summers, and W.C. Dolman. The formal verification of safety critical assembly code. In Safety of Computer Control Systems, pages 115–120. Pergammon Press, 1988.
L. C. Paulson. Isabelle: A generic theorem prover. Lecture Notes in Computer Science, 828:xvii + 321, 1994.
Requirements and Technical Concepts for Aviation. Software Considerations in Airborne Systems and Equipment Certification, Dec 1992. (document RTCA SC167/DO-178B).
S. Finn, M.P. Fourman, and G. Musgrave. Interactive synthesis in HOL-abstract. In M. Archer, J.J. Joyce, K.N. Levitt, and P.J. Windley, editors, International Workshop on Higher Order Logic Theorem Proving and its Applications, Davis, California, August 1991. IEEE Computer Society, ACM SIGDA, IEEE Computer Society Press.
S. Finn, M.P. Fourman, M.D. Francis, and B. Harris. Formal system design-interactive synthesis based on computer assisted formal reasoning. In Luc J. M. Claesen, editor, Applied Formal Methods For Correct VLSI Design, volume 1, pages 97–110. IMEC-IFIP, Elsevier Science Publishers, 1989.
H. Saiedan and L. M. Mc Clanahan. Frameworks for quality software process: SEI capability maturity model. Software Quality Journal, 5(1):1, 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Garbett, P., Parkes, J.P., Shackleton, M., Anderson, S. (1999). Secure synthesis of code: a process improvement experiment. In: Wing, J.M., Woodcock, J., Davies, J. (eds) FM’99 — Formal Methods. FM 1999. Lecture Notes in Computer Science, vol 1709. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48118-4_46
Download citation
DOI: https://doi.org/10.1007/3-540-48118-4_46
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66588-5
Online ISBN: 978-3-540-48118-8
eBook Packages: Springer Book Archive