Today's airplane consists of a big network linking embedded controllers to sensors/actuators and communications equipment onboard. Efforts made in recent years to simplify network wirings have resulted in significant reductions in the aircraft weight and labor required to run wiring harnesses. This has often come out at the cost of a more complex data bus architecture (bi-directional protocol instead of unidirectional protocol). As DO-178B is a requirement for certifiable avionics SW design, DO-254 is a set of design guidelines for airborne HW electronics. DO254 considers the use of formal methods and requirements traceability when developing HW to support safety-critical (Level A or B) functions. This article presents a static formal approach that may be used, in combination with requirements traceability features, to apply formal methods in the design and verification of HW controllers to support such protocols as ARINC 429, ARINC 629, MIL-STD-1553B, etc. Model simulation is today's standard practice in verifying HW electronics. A major drawback in simulation is the lack of exhaustive checking, since simulation results are only a function of the testbench scenario defined by the designers. For example, using simulation one cannot guarantee such system behaviors as "the controller shall always respond to a request," "acknowledge shall always arrive no later than N cycles," "the controller shall not drop any data," "the controller shall not lock up," etc. improve-HDL is a formal property checker that complements simulation in performing exhaustive debugging of VHDL/Verilog register-transfer-level HW models of complex avionics protocol controllers without the need to create testbenches. Reqtify is used to track requirements throughout the verification process and to produce coverage reports. Using improve-HDL coupled wit


    Access

    Check access

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Improve - HDL - a DO-254 formal property checker used for design and verification of avionics protocol controllers


    Contributors:


    Publication date :

    2003-01-01


    Size :

    525830 byte




    Type of media :

    Conference paper


    Type of material :

    Electronic Resource


    Language :

    English






    Model checker for railway signalling communication protocol

    Hwang, J.-G. / Jo, H.-J. / Lee, J. H. | British Library Conference Proceedings | 2006


    Formal Verification of the LDACS MAKE Protocol

    Mäurer, Nils / Grundner-Culemann, Sophia | German Aerospace Center (DLR) | 2022

    Free access