https://www.mdu.se/

mdu.sePublications
Change search
Link to record
Permanent link

Direct link
Sirjani, Marjan
Publications (10 of 65) Show all publications
Salimi, M., Loni, M., Afshar, S., Cicchetti, A. & Sirjani, M. (2025). ConstScene: A Dataset and Model for Advancing Robust Semantic Segmentation in Construction Environment. In: Lect. Notes Comput. Sci.: . Paper presented at Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (pp. 242-253). Springer Science and Business Media Deutschland GmbH
Open this publication in new window or tab >>ConstScene: A Dataset and Model for Advancing Robust Semantic Segmentation in Construction Environment
Show others...
2025 (English)In: Lect. Notes Comput. Sci., Springer Science and Business Media Deutschland GmbH , 2025, p. 242-253Conference paper, Published paper (Refereed)
Abstract [en]

The increasing demand for autonomous machines in construction environments necessitates the development of robust object detection algorithms that can perform effectively across various weather and environmental conditions. This paper introduces a new semantic segmentation dataset specifically tailored for construction sites, taking into account the diverse challenges posed by adverse weather and environmental conditions. The dataset is designed to enhance the training and evaluation of object detection models, fostering their adaptability and reliability in real-world construction applications. Our dataset comprises annotated images captured under a wide range of different weather conditions, including but not limited to sunny days, rainy periods, foggy atmospheres, and low-light situations. Additionally, environmental factors such as the existence of dirt/mud on the camera lens are integrated into the dataset through actual captures and synthetic generation to simulate the complex conditions prevalent in construction sites. We also generate synthetic images of the annotations including precise semantic segmentation masks for various objects commonly found in construction environments, such as wheel loader machines, personnel, cars, and structural elements. To demonstrate the dataset’s utility, we evaluate state-of-the-art object detection algorithms on our proposed benchmark. The results highlight the dataset’s success in adversarial training models across diverse conditions, showcasing its efficacy compared to existing datasets that lack such environmental variability.

Place, publisher, year, edition, pages
Springer Science and Business Media Deutschland GmbH, 2025
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 14893 LNCS
Keywords
Adversarial Attacks, Construction Environment, Dataset, Robust Object Detection, Semantic Segmentation, Adversarial machine learning, Camera lenses, Image annotation, Adverse weather, Autonomous machines, Condition, Construction sites, Environmental conditions, Object detection algorithms
National Category
Computer and Information Sciences
Identifiers
urn:nbn:se:mdh:diva-70418 (URN)10.1007/978-981-97-8705-0_16 (DOI)2-s2.0-85219205516 (Scopus ID)9789819787043 (ISBN)
Conference
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Available from: 2025-03-12 Created: 2025-03-12 Last updated: 2025-03-12Bibliographically approved
Moezkarimi, Z., Eriksson, K., Johansson, A. A., Bucaioni, A. & Sirjani, M. (2025). Harnessing ChatGPT for Model Transformation in Software Architecture: From UML State Diagrams to Rebeca Models for Formal Verification. In: Proc. - IEEE Int. Conf. Softw. Archit., ICSA-C: . Paper presented at Proceedings - 2025 IEEE 22nd International Conference on Software Architecture, ICSA-C 2025 (pp. 387-396). Institute of Electrical and Electronics Engineers (IEEE)
Open this publication in new window or tab >>Harnessing ChatGPT for Model Transformation in Software Architecture: From UML State Diagrams to Rebeca Models for Formal Verification
Show others...
2025 (English)In: Proc. - IEEE Int. Conf. Softw. Archit., ICSA-C, Institute of Electrical and Electronics Engineers (IEEE) , 2025, p. 387-396Conference paper, Published paper (Refereed)
Abstract [en]

