Abstract In many verification tasks, system models do not correspond to the focused and idealized models that appear in research literature. In practice, models usually contain components and execution paths that are irrelevant to the property being verified or have only a limited effect on it. Compositional verification presents a practical method for coping with the larger and less targeted models found in such settings. In this paper, we present an automated compositional framework for verifying timed safety properties in networks of timed automata. We show as a main result that the weakest environment assumption, commonly used in compositional reasoning, may in general fail to be recognizable within the timed automata formalism. This negative result motivates shifting the focus to the complement language of violation-inducing timed words, for which we establish recognizability using timed automata with silent transitions. We provide an algorithm for its construction and reduce its size by retaining only the parts directly relevant to the property. The synthesized assumption is later applied to verify the original system. This provides a sound and complete basis for compositional verification of timed automata, including the novel ability to handle automata with multiple clocks and non-deterministic behavior. Our results broaden the applicability of assume–guarantee verification techniques in timed automata and show substantial reductions in the size of the state-space, outperforming monolithic methods on a range of case studies.

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. However, challenging conditions at construction sites, such as mud splashes and vibrations, can degrade object detection performance by causing sensor occlusions and image blurriness. Traditional adversarial training methods, which enhance model robustness by using perturbed data, are limited in construction environments due to the scarcity of diverse real-world adversarial data and the dynamic nature of construction environments. To overcome these challenges, this paper explores utilizing few-shot learning (FSL) to improve the generalization performance and robustness of object detection models. FSL enables models to adapt quickly using minimal data, reducing the need for large datasets. In addition, we identify an often-overlooked issue: the hyperparameters used in FSL training are typically not optimized for this unique paradigm. To address this, we combine FSL with hyperparameter optimization to enhance model performance across multiple small-scale datasets. Experimental results demonstrate that our approach improves model performance on the ConstScene dataset over the default training paradigm. The code for this study is available at here.

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 behaviour. 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 two examples: a thermostat with alarm and a simplified brake-by-wire system with anti-lock braking system. We demonstrate 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 these intermediate transformed models.

Abstract 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.

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.

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.

This paper presents a method for detecting cyber-attacks in cyber-physical systems using a monitor. The method employs an abstract model called Tiny Twin, which is built at design time and is used at runtime to detect inconsistencies. Tiny Twin is a state transition system that represents the observable behavior of the system from the monitor point of view. We model the behavior of the system in the Rebeca modeling language and use Afra model checker to generate the state space. The Tiny Twin is built automatically, by abstracting the state space while keeping the observable actions and preserving the trace equivalence. For doing that we had to solve the complexities in the state space introduced by time-shifts, nondeterministic assignments and abstraction of internal actions. We formally define the state space as Concise Rebeca Timed Transition System (CRTTS), and then map CRTTS to an LTS. The LTS is then fed to a tool to abstract away the non-observable actions.

Conducting interactions between shared-purpose organizations that are not entirely trustworthy of each other without centralized oversight is an idea that emerged with the advent of private blockchains such as Hyperledger Fabric and its smart contracts. It is critical to check contracts to ensure their proper functionality, as organizations may collaborate with competitors. Due to the new architecture of Hyperledger Fabric, tools in this area are limited. To formally verify the source code of contracts, we mapped Fabric contract concepts into the Rebeca modeling language. Rebeca is an actor-based language that enables the modeling of concurrent and distributed systems and is supported by a model checking tool, Afra. We have identified vulnerabilities such as deadlock and starvation by examining the desired properties. Using the model checking approach, we could debug the code and hence benefit from speeding up the transactions, creating fewer extra blocks, requiring less storage space to store the ledger, and avoiding wasting computing resources.

