Search

Hybrid Rebeca is introduced for modeling asynchronous event-based Cyber-Physical Systems (CPSs). In this work, we extend Hybrid Rebeca to allow the modeling of non-deterministic time behavior. We provide a set of rules to define the semantic model of Hybrid Rebeca models in terms of Time Transition Systems which represents an over-approximation of the reachable states of a Hybrid Rebeca model. Then, we adapt the reachability analysis algorithm of Flow$^*$ for Hybrid Rebeca models leveraging our semantic rules. This improves the analysis significantly because the previous technique relied on the reachability analysis of hybrid automata by deriving a monolithic hybrid automaton from a given Hybrid Rebeca model, leading to a huge hybrid automaton. We illustrate the applicability of our approach through a case study.

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.

In cyber-physical systems like automotive systems, there are components like sensors, actuators, and controllers that communicate asynchronously with each other. The computational model of actor supports modeling distributed asynchronously communicating systems. We propose Hybrid Rebeca language to support modeling of cyber-physical systems. Hybrid Rebeca is an extension of actor-based language Rebeca. In this extension, physical actors are introduced as new computational entities to encapsulate physical behaviors. To support various means of communication among the entities, the network is explicitly modeled as a separate entity from actors. We derive hybrid automata as the basis for analysis of Hybrid Rebeca models. We demonstrate the applicability of our approach through a case study in the domain of automotive systems. We use SpaceEx framework for the analysis of the case study.

In this paper, we present a concolic execution technique for detecting SQL injection vulnerabilities in Android apps, with a new tool we called ConsiDroid. We extend the source code of apps with mocking technique, such that the execution of original source code is not affected. The extended source code can be treated as Java applications and may be executed by SPF with concolic execution. We automatically produce a DummyMain class out of static analysis such that the essential functions are called sequentially and, the events leading to vulnerable functions are triggered. We extend SPF with taint analysis in ConsiDroid. For making taint analysis possible, we introduce a new technique of symbolic mock classes in order to ease the propagation of tainted values in the code. An SQL injection vulnerability is detected through receiving a tainted value by a vulnerable function. Besides, ConsiDroid takes advantage of static analysis to adjust SPF in order to inspect only suspicious paths. To illustrate the applicability of ConsiDroid, we have inspected randomly selected 140 apps from F-Droid repository. From these apps, we found three apps vulnerable to SQL injection. To verify their vulnerability, we analyzed the apps manually based on ConsiDroid's reports by using Robolectric.

Component-based systems evolve as a new component is added or an existing one is replaced by a newer version. Hence, it is appealing to assure the new system still preserves its safety properties. However, instead of inspecting the new system as a whole, which may result in a large state space, it is beneficial to reuse the verification results by inspecting the newly added component in isolation. To this aim, we study the problem of model checking component-based asynchronously communicating systems in the presence of an unspecified component against safety properties. Our solution is based on assume-guarantee reasoning, adopted for asynchronous environments, which generates the weakest assumption. If the newly added component conforms to the assumption, then the whole system still satisfies the property. To make the approach efficient and convergent, we produce an overapproximated interface of the missing component and by its composition with the rest of the system components, we achieve an overapproximated specification of the system, from which we remove those traces of the system that violate the property and generate an assumption for the missing component. We have implemented our approach on two case studies. Furthermore, we compared our results with the state of the art direct approach. Our resulting assumptions are smaller in size and achieved faster.

Ad hoc On Demand distance Vector (AODV) routing protocol is one of the most prominent routing protocol used in Mobile Ad-hoc Networks (MANETs). Due to the mobility of nodes, there exists many revisions as scenarios leading to the loop formation were found. We demonstrate the loop freedom property violation of AODVv2-11, AODVv2-13, and AODVv2-16 through counterexamples. We present our proposed version of AODVv2 precisely which not only ensures loop freedom but also improves the performance.

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. We illustrate the applicability of our framework through a simple routing protocol. To prove its correctness, we introduce a novel proof process, based on a precongruence relation.

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.