https://www.mdu.se/

mdu.sePublications
Change search
Link to record
Permanent link

Direct link
Alternative names
Publications (10 of 150) Show all publications
Seceleanu, C. (2025). A Quantum-Like Intellect: Celebrating the Profound Impact of Tiziana Margaria, Professor and Friend. In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics): (pp. 50-54). Springer Science and Business Media Deutschland GmbH, 15240 LNCS
Open this publication in new window or tab >>A Quantum-Like Intellect: Celebrating the Profound Impact of Tiziana Margaria, Professor and Friend
2025 (English)In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Springer Science and Business Media Deutschland GmbH , 2025, Vol. 15240 LNCS, p. 50-54Chapter in book (Other academic)
Abstract [en]

It is not often that someone possesses qualities akin to those found in quantum phenomena, such as cleverness and quick reactions. Hence, I consider myself privileged that I have met and collaborated for many years with Tiziana Margaria, a renowed professor of Software Engineering and respected friend. This personal note that I dedicate to her tries to reflect both the professional and personal admiration that I hold for her. 

Place, publisher, year, edition, pages
Springer Science and Business Media Deutschland GmbH, 2025
Keywords
Quantum phenomena, Software engineering
National Category
Software Engineering
Identifiers
urn:nbn:se:mdh:diva-69014 (URN)10.1007/978-3-031-73887-6_5 (DOI)2-s2.0-85208027730 (Scopus ID)978-3-031-73887-6 (ISBN)
Available from: 2024-11-13 Created: 2024-11-13 Last updated: 2024-11-13Bibliographically approved
Filipovikj, P., Mahmud, N., Seceleanu, C., Rodriguez-Navas, G., Ljungkrantz, O. & Lönn, H. (2025). SIMPPAAL: A Framework for Statistical Model Checking of Industrial Simulink Models. In: Lecture Notes in Computer Science: . Paper presented at 12th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2024, Crete, Greece, 27-31 October, 2024 (pp. 220-246). Springer Science+Business Media B.V.
Open this publication in new window or tab >>SIMPPAAL: A Framework for Statistical Model Checking of Industrial Simulink Models
Show others...
2025 (English)In: Lecture Notes in Computer Science, Springer Science+Business Media B.V., 2025, p. 220-246Conference paper, Published paper (Refereed)
Abstract [en]

The evolution of automotive systems has been rapid. Nowadays, electronic brains control dozens of functions in vehicles, like braking, cruising, etc. Model-based design approaches, in environments such as MATLAB Simulink, seem to help in addressing the ever-increasing need to enhance quality, and manage complexity, by supporting functional design from predefined block libraries, which can be simulated and analyzed for hidden errors, but also used for code generation. For this reason, providing assurance that Simulink models fulfill given functional and timing requirements is desirable. In this paper, we propose formal syntax and semantics of Simulink blocks and their composition, and introduce the tool SIMPPAAL that automates a previously introduced pattern-based, execution-order preserving transformation of Simulink atomic and composite blocks into stochastic timed automata. The resulting model can then be analyzed formally with UPPAAL Statistical Model Checker. We validate the approach on an industrial prototype called the Brake-by-Wire system. This work enables the formal analysis of industrial Simulink models, by automatically generating their semantic counterpart.

Place, publisher, year, edition, pages
Springer Science+Business Media B.V., 2025
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 15221 LNCS
Keywords
MATLAB, Model checking, Stochastic control systems, Automotive Systems, Block libraries, Brain controls, Electronic brains, Functional design, MATLAB/ SIMULINK, Model-based design approaches, Simulink, Simulink models, Statistical model checking, Stochastic systems
National Category
Computer Systems
Identifiers
urn:nbn:se:mdh:diva-69177 (URN)10.1007/978-3-031-75380-0_13 (DOI)2-s2.0-85208558018 (Scopus ID)9783031753794 (ISBN)
Conference
12th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2024, Crete, Greece, 27-31 October, 2024
Available from: 2024-11-20 Created: 2024-11-20 Last updated: 2024-11-20Bibliographically approved
Hansson, H., Norström, C. & Seceleanu, C. (2025). Wang at MDU in a Nutshell. In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics): (pp. 8-11). Springer Science+Business Media B.V., 15230 LNCS
Open this publication in new window or tab >>Wang at MDU in a Nutshell
2025 (English)In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Springer Science+Business Media B.V., 2025, Vol. 15230 LNCS, p. 8-11Chapter in book (Other academic)
Abstract [en]

In the labyrinthine world of real-time systems, few names resonate as powerfully as that of Prof. Wang Yi. As the co-inventor of the UPPAAL model checker, alongside Prof. Kim G. Larsen and Prof. Paul Pettersson, Wang has charted new territories in computer science, setting a benchmark that stands as a testament to excellence.

