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.

Smart home environments receive substantial improvement from the Internet of Things (IoT) through automated systems and connected devices, which optimize living space management. The advanced technology of smart homes requires strong anomaly detection systems together with Root Cause Analysis (RCA) to maintain security and reliability. This paper presents a new immune system model for smart homes that detects unusual behavior patterns and conducts full RCA. Our methodology uses the Actor Model together with deep learning approaches that process sensor events while applying causal inference to detect anomalies and their root causes. We use multiple deep learning architectures, including sequence-to-sequence (Seq2Seq), autoencoder, and LSTM networks, to detect various anomalies, which include missing data and abnormal data values. Our autoencoder-based solution demonstrates superior performance, achieving 96.2% precision and a 98.0% F1-score. These results represent a significant improvement of 76.8% in precision and 73.7% in F1-score over state-of-the-art baseline methods. Our research demonstrates how advanced techniques improve both anomaly detection accuracy and the efficiency of RCA, which results in better smart home environment reliability and resilience.

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.

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.

Afra is an Eclipse -based tool for the modeling and model checking of Rebeca family models. Together with the standard enriched editor, easy to trace counter-example viewer, modular temporal property definition, exporting a model and its transition system to some other formats facilities are features of Afra. Rebeca family provides actor-based modeling languages which are designed to bridge the gap between formal methods and software engineering. Faithfulness to the system being modeled, and the usability of Rebeca family languages help in ease of modeling and analysis of the model, together with the synthesis of the system based on the model. In this paper, architectural decisions and design strategies we made in the development of Afra are presented. This makes Afra an extensible and reusable application for the modeling and analysis of Rebeca family models. Here, we show how different compilers can be developed for the family of languages which are the same in general language constructs but have some minor differences. Then we show how the model checking engine for these different languages is designed. Despite the fact that Afra has a layered object-oriented design and is developed in Java technology, we use C++ codes for developing its model checking for the performance purposes. This decision made the design of the application even harder.

Developing an automatic functional testing solution for high-capability software systems is challenging as these systems often have a complex architecture, resulting from satisfying a wide range of non-functional requirements. In this paper, we show how a specification-based approach can be used to generate test cases for providing a high level of confidence about the functional correctness of these systems. In this approach, the domain logic of a high-capability software system is specified in the Gallina language. The developed specification is used for both measuring coverage metrics and as the test oracle. Test cases are generated using a search-based approach, having the fitness functions defined in terms of the structural coverage of the specification. To illustrate the applicability of the approach, we applied it on an industrial stock market matching engine. The experiment indicates promising results in the effectiveness of our proposed approach, which is finding critical bugs in the system, although it has an acceptable number of manually developed test cases.

Several programming and formal modeling languages are designed based on actors. Each language has certain policies for message delivery between actors and for handling the messages in the buffers. These policies are implicit in the semantics of each language. One can infer interesting properties of actor languages related to communication and coordination based on different policies and their interactions. We define the "Transparent Actor" model where we make policies explicit as points of possible variations. We identify an abstract network entity and define the semantics of Transparent Actors in three parts: actors, network, and composition. We define a core actor language named BABEL as a basis to describe the semantics of Transparent Actors using structural operational semantics (SOS) rules with variation points. These parametric rules make the implicit policies clear and can be used as a template to define the semantics of different actor-based languages. We evaluate the applicability of the template by examining the semantics for actor-based languages Rebeca, Lingua Franca, ABS, AKKA, and Erlang. We implement BABEL in Maude as a proof of concept, then concretize the parametric rules to implement some of the above languages. We consider a few properties, check them via a set of designated litmus test cases using our Maude implementations, and discuss the policy interactions.

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.

Autonomous traffic control systems are large-scale systems with critical goals. To satisfy expected properties, these systems adapt themselves to possible changes in their environment and in the system itself. The adaptation may result in further changes propagated throughout the system. For each change and its consequent adaptation, assuring the satisfaction of properties of the system at runtime 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 an actor-based model where actors are grouped in components, and components are augmented with a coordinator. The Magnifier idea is zooming on the area (component) affected by a change and verifying the correctness of properties of interest of the system after adapting the component to the change. Magnifier checks if the change is propagating, and if that is the case, then it zooms out to perform adaptation on a larger area to contain the change. The process is iterative and incremental, and considers areas affected by the change one by one. In Magnifier, we use the Coordinated Adaptive Actor model (CoodAA) for traffic control systems. We present a formal semantics for CoodAA as a network of Timed Input-Output Automata (TIOAs), and prove the correctness of our compositional reasoning. 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 the non-compositional approach.

