As of June 2019, I am not employed by MDU anymore. Please visit my personal page for contact and other details.
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.
Education:
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.
Conferences:
Journals:
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 [1]. The process of pattern-based formal system specification has been automated to a great extend by the SeSAMM Specifier tool [2]. 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 [3]. 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 [4]. Currently we are actively working on automating the complete procedure.
Tools
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:
Service Realizability Check as a Technique to Support a Service Security Assurance Case (Feb 2020) Predrag Filipovikj, Aida Causevic, Elena Lisova 21st IEEE International Conference on Industrial Technology (ICIT'20)
Automated Approaches for Formal Verification of Embedded Systems Artifacts (May 2019) Predrag Filipovikj
Specifying Industrial System Requirements using Specification Patterns: A Case Study of Evaluation with Practitioners (May 2019) Predrag Filipovikj, Cristina Seceleanu 14th International Conference on Evaluation of Novel Approaches to Software Engineering (ENASE 2019)
Bounded Invariance Checking of Simulink Models (Apr 2019) Predrag Filipovikj, Guillermo Rodriguez-Navas, Cristina Seceleanu The 34th ACM/SIGAPP Symposium On Applied Computing (SAC'19)
Bounded Verification of Simulink Models (Dec 2018) Predrag Filipovikj, Guillermo Rodriguez-Navas, Cristina Seceleanu
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)
Project Title | Status |
---|---|
VeriSpec - Structured Specification and Automated Verification for Automotive Functional Safety | finished |