No AccessFull-Length Papers

Formal Framework for Safety, Security, and Availability of Aircraft Communication Networks

Iowa State University, Ames, Iowa 50011

*Graduate Student, Department of Computer Science.

and

Iowa State University, Ames, Iowa 50011

†Assistant Professor, Departments of Aerospace Engineering, Computer Science, Electrical and Computer Engineering, and Mathematics.

Search for more papers by this author

Published Online:26 May 2020https://doi.org/10.2514/1.I010769

Abstract

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.

References

[1] Canaday H., “War on Wiring,” Aerospace America, 2017, pp. 24–27, https://aerospaceamerica.aiaa.org/features/war-on-wiring/. Google Scholar
[2] Dureja R., Rozier E. W. and Rozier K. Y., “A Case Study in Safety, Security, and Availability of Wireless-Enabled Aircraft Communication Networks,” 17th AIAA Aviation Technology, Integration, and Operations Conference, AIAA Paper 2017-3112, June 2017. https://doi.org/10.2514/6.2017-3112 Link Google Scholar
[3] Attia S. B., Cunha A., Koubâa A. and Alves M., “Fault-Tolerance Mechanisms for ZigBee Wireless Sensor Networks,” Work-in-Progress (WiP) Session of the 19th Euromicro Conference on Real-Time Systems (ECRTS 2007), IEEE, New York, July 2007, pp. 37–40. Google Scholar
[4] Wan J., Wu J. and Xu X., “A Novel Fault Detection and Recovery Mechanism for Zigbee Sensor Networks,” Second International Conference on Future Generation Communication and Networking (FGCN), Vol. 1, IEEE, New York, 2008, pp. 270–274. https://doi.org/10.1109/FGCN.2008.105 Google Scholar
[5] Alena R., Ellis S. R., Hieronymus J. and Maclise D., “Wireless Avionics and Human Interfaces for Inflatable Spacecraft,” Aerospace Conference, IEEE, New York, 2008, pp. 1–16. https://doi.org/10.1109/AERO.2008.4526527 Google Scholar
[6] Alena R., Gilstrap R., Baldwin J., Stone T. and Wilson P., “Fault Tolerance in ZigBee Wireless Sensor Networks,” Aerospace Conference, IEEE, New York, 2011, pp. 1–15. https://doi.org/10.1109/AERO.2011.5747474 Google Scholar
[7] Ulusar U. D., Celik G., Turk E., Al-Turjman F. and Guvenc H., “Practical Performability Assessment for ZigBee-Based Sensors in the IoT Era,” Performability in Internet of Things, EAI/Springer Innovations in Communication and Computing, Springer, Cham, Switzerland, 2019, pp. 21–31. https://doi.org/10.1007/978-3-319-93557-7_2 Crossref Google Scholar
[8] Song D. X., Wagner D. and Perrig A., “Practical Techniques for Searches on Encrypted Data,” IEEE Symposium on Security and Privacy (S&P), IEEE Computer Soc., Washington, D.C., 2000, pp. 44–55. https://doi.org/10.1109/secpri.2000.848445 Google Scholar
[9] Goh E.-J., “Secure Indexes,” Report 2003/216, 2003, http://eprint.iacr.org/. Google Scholar
[10] Curtmola R., Garay J., Kamara S. and Ostrovsky R., “Searchable Symmetric Encryption: Improved Definitions and Efficient Constructions,” Journal of Computer Security, Vol. 19, No. 5, 2011, pp. 895–934. https://doi.org/10.3233/JCS-2011-0426 Crossref Google Scholar
[11] Boneh D. and Waters B., “Conjunctive, Subset, and Range Queries on Encrypted Data,” Theory of Cryptography, Springer, Berlin, 2007, pp. 535–554. https://doi.org/10.1007/978-3-540-70936-7_29 Crossref Google Scholar
[12] Wang C., Ren K., Yu S. and Urs K. M. R., “Achieving Usable and Privacy-Assured Similarity Search over Outsourced Cloud Data,” Proceedings of the IEEE International Conference on Computer Communications (INFOCOM), IEEE, New York, March 2012, pp. 451–459. https://doi.org/10.1109/infcom.2012.6195784 Google Scholar
[13] Ibrahim A., Jin H., Yassin A. A., Zou D. and Xu P., “Towards Efficient Yet Privacy-Preserving Approximate Search in Cloud Computing,” Computer Journal, Vol. 57, No. 2, 2014, pp. 241–254. https://doi.org/10.1093/comjnl/bxt045 Crossref Google Scholar
[14] Kamara S. and Lauter K., “Cryptographic Cloud Storage,” Financial Cryptography and Data Security, Springer, Berlin, 2010, pp. 136–149. https://doi.org/10.1007/978-3-642-14992-4_13 Crossref Google Scholar
[15] Hofheinz D. and Weinreb E., “Searchable Encryption with Decryption in the Standard Model,” IACR Cryptology ePrint Archive, Vol. 2008, 2008, p. 423, https://eprint.iacr.org/2008/423. Google Scholar
[16] Boneh D., Di Crescenzo G., Ostrovsky R. and Persiano G., “Public Key Encryption with Keyword Search,” International Conference on the Theory and Applications of Cryptographic Techniques, Springer, Berlin, 2004, pp. 506–522. https://doi.org/10.1007/978-3-540-24676-3_30 Google Scholar
[17] Zhao Y. and Rozier K. Y., “Formal Specification and Verification of a Coordination Protocol for an Automated Air Traffic Control System,” Proceedings of the 12th International Workshop on Automated Verification of Critical Systems (AVoCS 2012), Electronic Communications of the EASST, Vol. 53, European Assoc. of Software Science and Technology, Berlin, Germany, 2012. Google Scholar
[18] Zhao Y. and Rozier K. Y., “Formal Specification and Verification of a Coordination Protocol for an Automated Air Traffic Control System,” Science of Computer Programming, Vol. 96, No. 3, 2014, pp. 337–353. https://doi.org/10.1016/j.scico.2014.04.002 Crossref Google Scholar
[19] Zhao Y. and Rozier K. Y., “Probabilistic Model Checking for Comparative Analysis of Automated Air Traffic Control Systems,” Proceedings of the 33rd IEEE/ACM International Conference on Computer-Aided Design (ICCAD 2014), IEEE/ACM, San Jose, CA, 2014, pp. 690–695. https://doi.org/10.1109/iccad.2014.7001427 Google Scholar
[20] Mattarei C., Cimatti A., Gario M., Tonetta S. and Rozier K. Y., “Comparing Different Functional Allocations in Automated Air Traffic Control Design,” Proceedings of Formal Methods in Computer-Aided Design (FMCAD 2015), IEEE/ACM, Austin, TX, 2015. https://doi.org/10.1109/fmcad.2015.7542260 Google Scholar
[21] Gario M., Cimatti A., Mattarei C., Tonetta S. and Rozier K. Y., “Model Checking at Scale: Automated Air Traffic Control Design Space Exploration,” Proceedings of the 28th International Conference on Computer Aided Verification (CAV 2016), LNCS, Vol. 9780, Springer, Toronto, 2016, pp. 3–22. https://doi.org/10.1007/978-3-319-41540-6_1 Google Scholar
[22] Groce A., Havelund K., Holzmann G., Joshi R. and Xu R.-G., “Establishing Flight Software Reliability: Testing, Model Checking, Constraint-Solving, Monitoring and Learning,” Annals of Mathematics and Artificial Intelligence, Vol. 70, No. 4, 2014, pp. 315–349. https://doi.org/10.1007/s10472-014-9408-8 Crossref Google Scholar
[23] Mehlitz P. C., “Trust Your Model-Verifying Aerospace System Models with Java Pathfinder,” 2008 IEEE Aerospace Conference, IEEE, New York, 2008, pp. 1–11. https://doi.org/10.1109/aero.2008.4526573 Google Scholar
[24] Can A. B., Bultan T., Lindvall M., Lux B. and Topp S., “Eliminating Synchronization Faults in Air Traffic Control Software via Design for Verification with Concurrency Controllers,” Automated Software Engineering, Vol. 14, No. 2, 2007, pp. 129–178. https://doi.org/10.1007/s10515-007-0008-2 Crossref Google Scholar
[25] Munoz C., Carreño V. and Dowek G., “Formal Analysis of the Operational Concept for the Small Aircraft Transportation System,” Rigorous Development of Complex Fault-Tolerant Systems, Springer, Berlin, 2006, pp. 306–325. https://doi.org/10.1007/11916246_16 Crossref Google Scholar
[26] Bozzano M., Cimatti A., Katoen J.-P., Nguyen V. Y., Noll T. and Roveri M., “The COMPASS Approach: Correctness, Modelling and Performability of Aerospace Systems,” Computer Safety, Reliability, and Security, Springer, Berlin, 2009, pp. 173–186. https://doi.org/10.1007/978-3-642-04468-7_15 Crossref Google Scholar
[27] Chan W., Anderson R. J., Beame P., Burns S., Modugno F., Notkin D. and Reese J. D., “Model Checking Large Software Specifications,” IEEE Transactions on Software Engineering, Vol. 24, No. 7, 1998, pp. 498–520. https://doi.org/10.1109/32.708566 Crossref Google Scholar
[28] Sreemani T. and Atlee J. M., “Feasibility of Model Checking Software Requirements: A Case Study,” Proceedings of the 11th Annual Conference on Computer Assurance (COMPASS), IEEE, New York, 1996, pp. 77–88. https://doi.org/10.1109/cmpass.1996.507877 Google Scholar
[29] von Essen C. and Giannakopoulou D., “Analyzing the Next Generation Airborne Collision Avoidance System,” Tools and Algorithms for the Construction and Analysis of Systems, Springer, Berlin, 2014, pp. 620–635. https://doi.org/10.1007/978-3-642-54862-8_54 Crossref Google Scholar
[30] Bozzano M., Bruintjes H., Cimatti A., Katoen J.-P., Noll T. and Tonetta S., “COMPASS 3.0,” Tools and Algorithms for the Construction and Analysis of Systems (TACAS), edited by Vojnar T. and Zhang L., Springer, Cham, Switzerland, 2019, pp. 379–385. https://doi.org/10.1007/978-3-030-17462-0_25 Crossref Google Scholar
[31] Bozzano M., Cimatti A., Pires A. F., Jones D., Kimberly G., Petri T., Robinson R. and Tonetta S., “Formal Design and Safety Analysis of AIR6110 Wheel Brake System,” Proceedings of the 27th International Conference on Computer Aided Verification (CAV), Springer, Berlin, 2015, pp. 518–535. https://doi.org/10.1007/978-3-319-21690-4_36 Google Scholar
[32] “DO-178B: Software Considerations in Airborne Systems and Equipment Certification,” Radio Technical Commission for Aeronautics, Dec. 1992, https://www.rtca.org/content/standards-guidance-materials [retrieved 20 May 2020]. Google Scholar
[33] “DO-178C/ED-12C: Software Considerations in Airborne Systems and Equipment Certification,” Radio Technical Commission for Aeronautics, 2012, https://www.rtca.org/content/standards-guidance-materials [retrieved 20 May 2020]. Google Scholar
[34] “DO-333: Formal Methods Supplement to DO-178C and DO-278A,” Radio Technical Commission for Aeronautics, 2011, https://www.rtca.org/content/standards-guidance-materials [retrieved 20 May 2020]. Google Scholar
[35] “DO-254: Design Assurance Guidance for Airborne Electronic Hardware,” Radio Technical Commission for Aeronautics, April 2000, https://www.rtca.org/content/standards-guidance-materials [retrieved 20 May 2020]. Google Scholar
[36] Clarke E. M., Emerson E. A. and Sistla A. P., “Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications,” ACM Transactions on Programming Languages and Systems, Vol. 8, No. 2, 1986, pp. 244–263. https://doi.org/10.1145/5397.5399 Crossref Google Scholar
[37] Queille J. P. and Sifakis J., “Specification and Verification of Concurrent Systems in CESAR,” International Symposium on Programming, Vol. 137, Lecture Notes in Computer Science, Springer, Berlin, 1982, pp. 337–351. https://doi.org/10.1007/3-540-11494-7_22 Google Scholar
[38] Dureja R. and Rozier K. Y., “More Scalable LTL Model Checking via Discovering Design-Space Dependencies,” Tools and Algorithms for the Construction and Analysis of Systems (TACAS), edited by Beyer D. and Huisman M., Springer, Cham, Switzerland, 2018, pp. 309–327. https://doi.org/10.1007/978-3-319-89960-2_17 Crossref Google Scholar
[39] Cavada R., Cimatti A., Dorigatti M., Griggio A., Mariotti A., Micheli A., Mover S., Roveri M. and Tonetta S., “The nuXmv Symbolic Model Checker,” International Conference on Computer Aided Verification, Springer, Berlin, 2014, pp. 334–342. https://doi.org/10.1007/978-3-319-08867-9_22 Google Scholar
[40] Cimatti A., Clarke E., Giunchiglia F. and Roveri M., “NuSMV: A New Symbolic Model Checker,” International Journal on Software Tools for Technology Transfer, Vol. 2, No. 4, 2000, pp. 410–425. https://doi.org/10.1007/s100090050046 Crossref Google Scholar
[41] Cavada R., Cimatti A., Jochim A. C., Keighren G., Olivetti E., Pistore M., Roveri M. and Tchaltsev A., “NuSMV 2.4 User Manual,” CMU/ITC-irst, Tech. Rept., Trento, Italy, 2005. Google Scholar
[42] Bozzano M., Cavada R., Cimatti A., Dorigatti M., Griggio A., Mariotti A., Micheli A., Mover S., Roveri M. and Tonetta S., “nuXmv 2.0 User Manual,” Fondazione Bruno Kessler, Tech. Rept., Trento, Italy, 2019. Google Scholar
[43] Raimondi F., Lomuscio A. and Sergot M. J., “Towards Model Checking Interpreted Systems,” Proceedings of the Second International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS), ACM Press, New York, 2002, pp. 115–125. https://doi.org/10.1145/860575.860792 Google Scholar
[44] Gribaudo M., Horváth A., Bobbio A., Tronci E., Ciancamerla E. and Minichino M., “Model-Checking Based on Fluid Petri Nets for the Temperature Control System of the ICARO Co-Generative Plant,” Computer Safety, Reliability and Security, edited by Anderson S., Felici M. and Bologna S., Springer, Berlin, 2002, pp. 273–283. https://doi.org/10.1007/3-540-45732-1_27 Crossref Google Scholar
[45] Tribble A. and Miller S., “Software Safety Analysis of a Flight Management System Vertical Navigation Function—A Status Report,” 22nd Digital Avionics Systems Conference Proceedings (DASC), IEEE, New York, 2003, pp. 1.B.1–1.1–9. https://doi.org/10.1109/dasc.2003.1245805 Google Scholar
[46] Choi Y. and Heimdahl M., “Model Checking Software Requirement Specifications Using Domain Reduction Abstraction,” 18th IEEE International Conference on Automated Software Engineering, IEEE Computer Soc., Washington, D.C., 2003, pp. 314–317. https://doi.org/10.1109/ase.2003.1240328 Google Scholar
[47] Miller S. P., Tribble A. C., Whalen M. W. and Heimdahl M. P. E., “Proving the Shalls,” International Journal on Software Tools for Technology Transfer, Vol. 8, Nos. 4–5, 2006, pp. 303–319. https://doi.org/10.1007/s10009-004-0173-6 Crossref Google Scholar
[48] Miller S. P., “Will This Be Formal?” Theorem Proving in Higher Order Logics, edited by Mohamed O. A., Muñoz C. and Tahar S., Springer, Berlin, 2008, pp. 6–11. https://doi.org/10.1007/978-3-540-71067-7_2 Crossref Google Scholar
[49] Yoo J., Jee E. and Cha S., “Formal Modeling and Verification of Safety-Critical Software,” IEEE Software, Vol. 26, No. 3, 2009, pp. 42–49. https://doi.org/10.1109/MS.2009.67 Crossref Google Scholar
[50] Gan X., Dubrovin J. and Heljanko K., “A Symbolic Model Checking Approach to Verifying Satellite Onboard Software,” Science of Computer Programming, Vol. 82, March 2014, pp. 44–55. https://doi.org/10.1016/j.scico.2013.03.005 Crossref Google Scholar
[51] Lahtinen J., Valkonen J., Björkman K., Frits J., Niemelä I. and Heljanko K., “Model Checking of Safety-Critical Software in the Nuclear Engineering Domain,” Reliability Engineering & System Safety, Vol. 105, Sept. 2012, pp. 104–113. https://doi.org/10.1016/j.ress.2012.03.021 Crossref Google Scholar
[52] Dureja R. and Rozier K. Y., “FuseIC3: An Algorithm for Checking Large Design Spaces,” Formal Methods in Computer Aided Design (FMCAD), IEEE, New York, 2017, pp. 164–171. https://doi.org/10.23919/FMCAD.2017.8102255 Google Scholar
[53] McMillan K., “The SMV Language,” Cadence Berkeley Labs., Tech. Rept., Berkeley, CA, 1999. Google Scholar
[54] de Moura L., Owre S., Rueß H., Rushby J., Shankar N., Sorea M. and Tiwari A., “SAL 2,” Computer Aided Verification, edited by Alur R. and Peled D. A., Springer, Berlin, 2004, pp. 496–500. https://doi.org/10.1007/978-3-540-27813-9_45 Crossref Google Scholar
[55] Brayton R. and Mishchenko A., “ABC: An Academic Industrial-Strength Verification Tool,” Computer Aided Verification, edited by Touili T., Cook B. and Jackson P., Springer, Berlin, 2010, pp. 24–40. https://doi.org/10.1007/978-3-642-14295-6_5 Crossref Google Scholar
[56] Chang R. and et al., “SatCarrier CONOPS: A Concept of Operations for Satellite Carriers,” AIAA, Tech. Rept., Reston, VA, 2009. Google Scholar
[57] Erzberger H. and Heere K., “Algorithm and Operational Concept for Resolving Short-Range Conflicts,” Proceedings of the Institution of Mechanical Engineers, Part G: Journal of Aerospace Engineering, Vol. 224, No. 2, 2010, pp. 225–243. 10.1243/09544100 JAERO546 Crossref Google Scholar
[58] Ryan J., Cummings M., Roy N., Banerjee A. and Schulte A., “Designing an Interactive Local and Global Decision Support System for Aircraft Carrier Deck Scheduling,” Infotech@Aerospace, AIAA Paper 2011-1516, June 2011. Link Google Scholar
[59] Mindock J., Reilly J., Urbina M., Rubin D., Hailey M., Reyes D., Hanson A., Burba T., Cerro J., McGuire K. and Middour C., “Exploration Medical Capability ConOps and Systems Engineering Technical Interchange Meeting Summary,” NASA Johnson Space Center, JSC-CN-39099, Houston, TX, 2017, https://ntrs.nasa.gov/archive/nasa/casi.ntrs.nasa.gov/20170002573.pdf [retrieved 20 May 2020]. Google Scholar
[60] Clarke E. M., Henzinger T. A., Veith H. and Bloem R., Handbook of Model Checking, Springer International Publishing, 2018. https://doi.org/10.1007/978-3-319-10575-8 Crossref Google Scholar
[61] Rozier K. Y., “Linear Temporal Logic Symbolic Model Checking,” Computer Science Review, Vol. 5, No. 2, 2011, pp. 163–203. https://doi.org/10.1016/j.cosrev.2010.06.002 Crossref Google Scholar
[62] Cimatti A. and Tonetta S., “A Property-Based Proof System for Contract-Based Design,” 2012 38th Euromicro Conference on Software Engineering and Advanced Applications, IEEE, New York, 2012, pp. 21–28. https://doi.org/10.1109/seaa.2012.68 Google Scholar
[63] Cimatti A., Dorigatti M. and Tonetta S., “OCRA: A Tool for Checking the Refinement of Temporal Contracts,” Automated Software Engineering (ASE), IEEE, New York, 2013, pp. 702–705. https://doi.org/10.1109/ase.2013.6693137 Google Scholar
[64] Cimatti A. and Tonetta S., “Contracts-Refinement Proof System for Component-Based Embedded Systems,” Science of Computer Programming, Vol. 97, Jan. 2015, pp. 333–348. https://doi.org/10.1016/j.scico.2014.06.011 Crossref Google Scholar
[65] Gómez-Martínez E., Rodrguez R. J., Elorza L. E., Rezabal M. I. and Earle C. B., “Model-Based Verification of Safety Contracts,” International Conference on Software Engineering and Formal Methods, edited by Canal C. and Idani A., Springer, Cham, Switzerland, 2015, pp. 101–115. https://doi.org/10.1007/978-3-319-15201-1_7 Google Scholar
[66] Cimatti A. and Tonetta S., “A Temporal Logics Approach to Contract-Based Design,” Architecture-Centric Virtual Integration (ACVI), IEEE, New York, 2016, pp. 1–3. https://doi.org/10.1109/acvi.2016.7 Google Scholar
[67] Quinton S. and Graf S., “Contract-Based Verification of Hierarchical Systems of Components,” Software Engineering and Formal Methods (SEFM), IEEE, New York, 2008, pp. 377–381. https://doi.org/10.1109/sefm.2008.28 Google Scholar
[68] Graf S., Passerone R. and Quinton S., “Contract-Based Reasoning for Component Systems with Rich Interactions,” Embedded Systems Development, Springer, New York, 2013, pp. 139–154. https://doi.org/10.1007/978-1-4614-3879-3_8 Google Scholar
[69] Nuzzo P., Sangiovanni-Vincentelli A. L., Bresolin D., Geretti L. and Villa T., “A Platform-Based Design Methodology with Contracts and Related Tools for the Design of Cyber-Physical Systems,” Proceedings of the IEEE, Vol. 103, No. 11, 2015, pp. 2104–2132. https://doi.org/10.1109/JPROC.2015.2453253 Crossref Google Scholar
[70] Bozzano M., Cimatti A., Mattarei C. and Tonetta S., “Formal Safety Assessment via Contract-Based Design,” Automated Technology for Verification and Analysis, Springer International Publishing, Cham, 2014, pp. 81–97. https://doi.org/10.1007/978-3-319-11936-6_7 Crossref Google Scholar
[71] Cimatti A., Dorigatti M. and Tonetta S., “OCRA: Othello Contracts Refinement Analysis User Guide (Version 1.3),” 2015, https://es-static.fbk.eu/tools/ocra/download/OCRA_Language_User_Guide.pdf [retrieved 20 May 2020]. Google Scholar
[72] Bittner B., Bozzano M., Cavada R., Cimatti A., Gario M., Griggio A., Mattarei C., Micheli A. and Zampedri G., “The xSAP Safety Analysis Platform,” Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Springer, Berlin, 2016, pp. 533–539. https://doi.org/10.1007/978-3-662-49674-9_31 Crossref Google Scholar
[73] “xSAP: The eXtended Safety Assessment Platform User Guide (Version 1.2),” https://es.fbk.eu/tools/xsap/downloads/xsap-manual.pdf [retrieved 20 May 2020]. Google Scholar
[74] Schroeder B. and Gibson G. A., “Disk Failures in the Real World: What Does an MTTF of 1,000,000 Hours Mean to You?” Proceedings of the 5th USENIX Conference on File and Storage Technologies, USENIX Assoc., Berkeley, CA, 2007, p. 1–es. https://doi.org/10.5555/1267903.1267904 Google Scholar
[75] Rozier E., Belluomini W., Deenadhayalan V., Hafner J., Rao K. and Zhou P., “Evaluating the Impact of Undetected Disk Errors in Raid Systems,” 2009 IEEE/IFIP International Conference on Dependable Systems & Networks, IEEE, New York, 2009, pp. 83–92. https://doi.org/10.1109/dsn.2009.5270353 Google Scholar
[76] Hafner J. L., Deenadhayalan V., Belluomini W. and Rao K., “Undetected Disk Errors in RAID Arrays,” IBM Journal of Research and Development, Vol. 52, No. 4.5, 2008, pp. 413–425. https://doi.org/10.1147/rd.524.0413 Crossref Google Scholar
[77] Wallace G., Douglis F., Qian H., Shilane P., Smaldone S., Chamness M. and Hsu W., “Characteristics of Backup Workloads in Production Systems,” Proceedings of the 10th USENIX Conference on File and Storage Technologies, USENIX, Assoc., Berkeley, CA, 2012, p. 4. https://doi.org/10.5555/2208461.2208465 Google Scholar
[78] Tarasov V., Kumar S., Ma J., Hildebrand D., Povzner A., Kuenning G. and Zadok E., “Extracting Flexible, Replayable Models from Large Block Traces,” Proceedings of the 10th USENIX Conference on File and Storage Technologies, USENIX Assoc., San Jose, CA, 2012, p. 22. https://doi.org/10.5555/2208461.2208483 Google Scholar
[79] Anderson E., “Capture, Conversion, and Analysis of an Intense NFS Workload,” Proceedings of the 7th Conference on File and Storage Technologies, USENIX Assoc., Berkeley, CA, 2009, pp. 139–152. https://doi.org/10.5555/1525908.1525919 Google Scholar
[80] Madhyastha H. V., McCullough J. C., Porter G., Kapoor R., Savage S., Snoeren A. C. and Vahdat A., “scc: Cluster Storage Provisioning Informed by Application Characteristics and SLAs,” Proceedings of the 10th USENIX Conference on File and Storage Technologies, USENIX Assoc., Berkeley, CA, 2012, p. 23. https://doi.org/10.5555/2208461.2208484 Google Scholar
[81] Soundararajan G., Lupei D., Ghanbari S., Popescu A. D., Chen J. and Amza C., “Dynamic Resource Allocation for Database Servers Running on Virtual Storage,” Proceedings of the 7th Conference on File and Storage Technologies, USENIX Assoc., Berkeley, CA, 2009, pp. 71–84. https://doi.org/10.5555/1525908.1525914 Google Scholar
[82] Chen P. M., Lee E. K., Gibson G. A., Katz R. H. and Patterson D. A., “RAID: High-Performance, Reliable Secondary Storage,” ACM Computing Surveys, Vol. 26, No. 2, 1994, pp. 145–185. https://doi.org/10.1145/176979.176981 Crossref Google Scholar
[83] Anvin H. P., “The Mathematics of RAID-6,” 2007, http://alamos.math.arizona.edu/RTG16/ECC/raid6.pdf [retrieved 20 May 2020]. Google Scholar
[84] Jacobson N., Lectures in Abstract Algebra: III. Theory of Fields and Galois Theory, Vol. 32, Springer International Publishing, 2012. https://doi.org/10.1007/978-1-4612-9872-4 Google Scholar
[85] Salehi M. A., Caldwell T., Fernandez A., Mickiewicz E., Rozier E. W., Zonouz S. and Redberg D., “RESeED: Regular Expression Search over Encrypted Data in the Cloud,” IEEE 7th International Conference on Cloud Computing (CLOUD), IEEE, New York, 2014, pp. 673–680. https://doi.org/10.1109/cloud.2014.95 Google Scholar
[86] Salehi M. A., Caldwell T., Fernandez A., Mickiewicz E., Rozier E. W., Zonouz S. and Redberg D., “RESeED: A Secure Regular-Expression Search Tool for Storage Clouds,” Software: Practice and Experience, Vol. 47, No. 9, 2017, pp. 1221–1241. https://doi.org/10.1002/spe.2473 Crossref Google Scholar
[87] Joux A., “A One Round Protocol for Tripartite Diffie-Hellman,” Journal of Cryptology, Vol. 17, No. 4, 2004, pp. 263–276. https://doi.org/10.1007/s00145-004-0312-y Crossref Google Scholar
[88] Bernstein D. J., “Curve25519: New Diffie-Hellman Speed Records,” International Workshop on Public Key Cryptography, Springer, Berlin, 2006, pp. 207–228. https://doi.org/10.1007/11745853_14 Google Scholar
[89] Goldschlag D., Reed M. and Syverson P., “Onion Routing,” Communications of the ACM, Vol. 42, No. 2, 1999, pp. 39–41. https://doi.org/10.1145/293411.293443 Crossref Google Scholar
[90] Nezhad A. A., Miri A. and Makrakis D., “Location Privacy and Anonymity Preserving Routing for Wireless Sensor Networks,” Computer Networks, Vol. 52, No. 18, 2008, pp. 3433–3452. https://doi.org/10.1016/j.comnet.2008.09.005 Crossref Google Scholar
[91] Chakrabarty S., John M. and Engels D. W., “Black Routing and Node Obscuring in IoT,” IEEE 3rd World Forum on Internet of Things (WF-IoT), IEEE, New York, 2016, pp. 323–328. https://doi.org/10.1109/wf-iot.2016.7845477 Google Scholar
[92] Singh A. and Snigdh I., “Modelling Failure Conditions in Zigbee Based Wireless Sensor Networks,” International Journal of Wireless and Microwave Technologies, Vol. 7, No. 2, 2017, pp. 25–34. https://doi.org/10.5815/ijwmt.2017.02.03 Crossref Google Scholar
[93] Markov A. A., The Theory of Algorithms, Vol. 15, Springer, Netherlands, 1960. Google Scholar
[94] Law A. M. and Kelton D. M., Simulation Modeling and Analysis, 3rd ed., McGraw–Hill Higher Education, 1999. https://doi.org/10.5555/554952 Google Scholar
[95] Abramowitz M. and Stegun I. A., “Handbook of Mathematical Functions,” Vol. 55, Applied Mathematics Series, Dover Publications, 1966, p. 39. Google Scholar

Journal of Aerospace Information Systems, volume 17 issue 7 cover

Volume 17, Number 7July 2020

Metrics

Crossmark

Information

Copyright © 2020 by the American Institute of Aeronautics and Astronautics, Inc. All rights reserved. All requests for copying and permission to reprint should be submitted to CCC at www.copyright.com; employ the eISSN 2327-3097 to initiate your request. See also AIAA Rights and Permissions www.aiaa.org/randp.

Topics

Keywords

Acknowledgments

The authors acknowledge the National Science Foundation CAREER Award CNS-1664356 and NASA’s Efficient Reconfigurable Cockpit Design and Fleet Operations using Software Intensive, Networked and Wireless Enabled Architecture (ECON) grant NNX15AQ84G for supporting this work. The authors also thank the anonymous reviewers for their valuable feedback and comments.

Digital

Received17 June 2019
Accepted22 April 2020
Published online26 May 2020

Formal Framework for Safety, Security, and Availability of Aircraft Communication Networks

Abstract

References

What's Popular

Metrics

Information