Formalizing Air Traffic Control System Using Agent-based Mobile Petri Nets

Agent-based Mobile Petri Net (MPN) is an emerging variant of classical Petri Nets which allows graphical representation of system to be developed. In addition agent-based MPN integrates mobile agent technology for modeling concurrency and mobility. Unified Modeling Language (UML) has become a defacto standard for modeling any real world system. Unlike UML models, MPN are based on mathematical semantics and can be verified for presence of errors and inconsistencies. This paper demonstrates the strength of agent-based MPN to model and verify Air Traffic Control (ATC) which is a complex, highly distributed and safety critical system. Firstly the abstract model of ATC system is introduced by identifying mobile agents like aircraft and controller then the abstract ATC model is transformed into formal ATC model. The three major operations of Takeoff, enroute and landing have been formalized using agent-based MPN. Finally the reachability analysis has been used to verify formal ATC model.