Applications for data-driven systems are expected to be correct implementations of the system specifications, but developers usually test against a few indicative scenarios to verify them. In the absence of exhaustive testing, errors may occur in real time scenarios, especially when dealing with large data streams from moving objects like multicopters, vehicles, etc. Model checking techniques also lack scalability and completeness. We present a novel approach based on some existing tools which enables a developer to write high level code directly as system specifications and simultaneously be able to prove the correctness of the generated code. We present a fault detection and identification (FDI) software development approach using declarative programming language: PILOTS. The grammar of PILOTS has been updated to enable easier syntax for threshold validation techniques. The failure detection model is described as high level specifications that the generated code has to adhere to. The complete FDI problem is formally specified using Hoare logic and proven correct using an automated proof assistant: Dafny. A case study of rotor failures in a hexacopter has been used to illustrate the approach and visualize the results.


    Zugriff

    Zugriff prüfen

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    Proving the Correctness of Multicopter Rotor Fault Detection and Identification Software


    Beteiligte:


    Erscheinungsdatum :

    03.10.2021


    Format / Umfang :

    1890250 byte





    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Elektronische Ressource


    Sprache :

    Englisch



    MULTICOPTER ONLINE ROTOR FAULT DIAGNOSIS SYSTEM

    KOPSAFTOPOULOS FOTIOS / DUTTA AIRIN / GANDHI FARHAN | Europäisches Patentamt | 2023

    Freier Zugriff

    MULTICOPTER ONLINE ROTOR FAULT DIAGNOSIS SYSTEM

    KOPSAFTOPOULOS FOTIOS / DUTTA AIRIN / GANDHI FARHAN | Europäisches Patentamt | 2025

    Freier Zugriff

    ROTOR AND MULTICOPTER

    MATSUDA YASUTOSHI | Europäisches Patentamt | 2017

    Freier Zugriff

    Proving Correctness of Autocoded Control Software

    Alegre, Fernando / Valenzuela, Rene / Feron, Eric et al. | AIAA | 2007


    Multicopter using coaxial rotor

    LEE SEUNG WOO | Europäisches Patentamt | 2017

    Freier Zugriff