Verification and certification of flight critical software and application-specific integrated circuits (ASICs) is currently a labor-intensive, manual process involving extensive testing, inspections, and process documentation. The complexity of these systems and devices will increase both because increases in cockpit automation and application integration offer important safety benefits and because astonishing improvements in digital computing technology can potentially improve performance and decrease cost. The current approach to verification and certification will be challenged by this increased complexity. In order to reap fully the benefits of these technological advances we must develop new methods for verification and certification of flight critical devices that provide higher degrees of assurance for increasingly complex systems while simultaneously streamlining the verification process. The development of executable formal models may offer higher degrees of assurance, address increased complexity, and streamline certain aspects of the verification process. Increased assurance can be obtained as a result of rigorous, mechanical, mathematically complete checks of consistency and completeness of system requirements as well as proofs of correctness of specific implementations. As vector-based testing becomes increasingly inadequate to assure correctness in the face of exponentially growing state space, formal proofs of correctness can encompass the entire design, demonstrating correctness once and for all.


    Access

    Check access

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Executable formal models for validation and specless verification


    Contributors:
    Greve, D. (author) / Wilding, M. (author)


    Publication date :

    2000-01-01


    Size :

    766785 byte




    Type of media :

    Conference paper


    Type of material :

    Electronic Resource


    Language :

    English



    Executable formal models for validation and specless verification

    Greve, D. / Wilding, M. | Tema Archive | 2000


    Executable Formal Models for Validation and Specless Verification

    Greve, D. / IEEE / AIAA | British Library Conference Proceedings | 2000


    Automatic validation of Simulink/Stateflow models - formal verification of functional requirements

    Bienmueller,T. / Brockmeyer,U. / Sandmann,G. et al. | Automotive engineering | 2005


    Interface Verification Using Executable Reference Models: An Application in the Automotive Infotainment

    Christian, Drabek / Thomas, Pramsohler / Marc, Zeller, Gereon, Weiss | BASE | 2013

    Free access

    Hierarchical Accumulative Validation of Executable Control Specifications

    Mizuno, Hideaki / Farnsworth, Jared / Ueda, Koichi et al. | SAE Technical Papers | 2013