SYSE 505: System Safety and Certification Module 7: Formal Methods for Safety Assessment Project: Unmanned Aerial System Operation with State-Machine Modeling   The state machine model in the below figure considers four in-flight states of a small unmanned aerial system (sUAS)

SYSE 505: System Safety and Certification

Module 7: Formal Methods for Safety Assessment

Project: Unmanned Aerial System Operation with State-Machine Modeling

The state machine model in the below figure considers four in-flight states of a small unmanned aerial system (sUAS). The model uses transition probabilities and Linear Temporal Logic (LTL) for the transition from one state to another.

• Flight Path, where the sUAS is following the initial calculated flight path, while also monitoring the environment for external objects that could be located on, or intersecting, the flight path.
• Adjust Path, in which the sUAS is calculating a revised flight path when an object is detected on the initial flight path.
• Corrected Path, which is the sUAS path determined to avoid the risk of collision with the detected objects.
• Collision Path, when the sUAS is not able to avoid the total failure resulted from a collision with an object in the external environment; collision could occur in the case of object non-detection, failed path adjustment, or improper revised (corrected) path.

1. Derive the invariant(s) for sUAS collision with an external object. Write each invariant(s) such that, if not violated, it will only evaluate to FALSE during system execution. An invariant is a statement that does not change its truth evaluation during system execution. The transitions between the states of the system include probabilities of failure (which are the probabilities of object non-detection) Pfp, Pap, and Pcp, as well as LTL statements that you need to consider when writing the invariant.
2. Using TRUE and FALSE evaluations only, derive the execution of the state machine model, and highlight the unsafe cases that violate the invariant(s) identified (i.e., highlight the state machine cases that result in a TRUE evaluation of the invariant(s). Use the below table as example. Add as many rows and columns as necessary to capture all state transitions (all state machine cases).

For example, the first row (which is given) represents the case in which the sUAS is on the ground (non-operational). There is no object (actually, it is not important if there is any object since the sUAS is non-operational). Since the sUAS is non-operational, the object detection system is not working (not detecting objects) and the sUAS is not on either of the FlightPath, AdjustedPath, or CorrectedPath. So, all of those events and states evaluate to FALSE. Obviously, there is no collision (since again sUAS is non-operational) so the Collision cell evaluates to FALSE as well.