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.
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 Journal of Systems Architecture (JSA)
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)
Power-aware Allocation of Fault-tolerant Multi-rate AUTOSAR Applications (Dec 2018) Nesredin Mahmud, Guillermo Rodriguez-Navas, Hamid Reza Faragardi, Saad Mubeen, Cristina Seceleanu 25th Asia-Pacific Software Engineering Conference (APSEC'18)
Model-Checking-based vs. SMT-based Consistency Analysis of Industrial Embedded Systems Requirements: Application and Experience (Oct 2018) Predrag Filipovikj, Guillermo Rodriguez-Navas, Cristina Seceleanu Electronic Communications of the EASST Vol. 75 (ECEASST)
Schedule Reparability: Increasing Time-Triggered Network Recovery from Link Failures (Sep 2018) Francisco Pozo, Guillermo Rodriguez-Navas, Hans Hansson 24th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA'18)
|FORA - Fog Computing for Robotics and Industrial Automation||active|
|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||active|
|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|