Formal Specification and Verification of a Coordination Protocol for an Automated Air Traffic Control System
We detail all of the facets of adapting classical model checking to a real aerospace system, in- cluding deriving the formal model and a set of specifications from natural language descriptions. To ensure the model checking results are meaningful, we have to ensure that both the model and specifications correctly …