Guillermo Rodriguez-Navas is a Senior Lecturer of the Embedded Systems division of IDT. Previously, he worked as researcher and lecturer for the University of the Balearic Islands, in Spain.
His speciality is the study of the dependability and safety aspects of complex embedded systems, with strong emphasis on the application of formal verification techniques for the analysis of such systems. He also has wide experience in fault tolerance for distributed embedded systems and fieldbus communication, including fault-tolerant clock synchronization for real-time systems.
He is currently member of the Formal Modelling and Analysis of Embedded Systems (FMAES) and maintains an active collaboration with the Systems, Robotics and Vision research group of the University of the Balearic Islands, Spain.
He obtained the title of Telecommunications Engineer (Msc) by the University of Vigo, Spain, in 2001 and a PhD degree in Computer Science by the University of the Balearic Islands (UIB), Spain, in 2010. He is also a certified teacher of yoga IYENGAR® since 2010.
My current research interests lay on the application of formal verification techniques to requirements engineering and system specification in the areas of automotive and transportation. I am leading the project SaDIES, in collaboration with Bombardier AB and Volvo Construction Equipment, which aims at developing a method for safe insertion of dynamic binary instrumentation in embedded systems. I also participate in the project VeriSpec, in collaboration with Volvo Group Truck Technology and Scania SV, which aims at introducing state-of-the-art formal verification tools into the current development process of these companies. I am also part of the project RetNet, in which I collaborate with TTTech (Austria) developing a novel framework for efficient scheduling of real-time traffic over TTEthernet.
In the last years, I have developed a growing interest in the sustainability aspects of the technology we are designing and building (distributed embedded systems), since they have significant social, economical, political and environmental impact. This has not become part of my research yet, but I would love to find collaborations around these topics.
Verifying the timing of a persistent storage for stateful fog applications (Jun 2022) Zeinab Bakhshi , Guillermo Rodriguez-Navas, Hans Hansson
Using UPPAAL to Verify Recovery in a Fault-tolerant Mechanism Providing Persistent State at the Edge (Sep 2021) Zeinab Bakhshi Valojerdi, Guillermo Rodriguez-Navas, Hans Hansson 2021 ETFA – IEEE 26th International Conference on Emerging Technologies and Factory Automation (ETFA)
Fault-tolerant Permanent Storage for Container-based Fog Architectures (Mar 2021) Zeinab Bakhshi Valojerdi, Hans Hansson, Guillermo Rodriguez-Navas
Optimized Allocation of Fault-tolerant Embedded Software with End-to-end Timing Constraints (May 2019) Nesredin Mahmud, Cristina Seceleanu, Hamid Reza Faragardi, Guillermo Rodriguez-Navas, Saad Mubeen
Bounded Invariance Checking of Simulink Models (Apr 2019) Predrag Filipovikj, Guillermo Rodriguez-Navas, Cristina Seceleanu The 34th ACM/SIGAPP Symposium On Applied Computing (SAC'19)
Bounded Verification of Simulink Models (Dec 2018) Predrag Filipovikj, Guillermo Rodriguez-Navas, Cristina Seceleanu
|FORA - Fog Computing for Robotics and Industrial Automation||finished|
|PROMPT - Professional Master’s in Software Engineering (step II, phase B&C)||active|
|RetNet - The European Industrial Doctorate Programme on Future Real-Time Networks||finished|
|SaDIES. Safe Dynamic Software Instrumentation for Embedded Systems||finished|
|SafeCer - Safety Certification of Software-Intensive Systems with Reusable Components||finished|
|SYNOPSIS - Safety Analysis for Predictable Software Intensive Systems||finished|
|TRYM: Trust your Metrics!||active|
|VeriSpec - Structured Specification and Automated Verification for Automotive Functional Safety||finished|
Francisco Pozo (former)
Nesredin Mahmud (former)
Predrag Filipovikj (former)
|Design and evaluation of fault tolerant mechanisms for Dynamic Software Instrumentation||available|
|Design, implementation and validation of a highly-dependable communication infrastructure based on Switched FTT-Ethernet||available|
|Master thesis: Applying Model Checking Techniques on Scania Vehicle Control Systems||finished|