RADIOELECTRONIC AND COMPUTER SYSTEMS

This article discusses intelligent, computer-based learning methods for teaching reliability engineering principles to onboard computing platforms used in unmanned aerial vehicles and nanosatellites. This study focuses on integrating mathematical reliability models, simulation-based engineering tasks, and formal verification tools into an adaptive educational environment for safety-critical aerospace systems. This study aims to develop an educational methodology that combines adaptive intelligent tutoring with formal verification techniques to train students to design, analyze, and formally prove the correctness of reliability-related algorithms used in onboard computing systems. The tasks to be solved are: defining a competency model for fault-tolerant onboard computing, designing parameterized simulation-based learning tasks, integrating fault-injection scenarios into software quality assessment, and establishing correctness-critical computational kernels for adaptive tutoring. Additional tasks include developing a learner‑modeling mechanism for individualized trajectories and validating reliability-related algorithms used in education. The methods used include: Monte‑Carlo simulation of failure processes, analytic consistency checks, formal verification with Lean, Isabelle/HOL, and Rocq, fault‑injection-driven software quality evaluation, and adaptive knowledge‑tracing–based task sequencing. The proposed approach is demonstrated through an OnBoard1000 case study. The current validation is limited to a proof-of-concept prototype, reproducible computational checks, hidden-test diagnostics, and a prespecified classroom pilot protocol; completed classroom outcome data will be identified future work. Conclusions. The proposed approach demonstrates that combining simulation-driven engineering tasks with formal verification activities encourages students to validate the accuracy of their algorithms and reliability models rather than relying solely on numerical results. This supports the development of rigorous engineering reasoning required in safety-critical domains such as onboard computing in aerospace. Scientific novelty consists of integrating formal theorem-proving tools into an adaptive intelligent tutoring framework for reliability engineering education. The contribution is not a new knowledge-tracing algorithm but a domain-specific methodological layer that connects mission profiles and operating conditions, reliability assumptions and models, architectural redundancy decisions, and parameterized learning tasks with formally verified reference computations and adaptive task selection. In the proposed approach, formal proofs serve as a learning mechanism that teaches students to verify the correctness properties of algorithms and reliability models used in fault-tolerant onboard computing systems.

Bertot, Y. and Castéran, P. (2004) Interactive Theorem Proving and Program Development: Coq’Art. Berlin: Springer. DOI: 10.1007/978-3-662-07964-5.

CADFEM (2026) Reliability analysis for electronic/electrical systems. CADFEM Engineering Services. [Online]. Available at: https://www.cadfem.net [Accessed: 31 May 2026].

Corbett, A.T. and Anderson, J.R. (1994) 'Knowledge tracing: Modeling the acquisition of procedural knowledge', User Modeling and User-Adapted Interaction, 4(4), pp. 253–278. DOI: 10.1007/BF01099821.

Das Adhikary, P. and Metsämuuronen, J. (2025) 'Knowledge tracing models in digital learning: Historical evolution, categorization, and empirical evaluation'. DOI: 10.13140/RG.2.2.17277.27364.

De Moura, L. and Ullrich, S. (2021) 'The Lean 4 theorem prover and programming language', in Automated Deduction – CADE 28 (Lecture Notes in Computer Science, vol. 12699). Cham: Springer, pp. 625–635. DOI: 10.1007/978-3-030-79876-5_37.

European Space Agency (2026) 'System level methods', Digital Reliability Handbook. [Online]. Available at: https://handbook.reliability.space/en/latest/system/handbook/reliability_prediction/methods.html [Accessed: 31 May 2026].

Hao, W., Xian, B. and Xie, T. (2022) 'Fault-tolerant position tracking control design for a tilt tri-rotor unmanned aerial vehicle', IEEE Transactions on Industrial Electronics, 69(1), pp. 604–612. DOI: 10.1109/TIE.2021.3050384.

Hess, A.V., Mödersheim, S.A. and Brucker, A.D. (2023) 'Stateful protocol composition in Isabelle/HOL', ACM Transactions on Privacy and Security, 26(3), art. no. 25. DOI: 10.1145/3577020.

Hong, J.-H., Shin, H.-S. and Tsourdos, A. (2019) 'A design of a short course with COTS UAV system for higher education students', IFAC-PapersOnLine, 52(12), pp. 466–471. DOI: 10.1016/j.ifacol.2019.11.287.

Hussein, M. and Nouacer, R. (2022) 'Reference architecture specification for drone systems', Microprocessors and Microsystems, 95, art. no. 104705. DOI: 10.1016/j.micpro.2022.104705.

