Formal Verification
Last update: December-14th, 2023.
This page aims to support the DAES submission entitled Applying Formal Methods to Build a Safe Continuous-Control Architecture for an Unmanned Aerial Vehicle.
Preprints url: https://doi.org/10.21203/rs.3.rs-3668418/v1
The conducted study used the following formal verification & monitoring tools:
The following models/algorithms were used as input for the conducted analysis:
- AADL model of the proposed control architecture
- LQR continuous-control algorithm in C language (input for ESBMC)
- TA model generated from the AADL model (input for UPPAAL)