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

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.