I work for Scania Group, where I am a part of the complete vehicle integration testing section. My role is to improve the existing, and to develop new methods for the Hardware- and Software in the loop (HIL/SIL) verification of our products. Before joining Scania, I worked as a Postdoctoral Researcher at the KTH Royal Institute of Sweden in the division of Theoretical Computer Science. I hold a Ph.D. in Computer Science with specialization in Formal Modeling and Analysis of Embedded Software from Mälardalen University in 2019. The title of my thesis is "Automated Approaches for Formal Verification of Embedded Systems Artifacts". For the interested readers, the fulltext of the thesis is available via the following link.
If you are a student who is looking for a thesis project within the broad area of software verification (formal verification and/or testing), or a researcher who is looking for a collaboration partner, please do not hesitate to get in touch.
email: first.last at gmail.com
Scania Group
Sweden
News
- 2021-11-19: I am looking for 2 Master students for a maste degree project in test planning automation. More info on the following link. If you are interested, please do not hesitate to get in touch.
- 2021-10-29: I am looking for 2 Master students for a very interesting thesis project in software testing at Scania. The position has been filled. Welcome Selomie and Rohini!
- 2021-06-03: Delighted to announce that I have passed the examination for the Foundation Level Cerificate in Software Testing, Version 2018. Now officially an ISTQB Ceritified Tester!
- 2021-05-28: Happy and honoured to be invided as a PC member for the 3rd International Workshop on Automated and verifiable Software sYstem DEvelopment (ASYDE 2021)
- 2021-05-19: Honoured to be part of the program comittee for the 2nd International Workshop on Model-driven Engineering for Software Architecture (MDE4SA 2021)
- 2021-03-10: Published a technical report on Bounded Invariant Analysis for Stateflow Programs. Check out the preprint on arxiv.
Research statement
My main research interest is verification of embedded software, with particular focus on software in the automotive domain. I am interested in applying both formal techniques and software testing for the verification of the different embedded software artifacts, including but not limited to: system specifications, design-time behavioral models, and code. The following areas have been in my narrow focus:
- Formalizing system requirements specifications
- Formal analysis of formally encoded system requirements specifications with respect to different properties, such as: consistency, completeness, vacuity, etc.
- Formal verification of Simulink/Stateflow models
As I transitioned to a new position at Scania Group Research and Development sector, I have broadened my research interests to include integration testing. Specifically, I am looking at developing testing methodologies that can be applied for improving the efficiency and utilization of HIL testing platforms.
Projects
Thus far, I have been involved in the following academic research projects:
- VeriSpec: Structured Specification and Automated Verification for Automotive Functional Safety. Partners: Mälardalen University, Scania CV AB, and Volvo Group Trucks Technology.
- AVerT: Automated Verification and Testing.
Research Output
I have published more than 10 peer-reviewed scientific publications and several technical reports. The complete list of publications follows, but you can also check out my Google Scholar profile.
Peer-reviewed Publications (in reverse chronological order)
- Service Realizability Check as a Technique to Support a Service Security Assurance Case Elena Lisova, and Aida Causevic. Published in the Proceedings of the 21st IEEE International Conference on Industrial Technology (ICIT'20). February, 2020.
- Specifying Industrial System Requirements using Specification Patterns: A Case Study of Evaluation with Practitioners. and Cristina Seceleanu. Published in the Proceedings of 14th International Conference on Evaluation of Novel Approaches to Software Engineering (ENASE 2019). May, 2019.[Preprint]
- Bounded Invariance Checking of Simulink Models. , Guillermo Rodriguez-Navas, and Cristina Seceleanu. Published in the Proceedings of the 34th ACM/SIGAPP Symposium On Applied Computing (SAC'19). April, 2019.[Preprint]
- Model-Checking-based vs. SMT-based Consistency Analysis of Industrial Embedded Systems Requirements: Application and Experience. , Guillermo Rodriguez-Navas, and Cristina Seceleanu. Published in Electronic Communications of the EASST Vol. 75 (ECEASST). October, 2018.[Preprint]
- Automated SMT-based Consistency Checking of Industrial Critical Requirements. , Guillermo Rodriguez-Navas, Mattias Nyberg, and Cristina Seceleanu. Published in Journal of Applied Computing Review (ACR). January, 2018.[Preprint]
- An Energy-aware Mutation Testing Framework for EAST-ADL Architectural Models. Raluca Marinescu, , Guillermo Eduard Paul Enoiu, Jonatan Larsson, and Cristina Seceleanu. Published in the Proceedings of 29th Nordic Workshop on Programming Theory (NWPT'17). October, 2017.[Preprint]
- SMT-based Consistency Analysis of Industrial Systems Requirements. , Guillermo Rodriguez-Navas, and Cristina Seceleanu. Published in the Proceedings of the 32nd ACM SIGAPP Symposium On Applied Computing (SAC2017). April, 2017. [Preprint]
- Increasing Embedded Systems’ Quality through Automated Specification and Analysis of Requirements and Behavioral Models. . Published in the Proceedings of the 43rd International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM 2017). January, 2017. [Preprint]
- Simulink to UPPAAL Statistical Model Checker: Analyzing Automotive Industrial Systems. , Nesredin Mahmoud, Raluca Marinescu, Guillermo Rodriguez-Navas, Cristina Seceleanu, Oscar Ljungkrantz, Henrik Lönn. Published in the Proceedings of the 21st International Symposium on Formal Methods (FM2016). November, 2016.[Preprint]
- Integrating Pattern-based Formal Requirements Specification in an Industrial Tool-chain. , Trevor Jagerfeld, Guillermo Rodriguez-Navas, and Cristina Seceleanu. Published in the Proceedings of the 10th IEEE International Workshop on Quality Oriented Reuse of Software (QUORS'16). June, 2016.[Preprint]
- Reassessing the Pattern-Based Approach for Formalizing Requirements in the Automotive Domain. , Mattias Nyberg, and Guillermo Rodriguez-Navas. Published in the Proceedings of the 22nd IEEE International Requirements Engineering Conference (RE'14). August, 2014.[Preprint]
Technical Reports
- Bounded Invariant Checking for Stateflow Programs. , Dilian Gurov, and Mattias Nyberg. March, 2021.[Arxiv]
- Bounded Verification of Simulink Models. , Guillermo Rodriguez-Navas, and Cristina Seceleanu. MRTC Report, Mälardalen Real-Time Research Centre. December, 2018.[Preprint]
- Analyzing Industrial Simulink Models by Statistical Model Checking. , Nesredin Mahmoud, Raluca Marinescu, Guillermo Rodriguez-Navas, Cristina Seceleanu, Oscar Ljungkrantz, Henrik Lönn. MRTC Report, Mälardalen Real-Time Research Centre. March, 2017.[Preprint]
Tools and Libraries
I am also contributing to the dissemination of my research results through various tools. I have developed, either myself or with other developers the following tools and libraries:
- SeSf: A Python library for symbolic execution of Stateflow programs.
- SyMC: A Python tool for symblic bounded model checking of Simulink programs
- Simppaal: A Java-based tool for statistical model checking of Simulink models.
- ProPAS: A tool for formal requirements specification based on specification pattern system (SPS), written in C# and .NET.
- J2Uppaal: A Java library for easy manipulation of UPPAAL documents in .XML format.
All the above listed tools are free and open source. Each tool is liked to its own Github project repository. For more projects, please visit my GitHub profile.