Predrag Filipovikj (not working at IDT anymore)

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:

  • 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
  • SMT/SAT-based 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, MDH and University of Osijek with Ivica Crnkovic

 

Community service as reviewer.

Conferences:

  • 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)
  • Symposium on Reliable Distributed Systems (SRDS)
  • SEAMS 2018 13th International Symposium on Software Engineering for Adaptive and Self-Managing Systems
  • NFM 2019: 11th Annual NASA Formal Methods Symposium 

 

Journals:

  • IEEE Transactions on Industrial Informatics
  • IEEE Access Journal

 

Community service as Program Committee

  • International Conference ICT Innovations (2017, 2018, 2019)

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:

  • PROPAS (The PROperty PAtten Specification and Analysis) is a tool set for automated and formal consistency analysis of industrial critical requirements based on Satisfiability Modulo Theories (under development)
  • j2uppaal - a JAVA library for easy manipulation of UPPAAL models.