Campus Units

Aerospace Engineering, Computer Science, Electrical and Computer Engineering, Mathematics

Document Type


Publication Version

Accepted Manuscript

Publication Date


Journal or Book Title

Journal of Aerospace Information Systems




As the costs of fuel and maintenance increase and regulations on weight and environmental impact tighten, there is an increasing push to transition onboard aircraft networks to wireless, reducing weight, fuel, maintenance time, and pollution. A candidate short-range wireless network for aircraft onboard communications is outlined using the common ZigBee protocol and privacy-preserving search implemented as a secure publish/subscribe system using specially coded metadata. Formally specifying safety and security properties and modeling the network in New e(X)tensible Model Verifier enable verification and fault analysis via model checking and lay the groundwork for future certification avenues. Experiments formally analyzing the candidate wireless network are reported, showing overhead and availability for encrypted and fault-tolerant communications. A formal model is proposed, which allows system designers to estimate communication failure rates and directly trade off fault tolerance for bandwidth, while preserving communication security.


This is a manuscript of an article published as Dureja, Rohit, and Kristin Yvonne Rozier. "Formal Framework for Safety, Security, and Availability of Aircraft Communication Networks." Journal of Aerospace Information Systems (2020). DOI: 10.2514/1.I010769. Posted with permission.

Copyright Owner

American Institute of Aeronautics and Astronautics



File Format


Published Version