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.

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.

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.

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.

Assessment of architectural evolution is a challenge and plays a significant role in system evolution management. Although the evolution rules of the software architecture are defined by some expert engineers or architects, there is no guarantee that applying them will end to the desired change. So, having a reliable assessment technique promotes the overall accuracy and quality of the evolution process. Compliance checking with expert-defined rules is a well-known assessment approach that can be applied in architectural evolution. In this paper, an approach is proposed for compliance checking of evolution processes. To this end, evolution paths and processes are modeled by Reo coordination language and compliance checking is automatically performed by model checking of the Reo circuits. To demonstrate the applicability of our approach, we show how it can be applied to a real-world architecture evolution problem.

Dynamic creating of objects and processes as one of the widely used techniques for developing models does not support by the majority of model checking tools. In addition, although there exist few model checking tools which support dynamic creation of model elements, e.g. Spin, they do not provide a property language for presenting the behavioral specifications of dynamically created elements. In this paper, we address this shortage and provide proper support for the model checking of object-based models which contain dynamic object creation. To this aim, we propose LeeTL, a new temporal logic that supports quantifications over model objects. Using LeeTL, it is also possible to traverse objects to access the variables of the objects for defining property formulas. We propose an algorithm for transforming LeeTL formulas to Büchi automata to be able to use the existing model checking tools which support Büchi automata.

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.