Formal Modelling and Analysis of Embedded Systems
Focus:
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 reserach 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 wel 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
Model Checking Collision Avoidance of Nonlinear Autonomous Vehicle Models (Nov 2021) Rong Gu, Cristina Seceleanu, Eduard Paul Enoiu, Kristina Lundqvist Formal Methods 2021 (FM'21)
From UML Modeling to UPPAAL Model checking of 5G Dynamic Service Orchestration (May 2021) Ashalatha Kunnappilly, Peter Backeman, Cristina Seceleanu 7th international Conference on the Engineering of Computer Based Systems (ECBS 2021)
Formal Verification of Collision Avoidance for Nonlinear Autonomous Vehicle Models (Apr 2021) Rong Gu, Cristina Seceleanu, Eduard Paul Enoiu, Kristina Lundqvist
Is Requirements Similarity a Good Proxy for Software Similarity? An Empirical Investigation in Industry (Apr 2021) Muhammad Abbas, Alessio Ferrari , Anas Shatnawi , Eduard Paul Enoiu, Mehrdad Saadatmand Requirements Engineering: Foundation for Software Quality (REFSQ 2021)
Assured Cloud Platforms for Industrial Cyber-Physical Systems: The ACICS Approach (Apr 2021) Cristina Seceleanu, Eduard Paul Enoiu, Moris Behnam, Gabriele Capannini, Jan Carlson, Kristina Lundqvist, Séverine Sentilles 7th international Conference on the Engineering of Computer Based Systems (ECBS 2021)
Towards Human-Like Automated Test Generation: Perspectives from Cognition and Problem Solving (Mar 2021) Eduard Paul Enoiu, Robert Feldt International Conference on Cooperative and Human Aspects of Software Engineering 2021 (CHASE 2021)
Cristina Seceleanu, Associate Professor
Email: cristina.seceleanu@mdh.seRoom: U1-170
Phone: +46-70-2837717