HK, Jnanamurthy

Henskens, Frans

Paul, David

2016

Nowadays, Model-Driven Architectures (MDAs) are gaining more popularity because they offer an increase in productivity by improving compatibility between systems (reuse of standardized models), simplifying the process of design (models of recurring design patterns in the application domain), and supporting communication between individuals and different teams working on the system. Development of MDA software systems requires high integrity, with verification before deployment in critical applications. Verifying different properties of the system at the beginning of the development is highly desirable as the first line of defense against design faults. In this paper, we have modeled an Automated Air Traffic Control System (AATCS) using MDA and converted into the Process Meta Language (PROMELA) model, which is used by Simple Promela Interpreter (SPIN) model checker for verification. The entities in our model are Airplane, Ground Station, SWIM data and Data store. The communication between entities is modeled as transitions. The model is checked for conformance with its specifications to detect flaws using formal techniques to improve reliability and quality.

Proceedings of the 2nd International Conference on Contemporary Computing and Informatics (IC3I), p. 882-887

9781509052554

9781509052561

https://hdl.handle.net/1959.11/20173

en

Institute of Electrical and Electronics Engineers (IEEE)

Verification of Interactive Automated Air Traffic Control System in a Model Driven Approach

Conference Publication

Publication