Formal Verification and Safety-Synergy in Multicore Mixed-Criticality Systems: A Comprehensive Framework for Robust Automotive Zonal Control and Virtualized Isolation
Keywords:
Mixed-Criticality Systems, Automotive Zonal Control, Real-Time Hypervisors, Memory SafetyAbstract
The rapid evolution of automotive architectures toward software-defined vehicles has necessitated the integration of tasks with varying criticality levels onto shared multicore platforms. This integration presents significant challenges regarding spatial and temporal isolation, as well as the mitigation of inter-core interference. This research article explores a comprehensive framework for securing multicore mixed-criticality systems through the lens of formal verification, memory safety, and hardware-supported virtualization. We investigate the application of the Rust programming language and its ownership model as a mechanism for static memory safety in embedded contexts, alongside the traditional use of Ada and GNAT protected objects for high-integrity systems. Furthermore, we analyze the deployment of real-time hypervisors and fault-tolerant dual-core lockstep architectures, specifically utilizing the NXP S32G processor, to establish a "security-safety synergy" in automotive zonal controllers. The study evaluates the limitations of hyper-period generation in periodic task sets and assesses the impact of virtualization on the assessment of uncertified components in the automotive domain. By synthesizing model-based development paradigms like X-by-construction with hardware-level timing protections, this article provides a publication-ready roadmap for optimizing latency and cost under stringent safety constraints. The findings suggest that a combination of language-level safety, micro-hypervisor partitioning, and fault-tolerant hardware is essential for the next generation of time-sensitive autonomous architectures.
References
Abdul Salam Abdul Karim. (2023). Fault-Tolerant Dual-Core Lockstep Architecture for Automotive Zonal Controllers Using NXP S32G Processors. International Journal of Intelligent Systems and Applications in Engineering, 11(11s), 877–885. Retrieved from https://ijisae.org/index.php/IJISAE/article/view/7749
Carvalho A., Afons F., Cardoso P., Cabral J., Ekpanyapong M., Montenegro S., and Tavares A. Functionality farming in POK/rodosvisor. Proc. Int. J. Comput. Sci. Softw. Eng., vol. 5, pp. 161–174, Aug. 2016.
Cereia M. and Bertolotti I. C. Virtual machines for distributed realtime systems. Comput. Standards Interface, vol. 31, no. 1, pp. 30–39, Jan. 2009.
Chen N., Zhao S., Gray I., Burns A., Ji S., Chang W. MSRP-FT: Reliable Resource Sharing on Multiprocessor Mixed-Criticality Systems, in: 2022 IEEE 28th Real-Time and Embedded Technology and Applications Symposium, RTAS, 2022, pp. 201–213.
Cinque M., et al. Certify the uncertified: Towards assessment of virtualization for mixed-criticality in the automotive domain. In: 2022 52nd Annual IEEE/IFIP International Conference on Dependable Systems and Networks Workshops (DSN-W). pp. 8–11. IEEE (2022).
Collin A., et al. Autonomous driving systems hardware and software architecture exploration: optimizing latency and cost under safety constraints. Systems Engineering 23(3), 327–337 (2020).
Comar C., Dross C., Gilcher F., Moy Y. Dynamic memory management in critical embedded software. AdaCore White Papers.
COVESA. Vehicle signal specification (2025).
Crespo A., Balbastre P., Simo J., Coronel J., Gracia-Perez D., and Bonnot P. Hypervisor-based multicore feedback control of mixedcriticality systems. IEEE Access, vol. 6, pp. 50627–50640, 2018.
Curnow H.J., Wichmann B.A. A synthetic benchmark. Comput. J., 19 (1) (1976), pp. 43-49.
Druml N., et al. Time-of-flight 3d imaging for mixed-critical systems. In: 2015 IEEE 13th International Conference on Industrial Informatics (INDIN). pp. 1432–1437. IEEE (2015).
El-Bayoumi A. An enhanced algorithm for memory systematic faults detection in multicore architectures suitable for mixed-critical automotive applications. International Journal of Safety and Security Engineering 10(4), 467–474 (2020).
Ferraro D., et al. Time-sensitive autonomous architectures. Real-Time Systems 59(4), 568–608 (2023).
Goossens J., Macq C. Limitation of the hyper-period in real-time periodic task set generation. In: Proceedings of the 9th International Conference on Real-Time Systems, 2001.
Haghighatkhah A., et al. Automotive software engineering: A systematic mapping study. Journal of Systems and Software 128, 25–55 (2017).
Holstein T., Wietzke J. Contradiction of separation through virtualization and inter virtual machine communication in automotive scenarios. In: Proceedings of the 2015 European Conference on Software Architecture Workshops. pp. 1–5 (2015).
Kadry H.M., et al. Electrical architecture and in-vehicle networking: Challenges and future trends. In: 2022 IEEE International Symposium on Circuits and Systems (ISCAS). pp. 1009–1013. IEEE (2022).
Martins J., Alves J., Cabral J., Tavares A., and Pinto S. µRTZVisor: A secure and safe real-time hypervisor. Electronics, vol. 6, no. 4, p. 93, Oct. 2017.
Masing L. et al. XANDAR: Exploiting the X-by-construction paradigm in model-based development of safety-critical systems. In: Proc. Design, Autom. Test Eur. Conf. Exhib. (DATE), Mar. 2022, pp. 1–5.
Miranda J., Schonberg E. Protected objects GNAT: The GNU Ada Compiler, Free Software Foundation (2004).
Missimer E., West R., and Li Y. Distributed real-time fault tolerance on a virtualized multi-core system. In: Proc. OSPERT, 2014, p. 17.
Pinto S., Tavares A., and Montenegro S. Space and time partitioning with hardware support for space applications. In: Proc. Data Syst. Aerosp. (DASIA), Eur. Space Agency, ESA SP, 2016, pp. 1–7.
Pinto S., Martins J., Lopes J., Abreu M., and Tavares A. SecSSy hypervisor: Security-safety synergy for aerospace. In: Proc. DAta Syst. Aerosp. (DASIA), Jun. 2017, pp. 1–8.
Poggi T., Onaindia P., Azkarate-askatsua M., Gruttner K., Fakih M., Peiro S., and Balbastre P. A hypervisor architecture for low-power realtime embedded systems. In: Proc. 21st Euromicro Conf. Digit. Syst. Design (DSD), Aug. 2018, pp. 252–259.
The Rust Programming Language Documentation. Using threads to run code simultaneously.
The Rust Programming Language Documentation. What is ownership?
Tinto E. Providing-spatial-isolation-experiment. GitHub Repository.
Tinto E. Evaluating a multicore mixed-criticality system implementation against a temporal isolation kernel. GitHub Repository.
Winter J. Trusted computing building blocks for embedded Linux-based ARM trustzone platforms. In: Proc. 3rd ACM Workshop Scalable Trusted Comput., Oct. 2008, p. 2130.
Downloads
Published
How to Cite
Issue
Section
License
Copyright (c) 2025 Yasuka Tsunoda
This work is licensed under a Creative Commons Attribution 4.0 International License.
Individual articles are published Open Access under the Creative Commons Licence: CC-BY 4.0.
