Predrag Filipovikj is a Doctoral Student at Mälardalen University since January 2014. He joined Mälardalen University first as a Research Assistant in October 2013.
Predrag's research focus is on applied formal methods for improving the quality of embedded systems, with a special focus on the automotive industry. Predrag performs his resesarch within the VeriSpec project with a close cooperation with the following industrial partners: Scania and Volvo Group Trucks Technology. His research results have been published in proceedings of highly ranked scientific venues such as: Requirements Engineering (RE) Conference, Symphosium on Formal Methods (FM), ACM Symphosium on Applied Computing (SAC), etc.
Research topics of interest:
Beside research, Predrag is actively involved in teaching bachelor (basic) and master (advanced) level courses, as well as supervising master thesis projects:
Community service as reviewer:
Community service as Program Committee
The adoption of formal verification techniques in industrial settings is limited by the difficulty of producing formal system specification and generation of formal system models. Withing the VeriSpec project, we are developing methods and tools to automate this process and to enable non-expert practitioners in formal methods for increasing the level of confidence in the quality of their system models.
The complete body of work performed so far (incliding research, education as well as teaching) is summarized in a Licentiate thesis proposal available via the following link. A sumarry of the research proposal has been awarded the Best Student Paper and Best Student Presentation Award at the SOFSEM 2017 Student Research Forum.
Formal Specification and Analysis of Industrial Systems Requirements
For creating formal system specification, we adopt the usage of specification patterns, based on our results in which we proved their expressiveness for capturing requirements in the automotive domain . The process of pattern-based formal system specification has been automated to a great extend by the SeSAMM Specifier tool . The tool facilitates the specification of requirements, automatic generation of temporal formulas and visual feedback for validating the formalized behavior.
For assesing the quality of the system specification, we propose an SMT-based consistency analysis methodology for industrial requirements . The proposed methodology is lightweight and suitable for early debugging of system specification, in stages of development when no behavioral model of the system is available.
Formal Analysis of Behavioral System Models
Model-based development is often used in automotive industry to develop complex software functions, with Matlab Simulink becoming the de facto standard in the domain. More and more software functions are used for safety-critical features of the vehicles, making their quality assurance hot topic of interest. In our research, we propose a methodology for formal analysis of Simulink behavioral models using statical-model checking supported by UPPAAL SMC . Currently we are actively working on automating the complete procedure.
I have developed several research tools and libraries, which are published as free and open-source software on my github page. The list currently consists of the following projects:
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)
Automated SMT-based Consistency Checking of Industrial Critical Requirements (Jan 2018) Predrag Filipovikj, Guillermo Rodriguez-Navas, Mattias Nyberg , Cristina Seceleanu Applied Computing Review (ACR)
An Energy-aware Mutation Testing Framework for EAST-ADL Architectural Models (Oct 2017) Raluca Marinescu, Predrag Filipovikj, Eduard Paul Enoiu, Jonatan Larsson , Cristina Seceleanu 29th Nordic Workshop on Programming Theory (NWPT'17)
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)
|VeriSpec - Structured Specification and Automated Verification for Automotive Functional Safety||active|
|A Method and Tool for Automated Analysis of Heavy Vehicle Requirements||finished|
|Developing a type-inferencing mechanism for automatically detecting variable types in system requirements specifications||finished|