Exhaustive testing of complex and autonomous systems is intractable and cost prohibitive; however, design analysis techniques such as formal methods and design methodologies, including run-time assurance, could provide supplementary certification evidence early in system design. Incorporating formal methods analysis throughout the system design process provides an offline verification method to identify faults as they are introduced, which may drastically reduce the overall system development cost. In the event of a fault not identified during development, run-time assurance is a proposed online verification methodology to allow unproven autonomous controllers to perform within a predetermined envelope of acceptable behavior. In this research, a six-unit CubeSat attitude control subsystem is used as a challenge problem to evaluate the application of nontraditional verification methodologies, such as formal methods analysis and run-time assurance architectures. Strengths and weaknesses of the verification techniques are exposed in this research to recommend capability expansions for further development.


    Access

    Check access

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Run-Time Assurance and Formal Methods Analysis Nonlinear System Applied to Nonlinear System Control



    Published in:

    Publication date :

    2017-04-01




    Type of media :

    Conference paper , Article (Journal)


    Type of material :

    Electronic Resource


    Language :

    English




    Formal methods for control of nonlinear systems

    Li, Yinan / Liu, Jun | TIBKAT | 2023


    Nonlinear Adaptive Control of Quadrotor UAVs with Run-Time Safety Assurance

    Avram, Remus / Zhang, Xiaodong / Muse, Jonathan A. et al. | AIAA | 2017


    The Role of Formal Methods in Hardware Design Assurance

    Miner, P. / IEEE / AIAA | British Library Conference Proceedings | 2004


    Using formal methods for quality assurance of interlocking systems

    Eriksson, L.H. / Johansson, K. | Tema Archive | 1998


    Using formal methods for quality assurance of interlocking systems

    Eriksson, L.-H. / Johansson, K. / Wessex Institute of Technology | British Library Conference Proceedings | 1998