Software architecture relies heavily on modeling techniques to describe, analyze, and verify system designs. The Unified Modeling Language (UML) is widely recognized as both a de facto and de jure standard for modeling various types of systems. While UML has formalized semantics that enhance consistency and precision, it is not inherently designed for model checking. Rebeca, an actor-based modeling language, is designed to enable formal verification of concurrent reactive systems. Previous efforts to bridge UML and Rebeca through model transformations have required combining multiple UML diagrams and a deep understanding of Rebeca, limiting practical applicability. In this paper, we explore the potential of leveraging large language models, specifically GPT-4, to automate the transformation of UML state diagrams into Rebeca models. Using a few-shot learning approach, we investigated the feasibility of this translation process. Initial results revealed that UML state diagrams alone were insufficient for generating accurate Rebeca models. To address this limitation, we augmented the diagrams with metadata, enabling GPT-4 to produce models that required only minor corrections to be executable in Rebeca's model-checking tool, Afra. Our findings demonstrate that LLMs hold promise in facilitating model transformations for software architecture, particularly for translating UML state diagrams into Rebeca models for formal verification. While not yet fully automated, this approach significantly reduces the effort required for transformation, paving the way for further research into the integration of LLMs into model-driven engineering practices.

Place, publisher, year, edition, pages
Institute of Electrical and Electronics Engineers (IEEE), 2025
Keywords
Formal methods, Large language model (LLM), Model transformation, Rebeca modeling language, Unified Modeling Language (UML) state diagram, Computer software reusability, Formal specification, Model checking, Problem oriented languages, Program translators, Actor-based modeling, Language model, Large language model, Modelling techniques, Models checking, Rebecum modeling language, State diagram, Unified Modeling, Unified modeling language state diagram, Formal verification
National Category
Computer and Information Sciences
Identifiers
urn:nbn:se:mdh:diva-72422 (URN)10.1109/ICSA-C65153.2025.00061 (DOI)2-s2.0-105007918537 (Scopus ID)9798331520908 (ISBN)
Conference
Proceedings - 2025 IEEE 22nd International Conference on Software Architecture, ICSA-C 2025
Available from: 2025-06-25 Created: 2025-06-25 Last updated: 2025-06-25Bibliographically approved
Marksteiner, S., Schoegler, D., Sirjani, M. & Sjödin, M. (2025). Learning single and compound-protocol automata and checking behavioral equivalences. International Journal on Software Tools for Technology Transfer
Open this publication in new window or tab >>Learning single and compound-protocol automata and checking behavioral equivalences
2025 (English)In: International Journal on Software Tools for Technology Transfer, ISSN 1433-2779, E-ISSN 1433-2787Article in journal (Refereed) Published
Abstract [en]

This paper presents a method and a practical implementation that complements traditional conformance testing. We infer a Mealy state machine of the system-under-test using active automata learning. This automaton is checked for bisimulation with a specification automaton modeled after the standard, which provides a strong verdict of conformance or nonconformance. We further present a method to learn models of multiple communication protocols running on the same device using a dispatcher system in conjunction with the same automata learning algorithms. We subsequently use similar checking methods to compare it with separately learned models. This allows for determining whether there is some interference or interaction between those protocols. In the practical execution of the system, we concentrate on lower levels of the Near-Field Communication (NFC, ISO/IEC 14443-3) and the Bluetooth Low-Energy (BLE) protocols. As a by-product, we share some observations of the performance of different learning algorithms and calibrations in the specific setting of ISO/IEC 14443-3, which is the difficulty to learn models of systems that a) consist of two very similar structures and b) timeout very frequently, as well as the role of conformance testing for compound models and speed optimizations for time-sensitive protocols.

