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.

Predrag Filipovikj, Ph.D.

Computer Scientist and Formal Verification Expert

email: first.last at gmail.com
Scania Group
Sweden

Google Scholar
GitHub
LinkedIn

News

Hide old news

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

The quality of my research has continuously been recognized and rewarded from the research community. Our work on automated consistency analysis of system requirements specifications using satisfability modulo theories was awarded the Best Paper Award on the 32nd ACM SIGAPP Symposium on Applied Computing (SAC), 2017. I was also rewarded the Best Student Research Proposal and the Best Student Presentation at the 43rd International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM), 2017.

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 Predrag Filipovikj, 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. Predrag Filipovikj, and Cristina Seceleanu. Published in the Proceedings of 14th International Conference on Evaluation of Novel Approaches to Software Engineering (ENASE 2019). May, 2019.
  • Bounded Invariance Checking of Simulink Models. Predrag Filipovikj, Guillermo Rodriguez-Navas, and Cristina Seceleanu. Published in the Proceedings of the 34th ACM/SIGAPP Symposium On Applied Computing (SAC'19). April, 2019.
  • Model-Checking-based vs. SMT-based Consistency Analysis of Industrial Embedded Systems Requirements: Application and Experience. Predrag Filipovikj, Guillermo Rodriguez-Navas, and Cristina Seceleanu. Published in Electronic Communications of the EASST Vol. 75 (ECEASST). October, 2018.
  • Automated SMT-based Consistency Checking of Industrial Critical Requirements. Predrag Filipovikj, Guillermo Rodriguez-Navas, Mattias Nyberg, and Cristina Seceleanu. Published in Journal of Applied Computing Review (ACR). January, 2018.
  • An Energy-aware Mutation Testing Framework for EAST-ADL Architectural Models. Raluca Marinescu, Predrag Filipovikj, Guillermo Eduard Paul Enoiu, Jonatan Larsson, and Cristina Seceleanu. Published in the Proceedings of 29th Nordic Workshop on Programming Theory (NWPT'17). October, 2017.
  • SMT-based Consistency Analysis of Industrial Systems Requirements. Predrag Filipovikj, Guillermo Rodriguez-Navas, and Cristina Seceleanu. Published in the Proceedings of the 32nd ACM SIGAPP Symposium On Applied Computing (SAC2017). April, 2017. -- Best Paper Award --
  • Increasing Embedded Systems’ Quality through Automated Specification and Analysis of Requirements and Behavioral Models. Predrag Filipovikj. Published in the Proceedings of the 43rd International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM 2017). January, 2017. -- Best Paper Award --
  • Simulink to UPPAAL Statistical Model Checker: Analyzing Automotive Industrial Systems. Predrag Filipovikj, 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.
  • Integrating Pattern-based Formal Requirements Specification in an Industrial Tool-chain. Predrag Filipovikj, 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.
  • Reassessing the Pattern-Based Approach for Formalizing Requirements in the Automotive Domain. Predrag Filipovikj, Mattias Nyberg, and Guillermo Rodriguez-Navas. Published in the Proceedings of the 22nd IEEE International Requirements Engineering Conference (RE'14). August, 2014.

Technical Reports

  • Bounded Invariant Checking for Stateflow Programs. Predrag Filipovikj, Dilian Gurov, and Mattias Nyberg. March, 2021.
  • Bounded Verification of Simulink Models. Predrag Filipovikj, Guillermo Rodriguez-Navas, and Cristina Seceleanu. MRTC Report, Mälardalen Real-Time Research Centre. December, 2018.
  • Analyzing Industrial Simulink Models by Statistical Model Checking. Predrag Filipovikj, Nesredin Mahmoud, Raluca Marinescu, Guillermo Rodriguez-Navas, Cristina Seceleanu, Oscar Ljungkrantz, Henrik Lönn. MRTC Report, Mälardalen Real-Time Research Centre. March, 2017.

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.