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


    Zugriff

    Zugriff prüfen

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

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


    Beteiligte:
    Dellacherie, S. (Autor:in) / Burgaud, L. (Autor:in) / di Crescenzo, P. (Autor:in)


    Erscheinungsdatum :

    2003-01-01


    Format / Umfang :

    525830 byte




    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Elektronische Ressource


    Sprache :

    Englisch





    Formal Verification Method for Configuration of Integrated Modular Avionics System Using MARTE

    Lisong Wang / Miaofang Chen / Jun Hu | DOAJ | 2018

    Freier Zugriff

    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 | Deutsches Zentrum für Luft- und Raumfahrt (DLR) | 2022

    Freier Zugriff