Place, publisher, year, edition, pages
Springer Science+Business Media B.V., 2025
Series
Lecture Notes in Computer Science, ISSN 03029743 ; 15230
Keywords
Embedded systems, Interactive computer systems, Model checking, Lars-en, Model checker, Real - Time system, Real time systems
National Category
Computer Sciences
Identifiers
urn:nbn:se:mdh:diva-69842 (URN)10.1007/978-3-031-73751-0_2 (DOI)2-s2.0-85214351655 (Scopus ID)
Available from: 2025-01-23 Created: 2025-01-23 Last updated: 2025-01-23Bibliographically approved
Dust, L., Ekström, M., Gu, R., Mubeen, S. & Seceleanu, C. (2024). A Model-Based Methodology for Automated Verification of ROS 2 Systems. In: Proceedings - 2024 IEEE/ACM 6th International Workshop on Robotics Software Engineering, RoSE 2024: . Paper presented at 6th International Workshop on Robotics Software Engineering, RoSE 2024, co-located with the 46th International Conference on SoftwareLisbon15 April 2024 (pp. 35-42).
Open this publication in new window or tab >>A Model-Based Methodology for Automated Verification of ROS 2 Systems
Show others...
2024 (English)In: Proceedings - 2024 IEEE/ACM 6th International Workshop on Robotics Software Engineering, RoSE 2024, 2024, p. 35-42Conference paper, Published paper (Refereed)
Abstract [en]

To simplify the formal verification of ROS 2-based applications, in this paper, we propose a novel approach to the automation of their model-based verification using model-driven engineering techniques. We propose a methodology starting with ROS 2 execution traces, generated by ROS2_tracing and using models and model transformations in Eclipse to automatically initialize pre-defined formal model templates in UPPAAL, with system parameters. While the methodology targets the simplification of formal verification for robotics developers as users, the implementation is at an early stage and the toolchain is not fully implemented and evaluated. Hence, this paper targets tool developers and researchers to give a first overview of the underlying idea of automating ROS 2 verification.

Hence, we propose a toolchain that supports verification of implemented and conceptual ROS 2 systems, as well as iterative verification of timing and scheduling parameters. We propose using four different model representations, based on the ROS2_tracing output and self-designed Eclipse Ecore metamodels to model the system from a structural and verification perspective. The different model representations allow traceability throughout the modeling and verification process.Last, an initial proof of concept is implemented containing the core elements of the proposed toolchain and validated given a small ROS 2 system. 

National Category
Robotics and automation Embedded Systems Computer Sciences
Identifiers
urn:nbn:se:mdh:diva-67506 (URN)10.1145/3643663.3643970 (DOI)001285454300006 ()2-s2.0-85200922593 (Scopus ID)9798400705663 (ISBN)
Conference
6th International Workshop on Robotics Software Engineering, RoSE 2024, co-located with the 46th International Conference on SoftwareLisbon15 April 2024
Available from: 2024-06-14 Created: 2024-06-14 Last updated: 2025-02-05Bibliographically approved
Seceleanu, T., Xiong, N., Enoiu, E. P. & Seceleanu, C. (2024). Building a Digital Twin Framework for Dynamic and Robust Distributed Systems. In: Lect. Notes Comput. Sci.: . Paper presented at 8th International Conference on Engineering of Computer-Based Systems, ECBS 2023, Västerås, 16 October 2023 through 18 October 2023 (pp. 254-258). Springer Science and Business Media Deutschland GmbH
Open this publication in new window or tab >>Building a Digital Twin Framework for Dynamic and Robust Distributed Systems
2024 (English)In: Lect. Notes Comput. Sci., Springer Science and Business Media Deutschland GmbH , 2024, p. 254-258Conference paper, Published paper (Refereed)
Abstract [en]

Digital Twins (DTs) serve as the backbone of Industry 4.0, offering virtual representations of actual systems, enabling accurate simulations, analysis, and control. These representations help in predicting system behaviour, facilitating multiple real-time tests, and reducing risks and costs while identifying optimization areas. DTs meld cyber and physical realms, accelerating the design and modelling of sustainable innovations. Despite their potential, the complexity of DTs presents challenges in their industrial application. We sketch here an approach to build an adaptable and trustable framework for building and operating DT systems, which is the basis for the academia-industry project A Digital Twin Framework for Dynamic and Robust Distributed Systems (D-RODS). D-RODS aims to address the challenges above, aiming to advance industrial digitalization and targeting areas like system efficiency, incorporating AI and verification techniques with formal support. 