Wireless sensor and actuator networks (WSAN) are real-time systems which demand timing requirements. To ensure this level of requirements, different timing analysis approaches have been proposed for WSAN systems. Among different alternatives, analytical analysis and model checking approaches are two common ones which are widely used for the timing analysis of WSAN systems. Analytical approaches apply worst-case response time analysis techniques, whereas model checking generates explicit states of models to analyze them. In this paper, we develop schedulability analysis techniques based on two approaches, i.e., analytical and model checking approaches. We apply and compare the proposed analysis approaches on WSAN systems with an application in monitoring and control of civil infrastructures implemented on the Imote2 wireless sensor platform. We show that the highest possible data acquisition frequency for this application is computed while meeting the deadlines, and compare the results of the two approaches in terms of scalability, extensibility, and flexibility.

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.

Blockchain is a shared, distributed ledger on which transactions are digitally recorded and linked together. Smart Contracts are programs running on Blockchain and are used to perform transactions in a distributed environment without need for any trusted third party. Since smart contracts are used to transfer assets between contractual parties, their safety and security are crucial and badly written and insecure contracts may result in catastrophe. Actor-based programming is known to solve several problems in building distributed software systems. Moreover, formal verification is a solid technique for developing dependable systems. In this paper, we show how the actor model can be used for modeling, analysis and synthesis of smart contracts. We propose Smart Rebeca as an extension of the actor-based language Rebeca, and use the model checking toolset Afra for verification of smart contracts. We implement a synthesizer to synthesize Solidity programs that run on the Ethereum platform from Smart Rebeca models. We examine the challenges and opportunities of our approach in modeling, formal verification, and synthesis of smart contracts using actors.

Model checking a software system is about verifying that the state trajectory of every execution of the software satisfies formally specified properties. The set of possible executions is modeled as a transition system. Each "state" in the transition system represents an assignment of values to variables, and a state trajectory (a path through the transition system) is a sequence of such assignments. For cyberphysical systems (CPSs), however, we are more interested in the state of the physical system than the values of the software variables. The value of model checking the software therefore depends on the relationship between the state of the software and the state of the physical system. This relationship can be complex because of the real-time nature of the physical plant, the sensors and actuators, and the software that is almost always concurrent and distributed. In this paper, we study different ways to construct a transition system model for the distributed and concurrent software components of a CPS. We describe a logical-time based transition system model, which is commonly used for verifying programs written in synchronous languages, and derive the conditions under which such a model faithfully reflects physical states. When these conditions are not met (a common situation), a finer-grained event-based transition system model may be required. Even this finer-grained model, however, may not be sufficiently faithful, and the transition system model needs to be refined further to express not only the properties of the software, but also the properties of the hardware on which it runs. We illustrate these tradeoffs using a coordination language called Lingua Franca that is well-suited to extracting transition system models at these various levels of granularity, and we extend the Timed Rebeca language and its tool Afra to perform this extraction and then to perform model checking.

Vehicle platooning is a promising technology to save the road capacity and also fuel consumption by reducing the distance between the vehicles in the platoon. The closer the cars are to each other, the closer we are to the goals. But, this will increase the need for safety verification. In this paper we use formal methods to verify safety distance in a platoon. To do so, we present a formal actor-based model for a vehicle platoon which incorporates vehicle dynamics and communication protocol. Also, we present a method to do the analysis based on model checking that applies mathematical analysis to reduce the state space. The method uses an upper bound and a lower bound value as network delay, and verifies if a specified vehicle in a platoon has enough distance to the leader during its traveling.

In this paper, we propose a robust solution for the path planning and scheduling of the moving objects in a Track-based Traffic Control System (TTCS). The moving objects in a TTCS pass over pre-specified sub-tracks. Each sub-track accommodates at most one moving object in-transit. Due to the uncertainties in the context of a TTCS, we assign an arrival time window to each moving object for each sub-track in its route, instead of an exact value. The moving object can safely enter into the sub-track in the mentioned time window. To develop a safe plan, we adapt the tagged-signal model and provide a rigorous mathematical formalism for the actor model of a TTCS. To illustrate the applicability of the provided semantics, we provide a formal model of TTCSs in the Alloy language and use its analyzer to verify the developed model against system safety properties.

