Safety is an emergent property: Illustrating functional resonance in Air Traffic Management with formal verification

•Extension to Functional Resonance Analysis Method with formal verification tool SPIN.•Approach of automatically demonstrating functional resonance by generating emergent instantiations.•Countermeasure development to damp the undesired resonance, and check of mitigation effectiveness.•Application to a developing Minimum-Safe-Altitude-Warning-in-Air-Traffic-Management (MSAW-in-ATM) system.