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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Pampagnin, P., Menis, J.F.: DO254-ED80 for High Performance and High Reliable Electronic Components, Internal Paper, Barco-Siles S.A., Peynier, France (2007)
Bernardo, M., Cimatti, A. (eds.): SFM 2006. LNCS, vol. 3965. Springer, Heidelberg (2006)
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)
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)
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)
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)
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)
Hilton, A.J.: High-Integrity Hardware-Software Codesign, Ph.D. Thesis, The Open University (April 2004)
DO-254, Design Assurance Guidance for Airborne Electronic Hardware, RTCA Inc., Washington, DC (April 19, 2000)
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)
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)
Henson, J.: Equivalence Checking for FPGA Design, White Paper, Mentor Graphics Corp., Wilsonville, Ore. (May 2007)
IEEE Std 1076-2002, Standard VHDL Language Reference Manual, The Institute of Electrical and Electronics Engineers, New York (2002)
Bridgford, B., Carmichael, C., Tseng, C.W.: Single-Event Upset Mitigation Selection Guide, Application Note XAPP987, Xilinx Inc., San Jose, Calif. (March 2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Butka, B., Zalewski, J., Kornecki, A.J. (2009). Issues in Tool Qualification for Safety-Critical Hardware: What Formal Approaches Can and Cannot Do. In: Buth, B., Rabe, G., Seyfarth, T. (eds) Computer Safety, Reliability, and Security. SAFECOMP 2009. Lecture Notes in Computer Science, vol 5775. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04468-7_17
Download citation
DOI: https://doi.org/10.1007/978-3-642-04468-7_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-04467-0
Online ISBN: 978-3-642-04468-7
eBook Packages: Computer ScienceComputer Science (R0)