Formal Verification of Simulation Scenarios in Aviation Scenario Definition Language (ASDL)

Abstract

Formal methods offer well-defined means for mathematical verification of the functional specifications of software systems. For model-based engineering, model checking is a verification technique that explores all possible system states. The Aviation Scenario Definition Language is a domain-specific language designed based on a scenario development process from a model-driven engineering perspective. It aims at providing a well-structured definition language to specify departure, en route, re-route, and landing scenarios. This paper uses statecharts and a model checker for the verification of each scenario generated and uses examples to demonstrate conformance to the rules established in the statecharts to verify the logic of all future scenarios.

Keywords

• DSL
• ASDL
• formal methods
• verification
• statecharts