Real-time adaptive systems are complex systems capable to adapt their behavior to changing conditions in the environment, and/or internal state changes. Highly dynamic and possibly unpredictable environments, and uncertain operating conditions call for new paradigms of software design, and run-time adaptation mechanisms, to overcome the lack of knowledge at design time. Main application areas include vehicles or robots that need to collaborate to achieve a common task, e.g., minimize fuel consumption, moving objects at a construction site, or performing a set of operations in a factory. Moreover, these vehicles or robots need to interact and possibly collaborate with humans in a safe way, e.g., avoiding accidents or collisions, and prevent hazardous situations that may harm humans and/or machines. % This paper proposes a framework for developing safe and secure adaptive collaborative systems, with run-time guarantees. To enable this, our focus is on requirement engineering and safety assurance techniques to capture the specific safety and security properties for the collaborative system, and to provide an assurance case guaranteeing that the system is sufficiently safe. Moreover, the paper proposes an architecture and behavioral models to analyze the requirements at run-time. Finally, we design a suitable deployment platform to perform the run-time analysis and planning while guaranteeing the real-time constraints.

In this paper, we present AdaptiveFlow as a platform for designing system of systems. A model-based development approach is proposed and tools are provided for formal verification and performance evaluation. The actor-based language, Timed Rebeca, is used for modelling, and the model checking tool Afra is used for checking the safety properties and also for performance evaluation. We investigate the efficiency of our approach and the applicability of the developed platform by conducting experiments on a case study based on the Electric Site Research Project of Volvo Construction Equipment. In this project, a fleet of autonomous haulers is utilised to transport materials in a quarry site. We used three adaptive policies as plugins to our platform and examined these policies in different scenarios.

Programming time-critical systems is notoriously difficult. In this paper we propose an actor-oriented programming model with a semantic notion of time and a deterministic coordination semantics based on discrete events to exercise precise control over both the computational and timing aspects of the system behavior.

I will introduce timed actors for modeling distributed systems and will explain our theories, techniques and tools for model checking and performance evaluation of such models. Timed Rebeca can be used to model asynchronous event-based components in systems, and real time constraints can be captured in the language. I will explain how floating-time transition system can be used for model checking of such models when we are interested in event-based properties, and how it helps in state space reduction. I will show different applications of our approach including analysing a wireless sensor network application, mobile ad-hoc network protocols, network-on-chip designs, and a macroscopic agent-based simulation of urban planning.

In this paper we explain how the isolation or decoupling of actors can help in developing efficient analysis techniques. The Reactive Object Language, Rebeca, and its timed extension are introduced as actor-based languages for modeling and analyzing distributed systems. We show how floating-time transition system can be used for model checking of timed actor models when we are interested in event-based properties, and how it helps in state space reduction. We explain how the model of computation of actors helps in devising an efficient state distribution policy in distributed model checking. We show how we use Rebeca to verify the routing algorithms of mobile adhoc networks. The paper is written in a way to make the ideas behind each technique clear such that it can be reused in similar domains.

There is a growing interest in using the Blockchain for resolving IoT security and trustworthiness issues existing in today's complex systems. Blockchain concerns trust in peer to peer networks by providing a distributed tamper-resistant ledger. However, the combination of these two emerging technologies might create new problems and vulnerabilities that attackers might abuse. In this paper, we aim to investigate the trust mechanism of Lightweight Scalable BlockChain (LSB), that is a Blockchain specifically designed for Internet of Things networks, to show that a malicious participant in a Blockchain architecture have possibility to pursue an On-Off attack and downgrade the integrity of the distributed ledger. We choose a remote software update process as an instance to represent this violation. Finally, using the actor-based language Rebeca, we provide a model of a system under attack and verify the described attack scenario.

