Cristina Seceleanu, Professor

E-mail:
cristina.seceleanu@mdu.se
Room:
U1-194
Phone:
+46-70-2837717
Division:
Division of Networked and Embedded Systems
Research group:
Formal Modelling and Analysis of Embedded Systems


Cristina Seceleanu is Professor of Computer Science and Docent at MDU, Networked and Embedded Systems (NES) division, and research leader of the Computer and Data Science (CDS) research direction. She received a MSc. in Electronics from Polytechnic University of Bucharest, Romania, in 1993, and a Ph.D. in Computer Science from Åbo Akademi and Turku Centre for Computer Science, Åbo/Turku, Finland, in Dec. 2005. Her research focuses on developing formal models and verification techniques for designing predictable real-time, adaptive and autonomous systems.

Teaching:

  • DVA 468 - Catching Bugs by Formal Verification (PROMPT course): 2023, 2022, 2021, 2020, 2019, 2018, 2017
  • DVA 241 - Distributed Systems (undergraduate course): 2018, 2017
  • CDT 316 - Distributed Systems (undergraduate course): 2016, 2015, 2014, 2013
  • DVA 442 - Advanced Validation and Verification (graduate, distance course) : 2017, 2016, 2015
  • DVA 402 - Advanced Validation and Verification (graduate course): 2012, 2011, 2010
  • CDT 505 - Real-Time Systems II (graduate course): 2012, 2011, 2009, 2008
  • The Science of Programming (Ph.D. course): 2009

 

 

 

Cristina Seceleanu's research focuses on developing and applying formal methods (especially model checking and variants) for designing and reasoning about component-based, resource-constrained real-time systems, service-oriented systems, adaptive embedded systems, and autonomous systems. The goal is to provide mathematical means of predicting system behaviors at early stages of development.

Cristina is leading the Formal Modeling and Analysis of Embedded Systems research group, at MDU, and is also the research leader of the Computer and Data Science (CDS) research direction. She has also been teacher representative for Embedded Systems, IDT, in the committee for research of the faculty board (Utskottet för forskning), 2015-2016. 

Cristina is co-author of the following integrated development environments (IDE) / toolchains that implement the research results obtained together with wonderful collaborators:

  • REMES IDE    : developed as a cooperation between projects DICES and PROGRESS. It supports the construction and analysis of embedded system behavioral models described in the REMES language. REMES is a hierarchical, dense-time language for modeling function, time and resource usage of embedded components. The REMES IDE consists of a set of tools, as follows: (i) REMES editor, (ii) automated transformations of REMES models into priced timed automata for formal analysis and verification, and (iii) REMES simulator of the timing behavior and resource consumption of embedded components, at design time. Together with Aneta Vulgarakis Feljan, Ericsson Research, Stockholm, and Marin Orliς, Ericsson Nikola Tesla, Zagreb.

 

  • ViTAL toolchain      :  a verification tool tailored for the architectural language EAST-ADL, in which functional and timing behaviors of function prototypes are expressed as timed automata models that have precise semantics and can be formally verified. The ViTAL tool enables the automatic transformation of EAST-ADL functional models into UPPAAL PORT or UPPAAL, for model checking. Together with Raluca Marinescu, Eduard Paul Enoiu, and Paul Pettersson.
 
 
  • ReSA: a requirements specification language based on constrained natural language, which uses domain knowledge to limit the syntax as well as the semantics, thus reducing ambiguity and improving consistency of specifications. Its tool support consists of an editor and a consistency checker via SMT solving in Z3. The method and tool have been developed by Cristina's ex-Ph.D. student Nesredin Mahmud, currently at QRTECH, Sweden. 
 
 

Editorial Boards:

 

PC Chair and Organizer of:

 

Program Committees (selection): 

  • 37th Annual IEEE Computer Software and Applications Conference (COMPSAC 2013), Workshops Chair, July 22-26, 2013 - Kyoto, Japan.
  • 6th IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE 2012), July 4-6, 2012 - Beijing, China.

 

 


[Show all publications]

[Google Scholar author page]

Latest publications:

Modeling and Verification of ROS Systems Using Stochastic Timed Automata (Jun 2024)
Peter Backeman, Cristina Seceleanu
MRTC Report, Mälardalen Real-Time Research Centre (MRTC 2024)

Synthesis and Verification of Mission Plans for Multiple Autonomous Agents under Complex Road Conditions (Jun 2024)
Rong Gu, Eduard Baranov , Afshin Ameri E., Eduard Paul Enoiu, Baran Çürüklü, Cristina Seceleanu, Axel Legay , Kristina Lundqvist
ACM Transactions on Software Engineering and Methodology (TOSEM)

Automating Test Generation of Industrial Control Software through a PLC-to-Python Translation Framework and Pynguin (Feb 2024)
Mikael Ebrahimi Salari, Eduard Paul Enoiu, Cristina Seceleanu, Wasif Afzal
30th Asia-Pacific Software Engineering Conference (APSEC2023)

Pattern-Based Verification of ROS 2 Nodes using UPPAAL (Sep 2023)
Lukas Dust, Rong Gu, Cristina Seceleanu, Mikael Ekström, Saad Mubeen
FMICS 2023 - International Conference on Formal Methods for Industrial Critical Systems (FMICS 2023)

Experimental Evaluation of Callback Behavior in ROS 2 Executors (Sep 2023)
Lukas Dust, Emil Persson, Mikael Ekström, Saad Mubeen, Cristina Seceleanu, Rong Gu
28th International Conference on Emerging Technologies and Factory Automation (ETFA 2023)

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)

Project TitleStatus
A Digital Twin Framework for Dynamic and Robust Distributed Systems active
A-CPS - Automation in High-performance Cyber Physical Systems Development finished
ACICS - Assured Cloud Platforms for Industrial Cyber-physical Systems finished
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
DPAC - Dependable Platforms for Autonomous systems and Control active
Embedded Systems Verification using Timed Automata Technology (VR) finished
Health5G: Future eHealth powered by 5G finished
InSecTT: Intelligent Secure Trustable Things active
MBAT - Combined Model-based Analysis and Testing (Artemis/Vinnova) finished
PERformance-based Formal modelling and Optimal tRaffic Management for movING-block RAILway signalling active
Performant and Flexible digital Systems through Verifiable AI active
PG-CBD-CVer – Component Verification finished
PROGRESS finished
PROMPT - Professional Master’s in Software Engineering (step II, phase B&C) active
Q-ImPreSS - Quality Impact Prediction for Evolving Service-oriented Software finished
RELIANT Industrial graduate school: Reliable, Safe and Secure Intelligent Autonomous Systems active
V-trustEE finished
VeriDevOps - Automated Protection and Prevention to Meet Security Requirements in DevOps Environments finished
VeriSpec - Structured Specification and Automated Verification for Automotive Functional Safety finished
PhD students supervised as main supervisor:

Ashalatha Kunnappilly (former)
Nesredin Mahmud (former)
Predrag Filipovikj (former)
Raluca Marinescu (former)
Rong Gu (former)
Simin Cai (former)

PhD students supervised as assistant supervisor:

Aida Causevic (former)
Aneta Vulgarakis Feljan (former)
Emil Persson
Jagadish Suryadevara (former)
Leo Hatvani (former)
Lukas Dust
Mikael Ebrahimi Salari
Stefan Björnander (former)