Statistical Model Checking of Aircraft Digital Twins for Safety Verification

Digital Twins (DTs) are emerging as powerful tools to represent physical systems in virtual environments, facilitating the design, development, and testing of physical and cyber-physical systems. This is especially true in aviation, where DTs are used to represent an aircraft virtually, assisting in the validation, verification, and maintenance of aircraft. The use of DTs for aviation is still in its early stages, however, and formal techniques to verify safety properties of an aircraft have not yet been applied to DTs. This work proposes leveraging Statistical Model Checking (SMC) to verify safety properties at the intersection of the hardware and software components, focusing on potential failure states that may be missed through traditional verification methods. For example, the failure of a physical sensor must not cause erroneous behavior in the autopilot. Verifying safety in states where hardware and software connect is inherently challenging, and DTs provide an opportunity to tackle these problems. The use of SMC, as opposed to other types of Model Checking, can handle the significant state space of a DT, making it a viable candidate for this task. A framework is defined that translates a DT of an aircraft into the UPPAAL SMC model checker to determine if such failures exist. This framework may be applied in the verification phase of an aircraft program to augment traditional verification techniques and assist in certification.