Safety analysis of Hawk In Flight monitor

ABSTRACT

The development of a military safety critical system has many facets, one of which is the collecting of evidence that can be used to assist the production of the safety case necessary for certification of a system into military use. Within the certification process, static analysis is required by the UK Ministry of Defence to provide evidence of a systems integrity and fitness for purpose. In this paper we describe how we have extended the approach of static analysis to gain evidence of the dynamic integrity of a system. This work, based on the abstract interpretation of variable values into sets of ranges of values, has resulted in the development of a software tool, called the Exception Analyser. This tool can investigate the potential for code, written in C, C++ and Ada, to raise run time exceptions and then derive the system constraints which would prevent these exceptions from occurring. We outline the foundation behind our approach and present the results of a case study into the successful application of the tool on a safety critical military project.

REFERENCES

• Andf99: ANDF TenDRA Software. web site: http://alph.dra.hmg.gb/TenDRA/index.html, 1999 .
• Bar97: Barnes J. High Integrity Ada: The SPARK Approach. Addison-Wesley Longman, 1997.
• Bou93: François Bourdoncle, Abstract debugging of higher-order imperative languages, Proceedings of the ACM SIGPLAN 1993 conference on Programming language design and implementation, p.46-55, June 21-25, 1993, Albuquerque, New Mexico, United States
• Buc98: Buckle G. Static Analysis of Safety Critical Software (Techniques, Tools and Experiences). Proceedings of the Sixth Safety-Critical Systems Symposium, Birmingham UK, 1998.
• CG90: Carre B, and Garnsworthy J. Experiences with SPARK and its support tool, the SPARK Examiner. Ada UK Conference, October 1990.
• CC77: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• Cur98: Currie I. Rationale Behind the Prototype C Analyser. Defence Evaluation Research Agency, Internal Report, DERA/CIS/CIS3/CR97469/1 .O, January 1998.
• DDC99: DDC-I. Safety Critical Real- World Sofmare Development. web site: http://www.ddci.com, 1999.
• GH98: Granville R, and Harrison K. Use of Static Code Analysis to Support the Safety CertiJication of Airborne Software. Proceedings of the Sixth Safety-Critical Systems Symposium, Birmingham UK, 1998.
• IPL99: IPL. Eveleigh House, Grove Street, Bath. http://www.iplbath.com/oOOO.htm. 1999
• JN95: Neil D. Jones , Flemming Nielson, Abstract interpretation: a semantics-based tool for program analysis, Handbook of logic in computer science (vol. 4): semantic modelling, Oxford University Press, Oxford, 1995
• Lev95: Nancy G. Leveson, Safeware: system safety and computers, ACM Press, New York, NY, 1995
• Ldr99: Liverpool Data Research Associates Ltd. 131 Mount Pleasant, Liverpool. http://www.ldra.coml. 1999
• MIS98: The Motor Industry Software Reliability Association Guidelines for the use of the C Language in Vechicle Based Software MISRA, Nuneaton, Warwickshire, UK, April 1998.
• MOD91: Ministry of Defence, Directorate of Standardisation, Kentigern House, 65 Brown Street, Glasgow G2 8EX. Interim Defence Standard 00-55. The procurement of safety critical software in Defence equipment, April 1991.
• Moo66: Moore R.E. Interval Analysis Prentice-Hall, Englewood Cliffs, NJ, 1966
• OSF91: OSF. ANDF; application portability and open systems. Technical report, Open Software Foundation, 11 Cambridge Center, Cambridge, MA 02142, USA, 1991.
• Ost81: Osterweil L. Using Data Flow Tools in Software Engineering in: Program Flow Analysis: Theory and Applications, Edited by S.S.Muchnick and N.D.Jones, Prentice-Hall Software Series, 1981.
• Pal96: Palmer S. MALPAS Executive Overview. TACS/99006/37, TA Constancy Services Limited, UK, 1996.
• QAC99: QAC. Programming Research Ltd., Glenbrook House, Hersham, Surrey. http:Nwww.prqa.co.uWindex.htm, 1999
• RTC92: RTCA-DO- 178B. Software considerations in airborne systems and equipment certijcation, December 1992.
• WCC95: Wichmann B.A, Canning A.A, Clutterbuck D.L, Winsborrow L.A, Ward N.J, and Marsh D.W.R. Industrial Perspective on Static Analysis. Software Engineering Journal, March 1995.

INDEX TERMS

Primary Classification:
  J. Computer Applications
  J.1 ADMINISTRATIVE DATA PROCESSING
      Subjects: Military

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING

  K. Computing Milieux
  K.6 MANAGEMENT OF COMPUTING AND INFORMATION SYSTEMS
      K.6.3 Software Management
          Subjects: Software development

General Terms:
Design, Performance, Reliability, Theory