Advertisement

A Pragmatic View of Formal Methods: the Hi-Lite Project

  • Robert Dewar
Conference paper

Abstract

Formal methods can be applied in a variety of different modes. Even if the notion of proving an entire program correct is of limited applicability, we can still achieve more modest goals, such as proving specific properties of programs, and in fact there are existing examples where such approaches have been successful. The inability of formal methods to carry 100% of the burden means that the overall development process must rely on a combination of tools and techniques spanning the range from formal proof to testing. We thus need tools, languages, and development environments that allow easy integration of these various approaches. The Hi-Lite project aims to meet this need.

Keywords

Formal Method Formal Proof Formal Verification Buffer Overflow Entire Program 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. AdaCore (2009) The Tokeneer project. http://www.adacore.com/home/products/sparkpro/tokeneer/?gclid=CK_x243uk6QCFYs65QodHVGXXQ. Accessed 11 October 2010
  2. Alves-Foss J, Harrison W, Oman P, Taylor C (2007) The MILS architecture for high assurance embedded systems. Int J Embed Syst 2: 239-247CrossRefGoogle Scholar
  3. ATSB (2007) Australian Transport Safety Bureau, In-flight upset event, 240 km north-west of Perth, WA, Boeing Company 777-200, 9 M-MRG, 1 August 2005, Report No 200503722Google Scholar
  4. Barnes J (2003) High integrity software: the SPARK approach to safety and security. Addison WesleyGoogle Scholar
  5. Beck K et al (2001) Manifesto for agile software development. http://agilemanifesto.org/. Accessed 11 October 2010
  6. Bessey A, Block K, Chelf et al (2010) A few billion lines of code later: using static analysis to find bugs in the real world. Commun ACM 53(2):66-75. http://cacm.acm.org/magazines/2010/2/69354-a-few-billion-lines-of-code-later/fulltext. Accessed 11 October 2010
  7. Chapman R (2000) Industrial experience with SPARK. ACM SIGAda Ada Letters XX(4)64-68CrossRefGoogle Scholar
  8. Chess B, West J (2007) Static analysis as part of the code review process. In: Chess B, West J Secure programming with static analysis. Addison-WesleyGoogle Scholar
  9. Chilenski J (2002), Software development under DO-178B, Open Group http://www.opengroup.org/rtforum/jan2002/slides/safety-critical/chilenski.pdf. Accessed 11 October 2010
  10. Ernst M (2003) Static and dynamic analysis: synergy and duality. In: WODA 2003: ICSE Workshop on Dynamic Analysis. Portland, ORGoogle Scholar
  11. FAA (2008) Department of Transportation, FAA. Special conditions: Boeing model 787-8 airplane; systems and data networks security – isolation or protection from unauthorized passenger domain systems access. Federal RegisterGoogle Scholar
  12. Fisher G (2007) When, why and how to leverage source code analysis tools. http://www.klocwork.com/resources/white-paper/static-analysis-when-why-how. Accessed 11 October 2010 Ganssle J (2010) A guide to code inspections. http://www.ganssle.com/inspections.pdf. Accessed 11 October 2010
  13. Hackett B, Das M, Wang D, Yang Z (2006) Modular checking for buffer overflows in the large. In: ICSE ’06: Proc 28th Int Conf on Softw Eng, New York. ACMGoogle Scholar
  14. ISO (1995) Ada reference manual ISO/IEC 8652:1995 with Technical Corrigendum 1. http://www.adaic.org/standards/95lrm/html/RM-TTL.html. Accessed 11 October 2010
  15. Liskov B, Wing J (2001) Behavioral subtyping using invariants and constraints. In: Formal methods for distributed processing. Cambridge University PressGoogle Scholar
  16. MISRA (2004) MISRA-C: Guidelines for the use of the C language in critical systems. http://www.misra-c.com/. Accessed 11 October 2010
  17. Moy M, Wallenburg A (2010), Tokeneer: beyond formal program verification. Embedded Real Time Software and Systems (ERTS22010), Toulouse, FranceGoogle Scholar
  18. Moy Y, Bjorner N, Sielaff D (2009) Modular bug-finding for integer overflows in the large. http://research.microsoft.com/apps/pubs/?id=80722. Accessed 11 October 2010
  19. RTCA/EUROCAE (1992), RTCA SC-167/EUROCAE WG-12. RTCA/DO-178B. Software considerations in airborne systems and equipment certificationGoogle Scholar
  20. Souyris J, Wiels V et al (2009), Formal verification of avionics software products. FM 2009. LNCS 5850. SpringerGoogle Scholar
  21. Spivey J (2001) The Z notation: a reference manual. http://spivey.oriel.ox.ac.uk/∼mike/zrm/. Accessed 11 October 2010
  22. Taft T, Dewar R (2009) Making static analysis a part of code review. Embedded Computing Design. http://embedded-computing.com/making-static-analysis-part-code-review. Accessed 11 October 2010

Copyright information

© Springer-Verlag London Limited 2011

Authors and Affiliations

  • Robert Dewar
    • 1
  1. 1.AdaCore and New York UniversityNew YorkUSA

Personalised recommendations