-
LLM-based Property-based Test Generation for Guardrailing Cyber-Physical Systems
Authors:
Khashayar Etemadi,
Marjan Sirjani,
Mahshid Helali Moghadam,
Per Strandberg,
Paul Pettersson
Abstract:
Cyber-physical systems (CPSs) are complex systems that integrate physical, computational, and communication subsystems. The heterogeneous nature of these systems makes their safety assurance challenging. In this paper, we propose a novel automated approach for guardrailing cyber-physical systems using property-based tests (PBTs) generated by Large Language Models (LLMs). Our approach employs an LL…
▽ More
Cyber-physical systems (CPSs) are complex systems that integrate physical, computational, and communication subsystems. The heterogeneous nature of these systems makes their safety assurance challenging. In this paper, we propose a novel automated approach for guardrailing cyber-physical systems using property-based tests (PBTs) generated by Large Language Models (LLMs). Our approach employs an LLM to extract properties from the code and documentation of CPSs. Next, we use the LLM to generate PBTs that verify the extracted properties on the CPS. The generated PBTs have two uses. First, they are used to test the CPS before it is deployed, i.e., at design time. Secondly, these PBTs can be used after deployment, i.e., at run time, to monitor the behavior of the system and guardrail it against unsafe states. We implement our approach in ChekProp and conduct preliminary experiments to evaluate the generated PBTs in terms of their relevance (how well they match manually crafted properties), executability (how many run with minimal manual modification), and effectiveness (coverage of the input space partitions). The results of our experiments and evaluation demonstrate a promising path forward for creating guardrails for CPSs using LLM-generated property-based tests.
△ Less
Submitted 13 June, 2025; v1 submitted 29 May, 2025;
originally announced May 2025.
-
Hybrid Rebeca Revisited
Authors:
Fatemeh Ghassemi,
Saeed Zhiany,
Nesa Abbasimoghadam,
Ali Hodaei,
Ali Ataollahi,
József Kovács,
Erika Ábrahám,
Marjan Sirjani
Abstract:
Hybrid Rebeca is a modeling framework for asynchronous event-based cyber-physical systems (CPSs). In this work, we extend Hybrid Rebeca to allow the modeling of non-deterministic time behavior. Besides the syntactical extension, we formalize the semantics of the extended language in terms of Timed Transition Systems, and adapt a reachability analysis algorithm originally designed for hybrid automa…
▽ More
Hybrid Rebeca is a modeling framework for asynchronous event-based cyber-physical systems (CPSs). In this work, we extend Hybrid Rebeca to allow the modeling of non-deterministic time behavior. Besides the syntactical extension, we formalize the semantics of the extended language in terms of Timed Transition Systems, and adapt a reachability analysis algorithm originally designed for hybrid automata to be applicable to Hybrid Rebeca models. We prove the soundness of our approach and illustrate its applicability on a case study. The case study demonstrates that our dedicated algorithm is clearly superior to the alternative approach of transforming Hybrid Rebeca models to hybrid automata as an intermediate model and then applying the original reachability analysis method to this intermediate transformed models.
△ Less
Submitted 10 March, 2025; v1 submitted 5 November, 2024;
originally announced November 2024.
-
Formal Verification of Consistency for Systems with Redundant Controllers
Authors:
Bjarne Johansson,
Bahman Pourvatan,
Zahra Moezkarimi,
Alessandro Papadopoulos,
Marjan Sirjani
Abstract:
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…
▽ More
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.
△ Less
Submitted 27 March, 2024;
originally announced March 2024.
-
ConstScene: Dataset and Model for Advancing Robust Semantic Segmentation in Construction Environments
Authors:
Maghsood Salimi,
Mohammad Loni,
Sara Afshar,
Antonio Cicchetti,
Marjan Sirjani
Abstract:
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…
▽ More
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.
△ Less
Submitted 19 January, 2024; v1 submitted 27 December, 2023;
originally announced December 2023.
-
Timed Actors and Their Formal Verification
Authors:
Marjan Sirjani,
Ehsan Khamespanah
Abstract:
In this paper we review the actor-based language, Timed Rebeca, with a focus on its formal semantics and formal verification techniques. Timed Rebeca can be used to model systems consisting of encapsulated components which communicate by asynchronous message passing. Messages are put in the message buffer of the receiver actor and can be seen as events. Components react to these messages/events…
▽ More
In this paper we review the actor-based language, Timed Rebeca, with a focus on its formal semantics and formal verification techniques. Timed Rebeca can be used to model systems consisting of encapsulated components which communicate by asynchronous message passing. Messages are put in the message buffer of the receiver actor and can be seen as events. Components react to these messages/events and execute the corresponding message/event handler. Real-time features, like computation delay, network delay and periodic behavior, can be modeled in the language. We explain how both Floating-Time Transition System (FTTS) and common Timed Transition System (TTS) can be used as the semantics of such models and the basis for model checking. We use FTTS when we are interested in event-based properties, and it helps in state space reduction. For checking the properties based on the value of variables at certain point in time, we use the TTS semantics. The model checking toolset supports schedulability analysis, deadlock and queue-overflow check, and assertion based verification of Timed Rebeca models. TCTL model checking based on TTS is also possible but is not integrated in the tool.
△ Less
Submitted 13 September, 2023;
originally announced September 2023.
-
Schedulability Analysis of WSAN Applications: Outperformance of A Model Checking Approach
Authors:
Ehsan Khamespanah,
Morteza Mohaqeqi,
Mohammad Ashjaei,
Marjan Sirjani
Abstract:
Wireless sensor and actuator networks (WSAN) are real-time systems which demand high degrees of reliability requirements. To ensure this level of reliability, different analysis approaches have been proposed for WSAN applications. Among different alternatives, analytical analysis and model checking are two common approaches which are widely used for the formal analysis of WSAN applications. Analyt…
▽ More
Wireless sensor and actuator networks (WSAN) are real-time systems which demand high degrees of reliability requirements. To ensure this level of reliability, different analysis approaches have been proposed for WSAN applications. Among different alternatives, analytical analysis and model checking are two common approaches which are widely used for the formal analysis of WSAN applications. Analytical approaches apply constraint satisfaction methods, whereas model checking generates explicit states of models and analyze them. In this paper, we compare the two approaches in schedulability analysis of WSAN applications using an application for monitoring and control of civil infrastructures, which is implemented on the Imote2 wireless sensor platform. We show how the highest possible data acquisition frequency for this application is computed while meeting the deadlines, and compare the results of the two approaches as well as their scalability, extensibility, and flexibility.
△ Less
Submitted 30 April, 2022;
originally announced May 2022.
-
Specification and Verification of Timing Properties in Interoperable Medical Systems
Authors:
Mahsa Zarneshan,
Fatemeh Ghassemi,
Ehsan Khamespanah,
Marjan Sirjani,
John Hatcliff
Abstract:
To support the dynamic composition of various devices/apps into a medical system at point-of-care, a set of communication patterns to describe the communication needs of devices has been proposed. To address timing requirements, each pattern breaks common timing properties into finer ones that can be enforced locally by the components. Common timing requirements for the underlying communication su…
▽ More
To support the dynamic composition of various devices/apps into a medical system at point-of-care, a set of communication patterns to describe the communication needs of devices has been proposed. To address timing requirements, each pattern breaks common timing properties into finer ones that can be enforced locally by the components. Common timing requirements for the underlying communication substrate are derived from these local properties. The local properties of devices are assured by the vendors at the development time. Although organizations procure devices that are compatible in terms of their local properties and middleware, they may not operate as desired. The latency of the organization network interacts with the local properties of devices. To validate the interaction among the timing properties of components and the network, we formally specify such systems in Timed Rebeca. We use model checking to verify the derived timing requirements of the communication substrate in terms of the network and device models. We provide a set of templates as a guideline to specify medical systems in terms of the formal model of patterns. A composite medical system using several devices is subject to state-space explosion. We extend the reduction technique of Timed Rebeca based on the static properties of patterns. We prove that our reduction is sound and show the applicability of our approach in reducing the state space by modeling two clinical scenarios made of several instances of patterns.
△ Less
Submitted 31 May, 2022; v1 submitted 7 December, 2020;
originally announced December 2020.
-
Magnifier: A Compositional Analysis Approach for Autonomous Traffic Control
Authors:
Maryam Bagheri,
Marjan Sirjani,
Ehsan Khamespanah,
Christel Baier,
Ali Movaghar
Abstract:
Autonomous traffic control systems are large-scale systems with critical goals. Due to the dynamic nature of the surrounding world of these systems, assuring the satisfaction of their properties at runtime and in the presence of a change is important. A prominent approach to assure the correct behavior of these systems is verification at runtime, which has strict time and memory limitations. To ta…
▽ More
Autonomous traffic control systems are large-scale systems with critical goals. Due to the dynamic nature of the surrounding world of these systems, assuring the satisfaction of their properties at runtime and in the presence of a change is important. A prominent approach to assure the correct behavior of these systems is verification at runtime, which has strict time and memory limitations. To tackle these limitations, we propose Magnifier, an iterative, incremental, and compositional verification approach that operates on a component-based model. The Magnifier idea is zooming on the component affected by a change, verifying the correctness of properties of interest of the system after adapting the component to the change, and then zooming out and tracing the change if it propagates. If the change propagates, all components affected by the change are adapted and are composed to form a new component. Magnifier repeats the same process for the new component. This iterative process terminates whenever the propagation of the change stops. In Magnifier, we use the Coordinated Adaptive Actor model (CoodAA) of traffic control systems. We present a formal semantics for CoodAA as a network of Timed Input-Output Automata (TIOAs). The change does not propagate if TIOAs of the adapted component and its environment are compatible. We implement our approach in Ptolemy II. The results of our experiments indicate that the proposed approach improves the verification time and the memory consumption compared to a non-compositional approach.
△ Less
Submitted 11 March, 2021; v1 submitted 20 April, 2019;
originally announced May 2019.
-
VeriVANca: An Actor-Based Framework for Formal Verification of Warning Message Dissemination Schemes in VANETs
Authors:
Farnaz Yousefi,
Ehsan Khamespanah,
Mohammed Gharib,
Marjan Sirjani,
Ali Movaghar
Abstract:
One of the applications of vehicular ad-hoc networks is warning message dissemination among vehicles in dangerous situations to prevent more damage. The only communication mechanism for message dissemination is multi-hop broadcast; in which, forwarding a received message have to be regulated using a scheme regarding the selection of forwarding nodes. When analyzing these schemes, simulation-based…
▽ More
One of the applications of vehicular ad-hoc networks is warning message dissemination among vehicles in dangerous situations to prevent more damage. The only communication mechanism for message dissemination is multi-hop broadcast; in which, forwarding a received message have to be regulated using a scheme regarding the selection of forwarding nodes. When analyzing these schemes, simulation-based frameworks fail to provide guaranteed analysis results due to the high level of concurrency in this application. Therefore, there is a need to use model checking approaches for achieving reliable results. In this paper, we have developed a framework called VeriVANca, to provide model checking facilities for the analysis of warning message dissemination schemes in VANETs. To this end, an actor-based modeling language, Rebeca, is used which is equipped with a variety of model checking engines. To illustrate the applicability of VeriVANca, modeling and analysis of two warning message dissemination schemes are presented. Some scenarios for these schemes are presented to show that concurrent behaviors of the system components may cause uncertainty in both behavior and performance which may not be detected by simulation-based techniques. Furthermore, the scalability of VeriVANca is examined by analyzing a middle-sized model.
△ Less
Submitted 16 April, 2019;
originally announced May 2019.
-
Modelling and Simulation of Asynchronous Real-Time Systems using Timed Rebeca
Authors:
Luca Aceto,
Matteo Cimini,
Anna Ingolfsdottir,
Arni Hermann Reynisson,
Steinar Hugi Sigurdarson,
Marjan Sirjani
Abstract:
In this paper we propose an extension of the Rebeca language that can be used to model distributed and asynchronous systems with timing constraints. We provide the formal semantics of the language using Structural Operational Semantics, and show its expressiveness by means of examples. We developed a tool for automated translation from timed Rebeca to the Erlang language, which provides a first im…
▽ More
In this paper we propose an extension of the Rebeca language that can be used to model distributed and asynchronous systems with timing constraints. We provide the formal semantics of the language using Structural Operational Semantics, and show its expressiveness by means of examples. We developed a tool for automated translation from timed Rebeca to the Erlang language, which provides a first implementation of timed Rebeca. We can use the tool to set the parameters of timed Rebeca models, which represent the environment and component variables, and use McErlang to run multiple simulations for different settings. Timed Rebeca restricts the modeller to a pure asynchronous actor-based paradigm, where the structure of the model represents the service oriented architecture, while the computational model matches the network infrastructure. Simulation is shown to be an effective analysis support, specially where model checking faces almost immediate state explosion in an asynchronous setting.
△ Less
Submitted 31 July, 2011;
originally announced August 2011.
