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.

Protocols are typically specified in an operational manner by specifying the communication patterns among the different involved principals. However, many properties are of epistemic nature, e.g., what each principal believes after having seen a run of the protocol. We elaborate on a unified algebraic framework suitable for epistemic reasoning about operational protocols. This reasoning framework is based on a logic of beliefs and allows for the operational specification of untruthful communications. The information recorded in the semantic models to support reasoning about the interaction between the operational and epistemic aspects intensifies the state-space explosion. We propose an efficient on-the-fly reduction for such a unifying framework by providing a set of operational rules. These operational rules automatically generate efficient reduced semantics for a class of epistemic properties, specified in a rich extension of modal μ -calculus with past and belief modality, and can potentially reduce an infinite state space into a finite one. We reformulate and prove criteria that guarantee belief consistency for credulous agents, i.e., agents that are ready to believe what is told unless it is logically inconsistent. We adjust our reduction so that the belief consistency of an original model is preserved. We prove the soundness and completeness result for the specified class of properties.

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.

Abstract We provide a semantic framework to specify information propagation in social networks; our semantic framework features both the operational description of information propagation and the epistemic aspects in social networks. In our framework, based on annotated labelled transition systems, actions are decorated with function views to specify different types of announcements. Our function views enforce various common types of local privacy policies, i.e. those policies concerning a single action. Furthermore, we specify global privacy policies, those concerning multiple actions, using a combination of modal $\mu $-calculus and epistemic logic. To illustrate the applicability of our framework, we apply it to the specification of a real-world case study. As a fundamental property for the epistemic aspect of our semantic model, we prove that its indistinguishability relations are equivalence relations, namely they are reflexive, symmetric and transitive. We also study the complexity bounds for the model-checking problem concerning a subset of our logic and show that model checking is PSPACE-complete for the studied subset.

In the new generation of message-based systems such as network-based smart systems, distributed components collaborate via asynchronous message passing. In some cases, particular ordering among the messages may lead to violation of the desired properties such as data confidentiality. Due to the absence of a global clock and usage of off-the-shelf components, there is no control over the order of messages at design time. To make such systems safe, we propose a choreography-based runtime enforcement algorithm that given an automata-based specification of unwanted message sequences, prevents certain messages to be sent, and assures that the unwanted sequences are not formed. Our algorithm is fully decentralized in the sense that each component is equipped with a monitor, as opposed to having a centralized monitor. As there is no global clock in message-based systems, the order of messages cannot be determined exactly. In this way, the monitors behave conservatively in the sense that they prevent a message from being sent, even when the sequence may not be formed. We aim to minimize conservative prevention in our algorithm when the message sequence has not been formed. The efficiency and scalability of our algorithm are evaluated in terms of the communication overhead and the blocking duration through simulation.

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.

Malfunctions of a mobile ad hoc network (MANET) protocol caused by a conceptual mistake in the protocol design, rather than unreliable communication, can often be detected only by considering communication among the nodes in the network to be reliable. In Restricted Broadcast Process Theory, which was developed for the specification and verification of MANET protocols, the communication operator is lossy. Replacing unreliable with reliable communication invalidates existing results for this process theory. We examine the effects of this adaptation on the semantics of the framework with regard to the non-blocking property of communication in MANETs, the notion of behavioral equivalence relation and its axiomatization. To utilize our complete axiomatization for analyzing the correctness of protocols at the syntactic level, we introduce a precongruence relation which abstracts away from a sequence of multi-hop communications, leading to an application-level action preconditioned by a multi-hop constraint over the topology. We illustrate the applicability of our framework through a simple routing protocol. To prove its correctness, we introduce a novel proof process, based on our precongruence relation.

Abstract Wireless ad hoc networks, in particular mobile ad hoc networks (MANETs), are growing very fast as they make communication easier and more available. However, their protocols tend to be difficult to design due to topology dependent behavior of wireless communication, and their distributed and adaptive operations to topology dynamism. Therefore, it is desirable to have them modeled and verified using formal methods. In this paper, we present an actor-based modeling language with the aim to model MANETs. We address main challenges of modeling wireless ad hoc networks such as local broadcast, underlying topology, and its changes, and discuss how they can be efficiently modeled at the semantic level to make their verification amenable. The new framework abstracts the data link layer services by providing asynchronous (local) broadcast and unicast communication, while message delivery is in order and is guaranteed for connected receivers. We illustrate the applicability of our framework through two routing protocols, namely flooding and AODVv2-11, and show how efficiently their state spaces can be reduced by the proposed techniques. Furthermore, we demonstrate a loop formation scenario in AODV, found by our analysis tool.

Public key management scheme in mobile ad hoc networks (MANETs) is an inevitable solution to achieve different security services such as integrity, confidentiality, authentication and non reputation. Probabilistic asymmetric key pre-distribution (PAKP) is a self-organized and fully distributed approach. It resolves most of MANET's challenging concerns such as storage constraint, limited physical security and dynamic topology. In such a model, secure path between two nodes is composed of one or more random successive direct secure links where intermediate nodes can read, drop or modify packets. This way, intelligent selection of intermediate nodes on a secure path is vital to ensure security and lower traffic volume. In this paper, subjective logic is used to improve PAKP method with the aim to select the most trusted and robust path. Consequently, our approach results in a better data traffic and also improve the security. Proposed algorithm chooses the least number of nodes among the most trustworthy nodes which are able to act as intermediate stations. We exploit two subjective logic based models: one exploits the subjective nature of trust between nodes and the other considers path conditions. We then evaluate our approach using network simulator ns-3. Simulation results confirm the effectiveness and superiority of the proposed protocol compared to the basic PAKP scheme.

We provide an equational theory for Restricted Broadcast Process Theory to reason about ad hoc networks. We exploit an extended algebra called Computed Network Theory to axiomatize restricted broadcast. It allows one to define the behavior of an ad hoc network with respect to the underlying topologies. We give a sound and ground-complete axiomatization for CNT terms with finite-state behavior, modulo what we call rooted branching computed network bisimilarity.

We present a process algebra for modeling and reasoning about Mobile Ad hoc Networks (MANETs) and their protocols. In our algebra we model the essential modeling concepts of ad hoc networks, i.e. local broadcast, connectivity of nodes and connectivity changes. Connectivity and connectivity changes are modeled implicitly in the semantics, which results in a more compact state space. Our connectivity model supports unidirectional links. A key feature of our algebra is eliminating connectivity information from the specification of a network, and transferring its complexity to the semantics. We give a formal operational semantics for our process algebra, and define equivalence relations on protocols and networks. We show how our algebra can be applied to prove correctness of an adhoc routing protocol.