Open Access

ARTICLE

Modeling and Verification of Aircraft Takeoff Through Novel Quantum Nets

Maryam Jamal¹, Nazir Ahmad Zafar², Atta-ur-Rahman^3,*, Dhiaa Musleh³, Mohammed A. Gollapalli⁴, Sghaier Chabani⁴

1 School of Systems and Technology, University of Management & Technology (UMT), C-II Block C 2 Phase 1 Johar Town, Lahore, 54770, Punjab, Pakistan
2 Department of Computer Science, COMSATS University Islamabad–Sahiwal Campus, Sahiwal, 57000, Punjab, Pakistan
3 Department of Computer Science (CS), College of Computer Science and Information Technology (CCSIT), Imam Abdulrahman Bin Faisal University (IAU), Dammam, 31441, Saudi Arabia
4 Department of Computer Information System (CIS), College of Computer Science and Information Technology (CCSIT), Imam Abdulrahman Bin Faisal University (IAU), Dammam, 31441, Saudi Arabia

* Corresponding Author: Atta-ur-Rahman. Email:

Computers, Materials & Continua 2022, 72(2), 3331-3348. https://doi.org/10.32604/cmc.2022.025205

Received 16 November 2021; Accepted 11 February 2022; Issue published 29 March 2022

Abstract

The formal modeling and verification of aircraft takeoff is a challenge because it is a complex safety-critical operation. The task of aircraft takeoff is distributed amongst various computer-based controllers, however, with the growing malicious threats a secure communication between aircraft and controllers becomes highly important. This research serves as a starting point for integration of BB84 quantum protocol with petri nets for secure modeling and verification of takeoff procedure. The integrated model combines the BB84 quantum cryptographic protocol with powerful verification tool support offered by petri nets. To model certain important properties of BB84, a new variant of petri nets coined as Quantum Nets are proposed by defining their mathematical foundations and overall system dynamics, furthermore, some important system properties are also abstractly defined. The proposed Quantum Nets are then applied for modeling of aircraft takeoff process by defining three quantum nets: namely aircraft, runway controller and gate controller. For authentication between quantum nets, the use of external places and transitions is demonstrated to describe the encryption-decryption process of qubits stream. Finally, the developed takeoff quantum network is verified through simulation offered by colored petri-net (CPN) Tools. Moreover, reachability tree (RT) analysis is also performed to have greater confidence in feasibility and correctness of the proposed aircraft takeoff model through the Quantum Nets.

---

Keywords

---