Technical Papers Parallel Session-I: Formalizing air traffic control system using agent-based Mobile Petri Nets
Abstract/Description
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.
Keywords
Aircraft, Atmospheric modeling, Aerospace control, Mobile agents, Unified modeling language, Computational modeling, Mathematical model
Location
C-9, AMAN CED
Session Theme
Technical Papers Parallel Session-I (Artificial Intelligence)
Session Type
Parallel Technical Session
Session Chair
Dr. Jawwad Shamsi
Start Date
12-12-2015 3:10 PM
End Date
12-12-2015 3:30 PM
Recommended Citation
Jamal, M., & Zafar, N. A. (2015). Technical Papers Parallel Session-I: Formalizing air traffic control system using agent-based Mobile Petri Nets. International Conference on Information and Communication Technologies. Retrieved from https://ir.iba.edu.pk/icict/2015/2015/4
COinS
Technical Papers Parallel Session-I: Formalizing air traffic control system using agent-based Mobile Petri Nets
C-9, AMAN CED
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.