Place, publisher, year, edition, pages
Springer Science and Business Media Deutschland GmbH, 2024
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 14390 LNCS
Keywords
AI, digital twins, industrial automation, resource utilization, verification and validation, Actual system, Analysis and controls, Distributed systems, Resources utilizations, Simulation analysis, Simulation control, System behaviors, Verification-and-validation, Virtual representations, Artificial intelligence
National Category
Computer Sciences
Identifiers
urn:nbn:se:mdh:diva-65247 (URN)10.1007/978-3-031-49252-5_22 (DOI)2-s2.0-85180149728 (Scopus ID)9783031492518 (ISBN)
Conference
8th International Conference on Engineering of Computer-Based Systems, ECBS 2023, Västerås, 16 October 2023 through 18 October 2023
Available from: 2024-01-03 Created: 2024-01-03 Last updated: 2024-01-03Bibliographically approved
Naeem, M., Gu, R., Seceleanu, C., Guldstrand Larsen, K., Nielsen, B. & Albano, M. (2024). Energy-Efficient Motion Planning for Autonomous Vehicles Using Uppaal  Stratego. In: Theoretical Aspects of Software Engineering. TASE 2024. Lecture Notes in Computer Science.: . Paper presented at Theoretical Aspects of Software Engineering. TASE 2024 (pp. 356-373). Springer, 14777
Open this publication in new window or tab >>Energy-Efficient Motion Planning for Autonomous Vehicles Using Uppaal  Stratego
Show others...
2024 (English)In: Theoretical Aspects of Software Engineering. TASE 2024. Lecture Notes in Computer Science., Springer, 2024, Vol. 14777, p. 356-373Conference paper, Published paper (Refereed)
Abstract [en]

Energy-efficient motion planning for autonomous battery-powered vehicles is crucial to increase safety and efficiency by avoiding frequent battery recharge. This paper proposes algorithms for synthesizing energy- and time-efficient motion plans for battery-powered autonomous vehicles. We use stochastic hybrid games to model an appropriate abstraction of the autonomous vehicle and the environment. Based on the model, we synthesize energy- and time-efficient motion plans using Q-learning in Uppaal  Stratego. Via experiments, we show that pure Q-learning is insufficient when the problem becomes complex, e.g., Motion Planning (MOP) in large environments. To address this issue, we propose Concatenated Motion Planning (CoMOP), which divides the environment into several regions, synthesizes a motion plan in each region and concatenates the local plans into an entire motion plan for the whole environment. CoMOP enhances the applicability of Q-learning to large and complex environments, reduces synthesis time, and provides efficient navigation and precise motion plans. We conduct experiments with our approaches in an industrial use case. The results show that CoMOP outperforms MOP regarding synthesis time and the ability to deal with complex models. Moreover, we compare the energy- and time-efficient strategies and visualize their differences on different terrains.

Place, publisher, year, edition, pages
Springer, 2024
Series
Lecture Notes in Computer Science, ISSN 0302-9743, E-ISSN 1611-3349
National Category
Electrical Engineering, Electronic Engineering, Information Engineering
Identifiers
urn:nbn:se:mdh:diva-69378 (URN)10.1007/978-3-031-64626-3_21 (DOI)001315662800021 ()9783031646256 (ISBN)9783031646263 (ISBN)
Conference
Theoretical Aspects of Software Engineering. TASE 2024
Available from: 2024-12-09 Created: 2024-12-09 Last updated: 2024-12-20Bibliographically approved
ter Beek, M. H., Chapman, R., Cleaveland, R., Garavel, H., Gu, R., ter Horst, I., . . . Zhang, L. (2024). Formal Methods in Industry. Formal Aspects of Computing
Open this publication in new window or tab >>Formal Methods in Industry
Show others...
2024 (English)In: Formal Aspects of Computing, ISSN 0934-5043, E-ISSN 1433-299XArticle in journal (Refereed) Published
Abstract [en]

Formal methods encompass a wide choice of techniques and tools for the specification, development, analysis, and verification of software and hardware systems. Formal methods are widely applied in industry, in activities ranging from the elicitation of requirements and the early design phases all the way to the deployment, configuration, and runtime monitoring of actual systems. Formal methods allow one to precisely specify the environment in which a system operates, the requirements and properties that the system should satisfy, the models of the system used during the various design steps, and the code embedded in the final implementation, as well as to express conformance relations between these specifications. We present a broad scope of successful applications of formal methods in industry, not limited to the well-known success stories from the safety-critical domain, like railways and other transportation systems, but also covering other areas such as lithography manufacturing and cloud security in e-commerce, to name but a few. We also report testimonies from a number of representatives from industry who, either directly or indirectly, use or have used formal methods in their industrial project endeavours. These persons are spread geographically, including Europe, Asia, North and South America, and the involved projects witness the large coverage of applications of formal methods, not limited to the safety-critical domain. We thus make a case for the importance of formal methods, and in particular of the capacity to abstract and mathematical reasoning that are taught as part of any formal methods course. These are fundamental Computer Science skills that graduates should profit from when working as computer scientists in industry, as confirmed by industry representatives.

