I am employed by Scania Group, where I work as a Technical Lead in the Enablement sector within the R&D department. My primary responsibility is to lead and drive the development of tools based on automated reasoning technology for product data management. My position is rather diverse, and in addition to my primary responsibilities, I regularly take responsilities and taks primarily associated to Software Architect, Product Owner, and Team Lead. Before joining the Enablement sector, I was working on complete vehicle integration testing, where my main focus was on improving the the existing, and developing new methods for the Hardware- and Software in the loop (HIL/SIL) verification. 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.
I am a Ceritified ISTQB Test Professional. ISTQB Certified Test Analyst as of 2022, and Professional Tester as of 2021.
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
- 2023-06-11: Martin and David have successfully completed their thesis project. Please check out their report if you are interested to read more about dependency between test cases and their impact on passive testing.
- 2023-03-13: Martin Sten and David Halldoff are starting their Bachelor thesis project with us. They will be investigating the vacuity problem for offline testing. Welcome on board!
- 2023-03-06: Pranav Vijayachandran Nair is starting his master thesis project with us. The objective of his thesis is to study existing and propose novel techniques and methods for directed fuzzing for vehicle cybersecurity test. Looking forward to a great cooperation!
- 2023-02-28: Our paper "Identifying Redundancies and Gaps Across Testing Levels During Verification of Automotive Software" has been accepted at the International Workshop on User Interface Test Automation and Testing Techniques for Event Based Software, collocated with ICST 2023. Congrats to the coauthors!
- 2022-09-28: Our paper "Bounded Invariant Checking for Stateflow" has been accepted and presented at the 4th International Workshop on Automated and verifiable Software sYstem DEvelopment (ASYDE), collocated with SEFM 2022. Congrats to the coauthors!
- 2022-07-11: Pleased to announce that I have passed the examination for The ISTQB® Advanced Level Test Analyst (CTAL-TA) certification. Now officially certified Test Analyst!
- 2022-07-01: Selomie and Rohni have sucessfully completed their thesis project. Congratulations! Stay tuned for the link to the final thesis report.
- 2021-11-19: I am looking for 2 Master students for a 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)
- Identifying Redundancies and Gaps Across Testing Levels During Verification of Automotive Software. Rohini Bisht, Selomie Kindu Ejigu, Gregory Gay and Predrag Filipovikj. Published in the Proceedings 6th nternational Workshop on User Interface Test Automation and Testing Techniques for Event Based Software (INTUITESTBEDS 2023) co-located with ICST Conference 2023. April, 2023.[Preprint]
- Bounded Invariant Checking for Stateflow. Gustav Ung, Dilian Gurov, and Mattias Nyberg. Published in the Proceedings 4th International Workshop on Automated and verifiable Software sYstem DEvelopment (ASYDE) co-located with SEFM Conference 2022. September, 2022. [Link to Proceedings (open access)]
- 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.