Place, publisher, year, edition, pages
Springer Nature, 2025
Keywords
NFC, BLE, Automata learning, Protocol compliance, Bisimulation, Formal methods
National Category
Computer Sciences
Identifiers
urn:nbn:se:mdh:diva-71287 (URN)10.1007/s10009-025-00797-y (DOI)001467011100001 ()2-s2.0-105003122578 (Scopus ID)
Available from: 2025-04-30 Created: 2025-04-30 Last updated: 2025-05-07Bibliographically approved
Khosravi, R., Khamespanah, E., Ghassemi, F. & Sirjani, M. (2024). Actors Upgraded for Variability, Adaptability, and Determinism. In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics): (pp. 226-260). Springer Science and Business Media Deutschland GmbH, 14360 LNCS
Open this publication in new window or tab >>Actors Upgraded for Variability, Adaptability, and Determinism
2024 (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 , 2024, Vol. 14360 LNCS, p. 226-260Chapter in book (Other academic)
Abstract [en]

The Rebeca modeling language is designed as an imperative actor-based language with the goal of providing an easy-to-use language for modeling concurrent and distributed systems, with formal verification support. Rebeca has been extended to support time and probability. We extend Rebeca further with inheritance, polymorphism, interface declaration, and annotation mechanisms. These features allow us to handle variability within the model, support non-disruptive model evolution, and define method priorities. This enables Rebeca to be used more effectively in different domains, like in Software Product Lines, and holistic analysis of Cyber-Physical Systems. We develop specialized analysis techniques to support these extensions, partly integrated into Afra, the model checking tool of Rebeca.

Place, publisher, year, edition, pages
Springer Science and Business Media Deutschland GmbH, 2024
Keywords
Actor Languages, Cyber-Physical Systems, Model Checking, Variability Modeling, Cyber Physical System, Embedded systems, Modeling languages, Software design, Actor language, Concurrent and distributed systems, Cybe-physical systems, Different domains, Interface declaration, Model evolution, Models checking, Support time
National Category
Computer and Information Sciences
Identifiers
urn:nbn:se:mdh:diva-66094 (URN)10.1007/978-3-031-51060-1_9 (DOI)001215137600010 ()2-s2.0-85184279424 (Scopus ID)
Available from: 2024-02-20 Created: 2024-02-20 Last updated: 2025-04-07Bibliographically approved
Marksteiner, S., Sirjani, M. & Sjödin, M. (2024). Automated Passport Control: Mining and Checking Models of Machine Readable Travel Documents. In: ACM International Conference Proceeding Series: . Paper presented at 19th International Conference on Availability, Reliability and Security, ARES, Vienna, 30 July-2 August, 2024. Association for Computing Machinery, Article ID 171.
Open this publication in new window or tab >>Automated Passport Control: Mining and Checking Models of Machine Readable Travel Documents
2024 (English)In: ACM International Conference Proceeding Series, Association for Computing Machinery , 2024, article id 171Conference paper, Published paper (Refereed)
Abstract [en]

Passports are part of critical infrastructure for a very long time. They also have been pieces of automatically processable information devices, more recently through the ISO/IEC 14443 (Near-Field Communication - NFC) protocol. For obvious reasons, it is crucial that the information stored on devices are sufficiently protected. The International Civil Aviation Organization (ICAO) specifies exactly what information should be stored on electronic passports (also Machine Readable Travel Documents - MRTDs) and how and under which conditions they can be accessed. We propose a model-based approach for checking the conformance with this specification in an automated and very comprehensive manner: we use automata learning to learn a full model of passport documents and use trace equivalence and primitive model checking techniques to check the conformance with an automaton modeled after the ICAO standard. Since the full behavior is underspecified in the standard, we compare a part of the learned model and apply a primitive checking ruleset to assure proper authentication. The result is an automated (non-interactive), yet very thorough test for compliance, despite the underspecification. This approach can also be used with other applications for which a specification automaton can be modeled and is therefore broadly applicable.

Place, publisher, year, edition, pages
Association for Computing Machinery, 2024
Keywords
Automata Learning, Bisimulation, Formal Methods, NFC, Passports, Protocol Compliance, Automata theory, Automation, Compliance control, Model checking, Automaton learning, Bisimulations, Information devices, International Civil Aviation Organization, ISO/IEC-14443, Machine readable travel documents, Passport, Processable
National Category
Computer and Information Sciences
Identifiers
urn:nbn:se:mdh:diva-68173 (URN)10.1145/3664476.3670454 (DOI)001283894700098 ()2-s2.0-85200364225 (Scopus ID)9798400717185 (ISBN)
Conference
19th International Conference on Availability, Reliability and Security, ARES, Vienna, 30 July-2 August, 2024
Available from: 2024-08-14 Created: 2024-08-14 Last updated: 2024-12-11Bibliographically approved
Heip Hong, T., Sirjani, M., Moradi, F., Cicchetti, A. & Ciccozzi, F. (2024). Combining model-based development and formal verification of a complex ROS2 multi-robots system using Timed Rebeca. In: International Workshop on Reliability Engineering Methods for Autonomous Robots – REMARO 2024: . Paper presented at International Workshop on Reliability Engineering Methods for Autonomous Robots – REMARO 2024.
Open this publication in new window or tab >>Combining model-based development and formal verification of a complex ROS2 multi-robots system using Timed Rebeca
Show others...
2024 (English)In: International Workshop on Reliability Engineering Methods for Autonomous Robots – REMARO 2024, 2024Conference paper, Oral presentation with published abstract (Other academic)
Abstract [en]

ROS2 is an increasingly popular middleware framework for developing robotic applications. A ROS2 application is composed of nodes that run concurrently, coordinate with each other through asynchronous interfaces, and can be deployed in a distributed manner. Rebeca is an actor-based language for modelling asynchronous and concurrent systems. Timed Rebeca adds timing features to deal with timing requirements of real-time systems. The similarities in concurrency and message-based asynchronous interactions of reactive nodes, and the ability of modelling timed behaviours justify using Timed Rebeca models to assist the development and verification of ROS2 applications. Model-based development and model-checking techniques allow faster prototyping and earlier detection of system errors before developing the entire real system. However, there are challenges in bridging the gap between continuous behaviours of robotic systems and discrete states in a model for automatic verification, and between complex robotic computations and inequivalent programming facilities in a modelling language like Timed Rebeca. We investigated the problem systematically and have succeeded in modelling a realistic multiple autonomous mobile robots (AMR) system using Timed Rebeca, creating corresponding ROS2 demo code, and showing the match between the model and the program. Based on experiments, we demonstrated the value of the model in development and automatic formal verification of correctness properties (target reachability, collision freedom, and deadlock freedom). Our model-checking results show that certain system problems are not always detected through simulation. The modelling principles, modelling and implementation techniques that are created and used in this work can be generalized for many other cases. 

National Category
Computer and Information Sciences
Identifiers
urn:nbn:se:mdh:diva-69525 (URN)
Conference
International Workshop on Reliability Engineering Methods for Autonomous Robots – REMARO 2024
Available from: 2024-12-12 Created: 2024-12-12 Last updated: 2025-01-08Bibliographically approved
Moradi, F., Abbaspour Asadollah, S., Pourvatan, B., Moezkarimi, Z. & Sirjani, M. (2024). CRYSTAL framework: Cybersecurity assurance for cyber-physical systems. The Journal of logical and algebraic methods in programming, 139
Open this publication in new window or tab >>CRYSTAL framework: Cybersecurity assurance for cyber-physical systems
Show others...
2024 (English)In: The Journal of logical and algebraic methods in programming, ISSN 2352-2208, E-ISSN 2352-2216, ISSN 2352-2208, Vol. 139Article in journal (Refereed) Published
Abstract [en]

We propose CRYSTAL framework for automated cybersecurity assurance of cyber-physical systems (CPS) at design-time and runtime. We build attack models and apply formal verification to recognize potential attacks that may lead to security violations. We focus on both communication and computation in designing the attack models. We build a monitor to check and manage security at runtime and use a reference model, called Tiny Digital Twin, in detecting attacks. The Tiny Digital Twin is an abstract behavioral model that is automatically derived from the state space generated by model checking during design-time. Using CRYSTAL, we are able to systematically model and check complex coordinated attacks. In this paper we discuss the applicability of CRYSTAL in security analysis and attack detection for different case studies, Temperature Control System (TCS), Pneumatic Control System (PCS), and Secure Water Treatment System (SWaT). We provide a detailed description of the framework and explain how it works in different cases.

Place, publisher, year, edition, pages
Elsevier, 2024
Keywords
Cyber-Physical Systems (CPS), Formal verification, Model abstraction, Attack detection system, Runtime monitoring, Tiny Digital Twin
National Category
Computer Systems
Identifiers
urn:nbn:se:mdh:diva-66419 (URN)10.1016/j.jlamp.2024.100965 (DOI)001224282500001 ()2-s2.0-85189706631 (Scopus ID)
Available from: 2024-04-14 Created: 2024-04-14 Last updated: 2025-01-08Bibliographically approved
Abbaspour Asadollah, S., Imtiaz, S., Dehlaghi-Ghadim, A., Sjödin, M. & Sirjani, M. (2024). Enhancing Cybersecurity through Comprehensive Investigation of Data Flow-Based Attack Scenarios. Journal of Cybersecurity and Privacy, 4(4), 823-852
Open this publication in new window or tab >>Enhancing Cybersecurity through Comprehensive Investigation of Data Flow-Based Attack Scenarios
Show others...
2024 (English)In: Journal of Cybersecurity and Privacy, E-ISSN 2624-800X, Vol. 4, no 4, p. 823-852Article in journal (Refereed) Published
Abstract [en]

Integration of the Internet of Things (IoT) in industrial settings necessitates robust cybersecurity measures to mitigate risks such as data leakage, vulnerability exploitation, and compromised information flows. Recent cyberattacks on critical industrial systems have highlighted the lack of threat analysis in software development processes. While existing threat modeling frameworks such as STRIDE enumerate potential security threats, they often lack detailed mapping of the sequences of threats that adversaries might exploit to apply cyberattacks. Our study proposes an enhanced approach to systematic threat modeling and data flow-based attack scenario analysis for integrating cybersecurity measures early in the development lifecycle. We enhance the STRIDE framework by extending it to include attack scenarios as sequences of threats exploited by adversaries. This extension allows us to illustrate various attack scenarios and demonstrate how these insights can aid system designers in strengthening their defenses. Our methodology prioritizes vulnerabilities based on their recurrence across various attack scenarios, offering actionable insights for enhancing system security. A case study in the automotive industry illustrates the practical application of our proposed methodology, demonstrating significant improvements in system security through proactive threat modeling and analysis of attack impacts. The results of our study provide actionable insights to improve system design and mitigate vulnerabilities.

Place, publisher, year, edition, pages
Multidisciplinary Digital Publishing Institute (MDPI), 2024
Keywords
attack impact analysis, attack scenario, cyberattack, cybersecurity, cyber–physical system (CPS), STRIDE, threat modeling
National Category
Computer and Information Sciences
Identifiers
urn:nbn:se:mdh:diva-70692 (URN)10.3390/jcp4040039 (DOI)001466767400001 ()2-s2.0-85213453148 (Scopus ID)
Note

Article; Export Date: 31 March 2025; Cited By: 0; Correspondence Address: S. Abbaspour Asadollah; School of Innovation, Design and Engineering, Mälardalen University, Västerås, 721 23, Sweden; email: sara.abbaspour@mdu.se

Available from: 2025-04-01 Created: 2025-04-01 Last updated: 2025-04-23Bibliographically approved
Johansson, B., Pourvatan, B., Moezkarimi, Z., Papadopoulos, A. & Sirjani, M. (2024). Formal Verification of Consistency for Systems with Redundant Controllers. In: Electronic Proceedings in Theoretical Computer Science, EPTCS: . Paper presented at 6th Workshop on Models for Formal Analysis of Real Systems, MARS 2024, Luxembourg City, 6 April 2024 (pp. 169-191). Open Publishing Association, 399
Open this publication in new window or tab >>Formal Verification of Consistency for Systems with Redundant Controllers
Show others...
2024 (English)In: Electronic Proceedings in Theoretical Computer Science, EPTCS, Open Publishing Association , 2024, Vol. 399, p. 169-191Conference paper, Published paper (Refereed)
Abstract [en]

A potential problem that may arise in the domain of distributed control systems is the existence of more than one primary controller in redundancy plans that may lead to inconsistency. An algorithm called NRP FD is proposed to solve this issue by prioritizing consistency over availability. In this paper, we demonstrate how by using modeling and formal verification, we discovered an issue in NRP FD where we may have two primary controllers at the same time. We then provide a solution to mitigate the identified issue, thereby enhancing the robustness and reliability of such systems.

Place, publisher, year, edition, pages
Open Publishing Association, 2024
Series
Electronic Proceedings in Theoretical Computer Science, EPTCS, ISSN 20752180
Keywords
Controllers, Distributed parameter control systems, Finite difference method, Potential problems, Redundant controllers, Formal verification
National Category
Electrical Engineering, Electronic Engineering, Information Engineering
Identifiers
urn:nbn:se:mdh:diva-66500 (URN)10.4204/EPTCS.399.8 (DOI)001279518000001 ()2-s2.0-85190277600 (Scopus ID)
Conference
6th Workshop on Models for Formal Analysis of Real Systems, MARS 2024, Luxembourg City, 6 April 2024
Note

Conference code: 198553

Available from: 2024-04-25 Created: 2024-04-25 Last updated: 2024-12-04Bibliographically approved
Gu, R., Moezkarimi, Z. & Sirjani, M. (2024). Guess and Then Check: Controller Synthesis for Safe and Secure Cyber-Physical Systems. In: Lecture Notes in Computer Science: . Paper presented at 44th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2024, held as part of the 19th International Federated Conference on Distributed Computing Techniques, DisCoTec 2024, Groningen, Netherlands, 17 June through 21 June, 2024 (pp. 230-238). Springer Science+Business Media B.V.
Open this publication in new window or tab >>Guess and Then Check: Controller Synthesis for Safe and Secure Cyber-Physical Systems
2024 (English)In: Lecture Notes in Computer Science, Springer Science+Business Media B.V., 2024, p. 230-238Conference paper, Published paper (Refereed)
Abstract [en]

In this paper, we report our ongoing work on safe and secure controller synthesis for cyber-physical systems (CPS). Our approach separates the synthesis process into three phases, in which we alternatively perform exhaustive and selective exploration of the system’s state space. In this way, we combine the strengths of exhaustive search and learning to mitigate the state-space-explosion problem in controller synthesis while preserving the guarantee of safety and security. We implement the synthesis algorithms in the Rebeca (Reactive Objects Language) platform, which provides modelling, verification, and state-space visualization. We evaluate the new approach in an experiment, demonstrating the reduced number of explored states, which shows the potential of our approach for synthesizing safe and secure controllers for complex CPS.

Place, publisher, year, edition, pages
Springer Science+Business Media B.V., 2024
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 14678 LNCS
Keywords
Controllers, Cybersecurity, Embedded systems, Explosions, Modeling languages, Controller synthesis, Cybe-physical systems, Cyber-physical systems, Explosion problems, S state, State-space, State-space explosion, Synthesis process, Three phase, Three phasis, Cyber Physical System
National Category
Control Engineering
Identifiers
urn:nbn:se:mdh:diva-68046 (URN)10.1007/978-3-031-62645-6_13 (DOI)001273649500013 ()2-s2.0-85197245258 (Scopus ID)9783031626449 (ISBN)
Conference
44th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2024, held as part of the 19th International Federated Conference on Distributed Computing Techniques, DisCoTec 2024, Groningen, Netherlands, 17 June through 21 June, 2024
Available from: 2024-07-12 Created: 2024-07-12 Last updated: 2024-09-11Bibliographically approved
Organisations

Search in DiVA

Show all publications