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

被引：4

作者：

Chhaya, Bharvi ^{[1
]}

Jafer, Shafagh ^{[1
]}

Durak, Umut ^{[2
]}

机构：

[1] Embry Riddle Aeronaut Univ, Dept Elect Comp Software & Syst Engn, Daytona Beach, FL 32114 USA

[2] German Aerosp Ctr DLR, Inst Flight Syst, D-38108 Braunschweig, Germany

来源：

AEROSPACE | 2018年 / 5卷 / 01期

关键词：

DSL; ASDL; formal methods; verification; statecharts;

D O I：

10.3390/aerospace5010010

中图分类号：

V [航空、航天];

学科分类号：

08 ; 0825 ;

摘要：

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.

引用

页数：12