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.
Automated SMT-based Consistency Checking of Industrial Critical Requirements (Jan 2018) Predrag Filipovikj, Guillermo Rodriguez-Navas, Mattias Nyberg , Cristina Seceleanu Applied Computing Review (ACR)
SMT-based Consistency Analysis of Industrial Systems Requirements (Apr 2017) Predrag Filipovikj, Guillermo Rodriguez-Navas, Mattias Nyberg , Cristina Seceleanu 32nd ACM SIGAPP Symposium On Applied Computing (SAC2017)
Analyzing Industrial Simulink Models by Statistical Model Checking (Mar 2017) Predrag Filipovikj, Nesredin Mahmud, Raluca Marinescu, Guillermo Rodriguez-Navas, Cristina Seceleanu, Oscar Ljungkrantz , Henrik Lönn MRTC Report, Mälardalen Real-Time Research Centre (MRTC2017)
Schedule Synthesis for Next Generation Time-Triggered Networks (Feb 2017) Francisco Pozo, Guillermo Rodriguez-Navas, Hans Hansson, Wilfried Steiner MRTC Report, Mälardalen Real-Time Research Centre (MRTC2017)
Synthesizing time-triggered schedules for switched networks with faulty links (Oct 2016) Guy Avni , Guillermo Rodriguez-Navas, Shibashis Guha 2016 International Conference on Embedded Software (EMSOFT) (EMSOFT'16)
Next Generation Real-Time Networks Based on IT Technologies (Sep 2016) Wilfried Steiner , Pablo Gutiérrez Peón, Marina Gutiérrez, Ayhan Mehmed, Guillermo Rodriguez-Navas, Elena Lisova, Francisco Pozo 21st IEEE Conference on Emerging Technologies and Factory Automation (ETFA'16)
|PROMPT - Professional Master’s in Software Engineering (step II, phase B&C)||active|
|RetNet - The European Industrial Doctorate Programme on Future Real-Time Networks||active|
|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|
|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|