We present an extension of the actor model with real-time, including deadlines associated with messages, and explicit application-level scheduling policies, e.g.,"earliest deadline first" which can be associated with individual actors. Schedulability analysis in this setting amounts to checking whether, given a scheduling policy for each actor, every task is processed within its designated deadline. To check schedulability, we introduce a compositional automata-theoretic approach, based on maximal use of model checking combined with testing. Behavioral interfaces define what an actor expects from the environment, and the deadlines for messages given these assumptions. We use model checking to verify that actors match their behavioral interfaces. We extend timed automata refinement with the notion of deadlines and use it to define compatibility of actor environments with the behavioral interfaces. Model checking of compatibility is computationally hard, so we propose a special testing process. We show that the analyses are decidable and automate the process using the Uppaal model checker.

SystemC is an IEEE standard system-level language used in hardware/software co-design and has been widely adopted in the industry. This paper describes a formal approach to verifying SystemC designs by providing a mapping to the process algebra mCRL2. Our mapping formalizes both the simulation semantics as well as exhaustive state-space exploration of SystemC designs. By exploiting the existing reduction techniques of mCRL2 and also its model-checking tools, we efficiently locate the race conditions in a system and resolve them. A tool is implemented to automatically perform the proposed mapping. This mapping and the implemented tool enabled us to exploit process-algebraic verification techniques to analyze a number of case-studies, including the formal analysis of a single-cycle and a pipelined MIPS processor specified in SystemC.

SystemC is a system-level modeling language that can be used effectively for hardware/software co-design. Since a major goal of SystemC is to enable verification at higher levels of abstraction, the tendency is now directing to introducing formal verification approaches for SystemC. In this article, we propose an approach for formal verification of SystemC designs, and provide the semantics of SystemC using Labeled Transition Systems (LTS) for this purpose. An actor-based language, Rebeca, is used as an intermediate language. SystemC designs are mapped to Rebeca models and then Rebeca verification toolset is used to verify LTL and CTL properties. To tackle the state-space explosion, Rebeca model checkers offer some reduction policies that make them appropriate for SystemC verification. The approach also benefits from the modular verification and program slicing techniques applied on Rebeca models. To show the applicability of our approach, we verified a single-cycle MIPS design and two hardware/software co-designs. The results show that our approach can effectively be used both in hardware and hardware/software co-verification.

The Unified Modeling Language, has become effectively the standard modeling language for analysis and design of software systems. However, despite achievements in defining semi-formal semantics, with a combination of OCL constraints and textual descriptions of the UML semantics, UML is still an informal language. This paper introduces a tool for developing correct models of distributed and reactive systems using UML and Rebeca. Rebeca is an actor- based modeling language supported by a formal verification tool. This approach can bridge the gap between software development and formal verification by allowing users to develop their systems using UML and yet getting advantage of formal verification support of Rebeca tools and theory. In this way, we combine two separate approaches to modeling by adding verification step to software development lifecycle. Furthermore, this can make a contribution to defining rigorous semantics for UML diagrams and to provide tool support for verification of these diagrams.

Transaction level modeling allows exploring several SoC design architectures leading to better performance and easier verification of the final product. In this paper, we present an approach for design and verification of transaction level models. Verification is integrated as part of the design-flow. In the proposed method, we first model the design in UML. Then, we translate it into the reactive objects language, Rebeca (Marjan Sirjani et al., 2004), which is an actor-based language with formal foundation. A model in Rebeca is a set of concurrently executed reactive objects (called rebecs) interacted by asynchronous message passing. After mapping UML to Rebeca, Rebeca code will be translated into Promela which is a language for formal verification. Checking the correctness of the design is performed on-the-fly with the LTL properties using the SPIN model checker. Finally, we translate the verified design to SystemC and map the properties to a set of assertions that can be re-used to validate the design at lower levels through simulation.

In this paper, we introduce a component-based approach to specify and verify system-level designs. A coordination language, Reo, is used to support hierarchical design and verification. We move from functional specification to implementation through different levels of abstraction, considering TLM/RTL mixed levels and hardware/software co-designs. We discuss the mapping of a system design written in SystemC to Reo circuits, and how we can compositionally construct its behavior using constraint automata. A case study is used to show the applicability of our approach