Advertisement

Issues in Tool Qualification for Safety-Critical Hardware: What Formal Approaches Can and Cannot Do

  • Brian Butka
  • Janusz Zalewski
  • Andrew J. Kornecki
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5775)

Abstract

Technology has improved to the point that system designers have the ability to trade-off implementing complex functions in either hardware or software. However, clear distinctions exist in the design tools. This paper examines what is unique to hardware design, areas where formal methods can be applied to advantage in hardware design and how errors can exist in the hardware even if formal methods are used to prove the design is correct.

Keywords

Tool Qualification HDL PLD Hardware Design Safety-Critical Systems Formal Methods 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Pampagnin, P., Menis, J.F.: DO254-ED80 for High Performance and High Reliable Electronic Components, Internal Paper, Barco-Siles S.A., Peynier, France (2007)Google Scholar
  2. 2.
    Bernardo, M., Cimatti, A. (eds.): SFM 2006. LNCS, vol. 3965. Springer, Heidelberg (2006)Google Scholar
  3. 3.
    Kern, C., Greenstreet, M.R.: Formal Verification in Hardware Design: A Survey. ACM Trans. on Design Automation of Electronic Systems 4(2), 123–193 (1999)CrossRefGoogle Scholar
  4. 4.
    Turner, K.J., He, J.: Formally-based Design Evaluation. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol. 2144, pp. 104–109. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  5. 5.
    Aljer, A., Devienne, P.: Co-design and Refinement for Safety Critical Systems. In: Proc. DFT 2004, 19th IEEE International Symposium on Defect and Fault Tolerance in VLSI Systems, pp. 78–86. IEEE, Los Alamitos (2004)CrossRefGoogle Scholar
  6. 6.
    Nehme, C., Lundqvist, K.: A Tool for Translating VHDL to Finite State Machines. In: Proc. DACS 2003, 22nd Digital Avionics Systems Conference, October 12-16, vol. 1, pp. 3.B.6-1-7 (2003)Google Scholar
  7. 7.
    Dajani-Brown, S., Cofer, D., Bouali, A.: Formal Verification of an Avionics Sensor Voter Using SCADE. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS 2004 and FTRTFT 2004. LNCS, vol. 3253, pp. 5–20. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  8. 8.
    Hilton, A.J.: High-Integrity Hardware-Software Codesign, Ph.D. Thesis, The Open University (April 2004)Google Scholar
  9. 9.
    DO-254, Design Assurance Guidance for Airborne Electronic Hardware, RTCA Inc., Washington, DC (April 19, 2000)Google Scholar
  10. 10.
    Dellacherie, S., Burgaud, L., di Crescenzo, P.: imPROVE–HDL: A DO-254 Formal Property Checker Used for Design and Verification of Avionics Protocol Controllers. In: Proc. DACS 2003, 22nd Digital Avionics Systems Conference, Indianapolis, Ind., October 12-16, vol. 1, pp. 1.A.1-1.1-8 (2003)Google Scholar
  11. 11.
    Karlsson, K., Forsberg, H.: Emerging Verification Methods for Complex Hardware in Avionics. In: Proc. DASC 2005, 24th Digital Avionics Systems Conference, October 30 -November 3, vol. 1, pp. 6.B.1 - 61-12 (2005)Google Scholar
  12. 12.
    Henson, J.: Equivalence Checking for FPGA Design, White Paper, Mentor Graphics Corp., Wilsonville, Ore. (May 2007)Google Scholar
  13. 13.
    IEEE Std 1076-2002, Standard VHDL Language Reference Manual, The Institute of Electrical and Electronics Engineers, New York (2002)Google Scholar
  14. 14.
    Bridgford, B., Carmichael, C., Tseng, C.W.: Single-Event Upset Mitigation Selection Guide, Application Note XAPP987, Xilinx Inc., San Jose, Calif. (March 2008)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Brian Butka
    • 1
  • Janusz Zalewski
    • 2
  • Andrew J. Kornecki
    • 3
  1. 1.Electrical EngineeringEmbry Riddle Aeronautical Univ.Daytona BeachUSA
  2. 2.Computer ScienceFlorida Gulf Coast UniversityFort MeyersUSA
  3. 3.Computer&Software EngineeringEmbry-Riddle Aeronautical Univ.Daytona BeachUSA

Personalised recommendations