National Category
Electrical Engineering, Electronic Engineering, Information Engineering
Identifiers
urn:nbn:se:mdh:diva-69381 (URN)10.1145/3689374 (DOI)
Available from: 2024-12-09 Created: 2024-12-09 Last updated: 2024-12-09Bibliographically approved
Backeman, P. & Seceleanu, C. (2024). Modeling and Verification of ROS SystemsUsing Stochastic Timed Automata.
Open this publication in new window or tab >>Modeling and Verification of ROS SystemsUsing Stochastic Timed Automata
2024 (English)Report (Other academic)
Abstract [en]

Robotic systems often operate under real-time constraints,requiring timely responses to sensor inputs. Early consideration of suchrequirements during design is advantageous. The Robot Operating System(ROS) provides a mature framework for system setup and communication,with ROS2 offering real-time capabilities. However, determiningthe maximum reaction time within a ROS network is intricatedue to complex variable processing and scheduling, especially with periodicand event-triggered tasks. In this report, we propose a model ofROS-based structural designs with timed automata semantics, facilitatingreal-time behavior analysis. We extend this model to incorporatenon-deterministic execution time and probabilistic loads, employing statisticalmodel checking (SMC) for scalability and accuracy. We compareagainst previous work to confirm the validity of our approach.

Publisher
p. 24
National Category
Computer and Information Sciences
Identifiers
urn:nbn:se:mdh:diva-69210 (URN)
Available from: 2024-11-26 Created: 2024-11-26 Last updated: 2024-11-26Bibliographically approved
Kofroň, J., Seceleanu, C. & Margaria, T. (2024). Preface. In: Lecture Notes in Computer Science: . Paper presented at 8th International Conference on Engineering of Computer-Based Systems, ECBS 2023, Västerås, 16 October 2023 through 18 October 2023. Springer Science and Business Media Deutschland GmbH, 14390
Open this publication in new window or tab >>Preface
2024 (English)In: Lecture Notes in Computer Science, Springer Science and Business Media Deutschland GmbH , 2024, Vol. 14390Conference paper, Published paper (Refereed)
Place, publisher, year, edition, pages
Springer Science and Business Media Deutschland GmbH, 2024
National Category
Computer Sciences
Identifiers
urn:nbn:se:mdh:diva-65240 (URN)2-s2.0-85180298994 (Scopus ID)9783031492518 (ISBN)
Conference
8th International Conference on Engineering of Computer-Based Systems, ECBS 2023, Västerås, 16 October 2023 through 18 October 2023
Available from: 2024-01-03 Created: 2024-01-03 Last updated: 2024-01-03Bibliographically approved
Gu, R., Baranov, E., Ameri, A., Enoiu, E. P., Curuklu, B., Seceleanu, C., . . . Lundqvist, K. (2024). Synthesis and Verification of Mission Plans for Multiple Autonomous Agents under Complex Road Conditions. ACM Transactions on Software Engineering and Methodology, 33(7), 1-46, Article ID 173.
Open this publication in new window or tab >>Synthesis and Verification of Mission Plans for Multiple Autonomous Agents under Complex Road Conditions
Show others...
2024 (English)In: ACM Transactions on Software Engineering and Methodology, ISSN 1049-331X, Vol. 33, no 7, p. 1-46, article id 173Article in journal (Other academic) Published
Abstract [en]

Mission planning for multi-agent autonomous systems aims to generate feasible and optimal mission plans that satisfy the given requirements. In this article, we propose a mission-planning methodology that combines (i) a path-planning algorithm for synthesizing path plans that are safe in environments with complex road conditions, and (ii) a task-scheduling method for synthesizing task plans that schedule the tasks in the right and fastest order, taking into account the planned paths. The task-scheduling method is based on model checking, which provides means of automatically generating task execution orders that satisfy the requirements and ensure the correctness and efficiency of the plans by construction. We implement our approach in a tool named MALTA, which offers a user-friendly GUI for configuring mission requirements,  a module for path planning, an integration with the model checker UPPAAL, and functions for automatic generation of formal models, and parsing of the execution traces of models. Experiments with the tool demonstrate its applicability and performance in various configurations of an industrial case study of an autonomous quarry. We also show the adaptability of our tool by employing it on a special case of the industrial case study.

National Category
Computer Sciences
Identifiers
urn:nbn:se:mdh:diva-58047 (URN)10.1145/3672445 (DOI)2-s2.0-85202215443 (Scopus ID)
Available from: 2022-04-20 Created: 2022-04-20 Last updated: 2024-12-09Bibliographically approved
Organisations
Identifiers
ORCID iD: ORCID iD iconorcid.org/0000-0003-2870-2680

Search in DiVA

Show all publications