We propose a compositional approach for the Partial Order Reduction (POR) in the state space generation of asynchronous timed actors. We define the concept of independent actors as the actors that do not send messages to a common actor. The approach avoids exploring unnecessary interleaving of executions of independent actors. It performs on a component-based model where actors from different components, except for the actors on borders, are independent. To alleviate the effect of the cross-border messages, we enforce a delay condition, ensuring that an actor introduces a delay in its execution before sending a message across the border of its component. Within each time unit, our technique generates the state space of each individual component by taking its received messages into account. It then composes the state spaces of all components. We prove that our POR approach preserves the properties defined on timed states (states where the only outgoing transition shows the progress of time). We generate the state space of a case study in the domain of air traffic control systems based on the proposed POR. The results on our benchmarks illustrate that our POR method, on average, reduces the time and memory consumption by 76 and 34%, respectively.

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.

High-capability software services, like transaction processing systems, need to satisfy a range of non-functional characteristics such as performance, availability, and scalability. To fulfill these needs, the core business logic is usually extended with a large amount of non-domain logic in the form of frameworks, libraries, and custom code, which sometimes cannot be cleanly separated from the domain logic. So, it is nearly impossible to generate test cases for the whole system systematically guided by structural metrics on the source code. In this paper, we propose a specification-based approach to generate test cases. In this approach, the domain logic is specified in a functional notation (based on Gallina). Test cases are generated using a search-based approach where the fitness function is defined in terms of the structural coverage of the specification (measured over an equivalent Haskell implementation). An experiment on an industrial stock exchange trading engine indicates promising results in the effectiveness of our proposed approach.

Track-based flow management systems like transportation systems and traffic control systems play a crucial role in our daily life. Safety and performance are among the most important quality requirements for these systems. This paper presents AdaptiveFlow as a framework for modeling, safety checking and performance analysis of track-based flow management systems. AdaptiveFlow is based on the Hewitt actors computation model. In particular, tracks are modeled as actors and moving objects as messages. Timed Rebeca is used for modeling, and the model checking tool Afra is used for safety verification and performance evaluation in AdaptiveFlow. To react to dynamic changes in the environment, AdaptiveFlow provides support for three adaptive policies, which can be examined and compared in different scenarios. To demonstrate the applicability of AdaptiveFlow, we consider the Electric Site Research Project of Volvo Construction Equipment as a case study. In this project, a fleet of autonomous haulers is utilized to transport materials in a quarry site. Furthermore, to show the reusability of the framework for other flow management scenarios, an experiment on an urban garbage collection system is presented.

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.

The value of verification of cyberphysical systems 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 and different timelines 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. The purpose of the transition system model is to enable model checking, an established and widely used verification technique. 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. We propose an approach for formal verification of cyberphysical systems using Lingua Franca, a language designed for programming cyberphysical systems, and Rebeca, an actor-based language designed for model checking distributed event-driven systems. We focus on the cyber part and model a faithful interface to the physical part. Our method relies on the assumption that the alignment of different timelines during the execution of the system is the responsibility of the underlying platforms. We make those assumptions explicit and clear.

Vehicular ad hoc networks have attracted the attention of many researchers during the last years due to the emergence of autonomous vehicles and safety concerns. Most of the frameworks which are proposed for the modeling and analysis VANET applications make use of simulation techniques. Due to the high level of concurrency in these applications, simulation results do not guarantee the correct behavior of the system and more accurate analysis techniques are required. In this paper, we have developed a framework to provide model checking facilities for the analysis of VANET applications. To this end, an actor-based modeling language, Rebeca, is used which is equipped with a variety of model checking engines. We have extended Rebeca with the inheritance mechanism to support model-specific message passing among vehicles, which is crucial for the modeling of VANET applications. To illustrate the applicability of this framework, we modeled and analyzed two warning message dissemination schemes. Reviewing the results of using the model checking technique supports the claim that concurrent behaviors of the system components in VANETs may cause uncertainty which may not be detected by simulation-based techniques. We also observed that considering the interleaving of concurrent executions of the system components affects the performance metrics of it.