Predrag Filipovikj, Doctoral student

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:

  • Licentiate in Technology, Mälardalen University, Sweden, 2017
  • Master of Science in Software Engineering, Mälardalen University, Sweden 2013
  • Master of Science in Computer Networks and e-Technologies, Faculty of Computer Science and Engineering, Macedonia, 2014
  • Bachelor in Computer Science and Electrical Engineering, Faculty of Electrical Engineering and Information Technologies, Macedonia, 2011
 

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:

  • Structured and automated formal specification of system requirements
  • Automated analysis of system specification 
  • Formal modeling and analysis of industrial behavioral models, modeled using Simulink
  • Statistical Model Checking

 

Beside research, Predrag is actively involved in teaching bachelor (basic) and master (advanced) level courses, as well as supervising master thesis projects:

  • DVA332 - Software Engineering 1, Basic Level, with Jan Carlson
  • CDT501 - Advanced Component-Based Sofware Engineering, Advanced Level, with Séverine Sentilles
  • Formal Languages and Automata, Advanced Level, University of Osijek with Ivica Crnkovic

 

Community service as reviewer:

  • IEEE Real-Time and Embedded Technology and Applications Symposium
  • IEEE Computer Society Signature Conference on Computers, Software, and Applications (COMPSAC) 
  • International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS)
  • International Conference on Engineering of Complex Computer Systems (ICECCS)
  • IEEE Transactions on Industrial Informatics
  • Symposium on Reliable Distributed Systems (SRDS)

 

Program Committee

  • International Conference ICT Innovations 2017

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.


[Show all publications]

Latest publications:

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

Increasing Embedded Systems’ Quality through Automated Specification and Analysis of Requirements and Behavioral Models (Jan 2017)
Predrag Filipovikj
43rd International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM 2017)

Simulink to UPPAAL Statistical Model Checker: Analyzing Automotive Industrial Systems (Nov 2016)
Predrag Filipovikj, Nesredin Mahmud, Raluca Marinescu, Cristina Seceleanu, Oscar Ljungkrantz , Henrik Lönn
21st International Symposium on Formal Methods (FM2016)

Integrating Pattern-based Formal Requirements Specification in an Industrial Tool-chain (Jun 2016)
Predrag Filipovikj, Trevor Jagerfield , Mattias Nyberg , Guillermo Rodriguez-Navas, Cristina Seceleanu
The 10th IEEE International Workshop on Quality Oriented Reuse of Software (QUORS'16)

Reassessing the Pattern-Based Approach for Formalizing Requirements in the Automotive Domain (Aug 2014)
Predrag Filipovikj, Mattias Nyberg , Guillermo Rodriguez-Navas
22nd IEEE International Requirements Engineering Conference (RE'14)