IEEE - Aerospace and Electronic Systems - May 2023 - 88

Formal Verification of Safety-Critical Aerospace Systems
[22] S. Paul,G.A.Agha, S.Patterson, and C.A.Varela,
" Verification of eventual consensus in Synod using a failure-aware
actor model, " in Proc. 13th NASA Formal
Methods Symp., , 2021, pp. 249-267.
[23] L. Lamport, " The part-time parliament, " ACM Trans.
Comput. Syst., vol. 16, no. 2, pp. 133-169, 1998.
[24] M. J. Fischer, N. A. Lynch, and M. S. Paterson,
" Impossibility of distributed consensus with one faulty
process, " J. ACM, vol. 32, no. 2, pp. 374-382, 1985.
[25] L. Lamport, Specifying Systems: The TLA Language and
Toolsfor Hardware and Software Engineers. Boston, MA,
USA: Addison-Wesley., 2002.
[26] R. Fagin, J. Y. Halpern, Y. Moses, andM. Vardi, Reasoning
AboutKnowledge. Cambridge,MA, USA: MIT Press, 2004.
[27] S. Paul, S. Patterson, and C. A. Varela, " Collaborative situational
awareness for conflict-aware flight planning, " in Proc.
39th IEEE/AIAADigit.Avionics Syst. Conf., 2020, pp. 1-10.
[28] L. G€onczy, M. Kovacs, and D. Varro, " Modeling and verification
of reliable messaging by graph transformation systems, "
Electron. Notes Theor. Comput. Sci., vol. 175,
no. 4, pp. 37-50, 2007.
[29] C. C. Insaurralde andE. Blasch, " Framework prototype to test
decision support system for avionics analytics, " in Proc.
IEEE/AIAA 40thDigit.Avionics Syst. Conf., 2021, pp. 1-11.
[30] E. Blasch and B. Pokines, " Analytical science for autonomy
evaluation, " in Proc. IEEE Nat. Aerosp. Electron.
Conf., 2019, pp. 598-605.
[31] E. Blasch, F. Darema, S. Ravela, and A. Aved, Eds.,
Handbook ofDynamic Data Driven Applications Systems.
New York, NY, USA: Springer, 2021.
[32] E. Blasch,E. Bosse, and D. A. Lambert, High-Level Information
Fusion Management and Systems Design.Norwood,
MA, USA:Artech House, 2012.
[33] E. Cruz-Camacho, S. Paul, F. Kopsaftopoulos, and C. A.
Varela, " Towards provably correct probabilistic flight systems, "
in Proc. Int. Conf. Dyn. Data Driven Appl. Syst.,
2020, pp. 236-244.
[34] A. Bhaumik, A. Dutta, F. Kopsaftopoulos, and C. A. Varela,
" Proving the correctness of multicopter rotor fault
detection and identification software, " in Proc. 40th AIAA/
IEEE Digit. Avionics Syst. Conf., 2021, pp. 1-10.
[35] F. Kopsaftopoulos and F.-K. Chang, " A dynamic datadriven
stochastic state-awareness framework for the next
generation of bio-inspired fly-by-feel aerospace vehicles, "
in Handbook of Dynamic Data Driven Applications Systems.
Cham, Switzerland: Springer, 2018, pp. 697-721.
[36] F. Kopsaftopoulos, R. Nardari, Y. Li, and F. Chang,
" Data-driven state awareness for fly-by-feel aerial vehicles:
Experimental assessment of a non-parametric probabilistic
stall detection approach, " Proc. 11th Int. Workshop Struct.
Health Monit., pp. 1596-1604, 2017.
[37] S. Breese, F. Kopsaftopoulos, and C. Varela, " Towards
proving runtime properties of data-driven systems using
safety envelopes, " in Proc. 12th Int. Work. Struct. Health
Monit., Stanford, CA, USA, 2019.
[38] A. Dutta, M. E. McKay, F. Kopsaftopoulos, and F. Gandhi,
" Fault detection and identification for multirotor aircraft
by data-driven and statistical learning methods, " in
Proc. AIAA/IEEE Elect. Aircr. Technol. Symp., 2019,
pp. 1-18.
[39] A. Dutta, M. McKay, F. Kopsaftopoulos, and F. Gandhi,
" Statistical residual-based time series methods for multicopter
fault detection and identification, " Aerosp. Sci.
Technol., vol. 112, 2021, Art. no. 106649.
[40] S. Paul, S. Patterson, and C. A. Varela, " Formal guarantees
of timely progress for distributed knowledge propagation, "
in Proc. 3rd Work. Form. Method. Autom. Syst., (Electronic
Proc. in Theoretical Computer Science Series),
vol. 348. The Hague, Netherlands: Open Publishing Association,
2021, pp. 73-91.
[41] Y. Wang and Y. J. Zhao, " Fundamental issues in systematic
design of airborne networks for aviation, " in Proc.
IEEE Aerosp. Conf., 2006, pp. 8-pp.
[42] L. Lipsky, " M/M/1 queue, " Queueing Theory: A. Linear
Algebraic Approach. New York, NY, USA: Springer,
pp. 33-75, 2009.
[43] A. Al Hanbali, A. A. Kherani, and P. Nain, " Simple models
for the performance evaluation of a class of two-hop
relay protocols, " in Proc. Int. Conf. Res. Netw., 2007,
pp. 191-202.
[44] M. M. Hamdi, L. Audah, S. A. Rashid, A. H. Mohammed,
S. Alani, and A. S. Mustafa, " A review of applications,
characteristics and challenges in vehicular ad-hoc networks
(VANETs), " in Proc. Int. Congr. Hum.-Comput. Interact.,
Optim. Robot. Appl., 2020, pp. 1-7.
[45] D. P. Bertsekas, R. G. Gallager, and P. Humblet, Data
Networks, vol. 2. Hoboken, NJ, USA: Prentice-Hall,
1992.
[46] A. Leon-Garcia, Probability and Random Processes for
Electrical Engineering, 2nd ed.,Reading, MA, USA: Addison-Wesley,
1994.
[47] S. Paul, F. Kopsaftopoulos, S. Patterson, and C. A. Varela,
" Dynamic data-driven formal progress envelopes for distributed
algorithms, " in Proc. Dyn. Data-Driven Appl.
Syst., 2020, pp. 245-252.
[48] S. Imai, A. Galli, and C. A. Varela, " Dynamic data-driven
avionics systems: Inferring failure modes from data
streams, " in Proc. Dyn. Data-Driven Appl. Syst,Reykjavik,
Iceland, Jun. 2015, pp. 1665-1674.
[49] L. De Moura and N. Bjørner, " Z3: An efficient SMT solver, "
in Proc. Int. Conf. Tools Alg. Const. Anal. Syst., 2008,
pp. 337-340.
88
IEEE A&E SYSTEMS MAGAZINE
MAY 2023
IEEE - Aerospace and Electronic Systems - May 2023

Table of Contents for the Digital Edition of IEEE - Aerospace and Electronic Systems - May 2023
