Formal Modelling and Analysis of Embedded Systems


Focuses on techniques and tools for formal modelling, analysis, and verification of real-time, adaptive, autonomous, cloud-based, and 5G-based systems. In particular, we focus on the formal syntax and semantics of component-based, service-oriented, and cloud-based models with extra-functional requirements with respect to timing and resource usage.

Currently, most embedded systems must function in a distributed setting, communicating with other systems, often unknown at the time of their creation, over networks or other communication channels. In this context, systematic techniques for managing complexity and for ensuring critical system properties during design become a necessity. Formal modeling and analysis techniques, by their very nature, can play a significant role in this regard.

One of the main targets of the Formal Modeling and Analysis of Embedded Systems research group is to develop rigorous/formal frameworks (theory and tools) for designing and verifying embedded systems, be they resource-constrained real-time systems, ambient assisted living or autonomous cyber-physical systems (e.g., autonomous heavy vehicles, drones etc.), as well as to provide mathematical means of predicting and assuring their behaviors at early stages of system development. In addition, we enhance the formal analysis frameworks with testing capabilities against functional, timing, and energy-usage requirements, which rely on similar techniques as verification (e.g. model checking), yet set the premises for testing code.

Latest research includes:

  • Modeling and Verifying Functional, Timing, and Resource-usage Behavior of Embedded Systems (supported by REMES IDE)
  • Automatic test generation for Industrial Safety-critical Control Systems (supported by CompleteTest tool)
  • Pattern-based Requirements Specification and Consistency Analysis: supported by the tools ProPas and ReSA (Tutorial)
  • Statistical Model Checking (supported by the SIMPPAAL tool) and Bounded Model Checking (supported by the SyMC tool) of Industrial Simulink Models
  • Automated Verification of Atomic Concurrent Real-Time Transactions (supported by the UPPCART framework)
  • Assurance of Intelligent Ambient Assisted Living Solutions (using the tools UPPAAL, UPPAAL SMC, and PRISM)
  • Formal Verification of Complex Robotic Systems
  • Strategy Synthesis and Collision-Avoidance Verification for Autonomous Agents
  • Model checking 5G Service Orchestration
Project TitleStatus
A Digital Twin Framework for Dynamic and Robust Distributed Systems active
ACICS - Assured Cloud Platforms for Industrial Cyber-physical Systems active
DPAC - Dependable Platforms for Autonomous systems and Control active
PERformance-based Formal modelling and Optimal tRaffic Management for movING-block RAILway signalling active
Performant and Flexible digital Systems through Verifiable AI active
RELIANT Industrial graduate school: Reliable, Safe and Secure Intelligent Autonomous Systems active
SmartDelta: Automated Quality Assurance and Optimization in Incremental Industrial Software Systems Development active
Software Center: Aspects of Automated Testing active
VeriDevOps - Automated Protection and Prevention to Meet Security Requirements in DevOps Environments active
Adequacy-based Testing of Extra-Functional Properties of Embedded Systems (VR) finished
ARROWS - Design Techniques for Adaptive Embedded Systems finished
CAMI - Artificially intelligent ecosystem for self-management and sustainable quality of life in AAL (Ambient Assisted Living) finished
DAGGERS - Data aggregation for embedded real-time database systems finished
Embedded Systems Verification using Timed Automata Technology (VR) finished
Health5G: Future eHealth powered by 5G finished
MBAT - Combined Model-based Analysis and Testing (Artemis/Vinnova) finished
PG-CBD-CVer – Component Verification finished
Q-ImPreSS - Quality Impact Prediction for Evolving Service-oriented Software finished
V-trustEE finished
VeriSpec - Structured Specification and Automated Verification for Automotive Functional Safety finished
XIVT - eXcellence in Variant Testing finished

[Show all publications]

An Experiment in Requirements Engineering and Testing using EARS Notation for PLC Systems (May 2023)
Mikael Ebrahimi Salari, Eduard Paul Enoiu, Wasif Afzal, Cristina Seceleanu
19th Workshop on Advances in Model Based Testing (A-MOST 2023)

Model-Based Policy Synthesis and Test-Case Generation for Autonomous Systems (Apr 2023)
Rong Gu, Eduard Paul Enoiu
19th Workshop on Advances in Model Based Testing (A-MOST 2023)

PyLC: A Framework for Transforming and Validating PLC Software using Python and Pynguin Test Generator (Apr 2023)
Mikael Ebrahimi Salari, Eduard Paul Enoiu, Wasif Afzal, Cristina Seceleanu
SAC2023, The 38th ACM/SIGAPP Symposium On Applied Computing (SAC 2023)

A Systematic Approach to Automotive Security (Mar 2023)
Masoud Ebrahimi , Stefan Marksteiner, Dejan Nickovic , Roderick Bloem , David Schögler , Philipp Eisner , Samuel Sprung , Thomas Schober , Sebastian Chlup , Christoph Schmittner , Sandra König
25th International Symposium On Formal Methods (FM'23)

Correctness-Guaranteed Strategy Synthesis and Compression for Multi-Agent Autonomous Systems (Sep 2022)
Rong Gu, Peter Jensen , Cristina Seceleanu, Eduard Paul Enoiu, Kristina Lundqvist
Science of Computer Programming (SCICO-223)

Verifiable Strategy Synthesis for Multiple Autonomous Agents: A Scalable Approach (Jun 2022)
Rong Gu, Peter Jensen , Danny Poulsen , Cristina Seceleanu, Eduard Paul Enoiu, Kristina Lundqvist
International Journal on Software Tools for Technology Transfer (STTT)

Cristina Seceleanu, Associate Professor

Room: U1-194
Phone: +46-70-2837717