Ihekoronye, V.U., Ajakwe, S.O., Lee, J.M. and Kim, D.-S. (2025) 'DroneGuard: An explainable and efficient machine learning framework for intrusion detection in drone networks', IEEE Internet of Things Journal, 12(7), pp. 7708–7722. DOI: 10.1109/JIOT.2024.3519633.

Impagliazzo, J., Bourque, P. and Mead, N.R. (2020) 'Incorporating CC2020 and SWECOM competencies into software engineering curricula: A tutorial', in Proceedings of the IEEE 32nd Conference on Software Engineering Education and Training (CSEE&T). Munich, Germany, pp. 1–3. DOI: 10.1109/CSEET49119.2020.9206238.

Kurup, L.D., Joshi, A. and Shekhokar, N. (2016) 'A review on student modeling approaches in ITS', in Proceedings of the 3rd International Conference on Computing for Sustainable Global Development (INDIACom). New Delhi, India, pp. 2513–2517.

Li, S., Jin, J., Afrin, M., Zheng, Q., Fu, J. and Tian, Y.-C. (2024) 'UAV-as-a-Service for robotic edge system resilience', in Proceedings of the IEEE International Conference on Web Services (ICWS). Shenzhen, China, pp. 142–148. DOI: 10.1109/ICWS62655.2024.00034.

Malviya, V.K., Minn, W., Shar, L.K. and Jiang, L. (2025) 'Fuzzing drones for anomaly detection: A systematic literature review', Computers & Security, 148, art. no. 104157. DOI: 10.1016/j.cose.2024.104157.

Nugroho, V.A. and Lee, B.M. (2025) 'GPS-aided deep learning for beam prediction and tracking in UAV mmWave communication', IEEE Access, 13, pp. 117065–117077. DOI: 10.1109/ACCESS.2025.3586594.

Paramesha, K., Hamsaveni, M. and Soumya, B.J. (2025) 'Artificial intelligence driven curriculum development: Challenges and modalities', in Proceedings of the Annual International Conference on Data Science, Machine Learning and Blockchain Technology (AICDMB). Mysuru, India, pp. 1–7. DOI: 10.1109/AICDMB64359.2025.11277952.

Pu, Y., Wu, W., Han, Y. and Chen, D. (2018) 'Parallelizing Bayesian knowledge tracing tool for large-scale online learning analytics', in Proceedings of the IEEE International Conference on Big Data (Big Data). Seattle, WA, USA, pp. 3245–3254. DOI: 10.1109/BigData.2018.8622355.

Ramezanian, S. and Niemi, V. (2024) 'Cybersecurity education in universities: A comprehensive guide to curriculum development', IEEE Access, 12, pp. 61741–61766. DOI: 10.1109/ACCESS.2024.3392970.

Rausand, M. and Høyland, A. (2003) System Reliability Theory: Models, Statistical Methods, and Applications. 2nd edn. Hoboken, NJ: Wiley. DOI: 10.1002/9780470317046.

Saied, M., Mishi, A., Francis, C. and Noun, Z. (2024) 'A deep learning approach for fault-tolerant data fusion applied to UAV position and orientation estimation', Electronics, 13(16), art. no. 3342. DOI: 10.3390/electronics13163342.

Shi, Y., Li, J., Lv, M., Wang, N. and Zhang, B. (2025) 'Distributed consensus control for 6-DOF fixed-wing multi-UAVs in asynchronously switching topologies', IEEE Transactions on Vehicular Technology, 74(4), pp. 5649–5663. DOI: 10.1109/TVT.2024.3520141.

Sun, C., et al. (2024) 'Advancing UAV communications: A comprehensive survey of cutting-edge machine learning techniques', IEEE Open Journal of the Vehicular Technology, 5, pp. 825–854. DOI: 10.1109/OJVT.2024.3401024.

Tolo, S. and Andrews, J. (2024) 'Fault tree analysis including component dependencies', IEEE Transactions on Reliability, 73(1), pp. 413–421. DOI: 10.1109/TR.2023.3264943.

VanLehn, K. (2006) 'The behavior of tutoring systems', International Journal of Artificial Intelligence in Education, 16(3), pp. 227–265. DOI: 10.3233/IRG-2006-16(3)02.

Zhang, K., Zhang, W., Du, X. and Li, Z. (2025) 'Fixed-time event-triggered sliding mode consensus control for multi-AUV formation under external disturbances and communication delays', Journal of Marine Science and Engineering, 13(12), art. no. 2294. DOI: 10.3390/jmse13122294