Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userTool Supported Analysis of IoT
87
0
0.0
(
0
)
Added by
EPTCS
Publication date
2017
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
The design of IoT systems could benefit from the combination of two different analyses. We perform a first analysis to approximate how data flow across the system components, while the second analysis checks their communication soundness. We show how the combination of these two analyses yields further benefits hardly achievable by separately using each of them. We exploit two independently developed tools for the analyses. Firstly, we specify IoT systems in IoT-LySa, a simple specification language featuring asynchronous multicast communication of tuples. The values carried by the tuples are drawn from a term-algebra obtained by a parametric signature. The analysis of communication soundness is supported by ChorGram, a tool developed to verify the compatibility of communicating finite-state machines. In order to combine the analyses we implement an encoding of IoT-LySa processes into communicating machines. This encoding is not completely straightforward because IoT-LySa has multicast communications with data, while communication machines are based on point-to-point communications where only finitely many symbols can be exchanged. To highlight the benefits of our approach we appeal to a simple yet illustrative example.
rate research
Read More
We present Ultimate TreeAutomizer, a solver for satisfiability of sets of constrained Horn clauses. Constrained Horn clauses (CHC) are a fragment of first order logic with attractive properties in terms of expressiveness and accessibility to algorithmic solving. Ultimate TreeAutomizer is based on the techniques of trace abstraction, tree automata and tree interpolation. This paper serves as a tool description for TreeAutomizer in CHC-COMP 2019.
We present MoonLight, a tool for monitoring temporal and spatio-temporal properties of mobile and spatially distributed cyber-physical systems (CPS). In the proposed framework, space is represented as a weighted graph, describing the topological configurations in which the single CPS entities (nodes of the graph) are arranged. Both nodes and edges have attributes modelling physical and logical quantities that can change in time. MoonLight is implemented in Java and supports the monitoring of Spatio-Temporal Reach and Escape Logic (STREL). MoonLight can be used as a standalone command line tool, as a Java API, or via Matlab interface. We provide here some examples using the Matlab interface and we evaluate the tool performance also by comparing with other tools specialized in monitoring only temporal properties.
The paper aims to do a survey along with a comparative analysis of the various cryptography libraries that are applicable in the field of Internet of Things (IoT). The first half of the paper briefly introduces the various cryptography libraries available in the field of cryptography along with a list of all the algorithms contained within the libraries. The second half of the paper deals with cryptography libraries specifically aimed for application in the field of Internet of Things. The various libraries and their performance analysis listed down in this paper are consolidated from various sources with the aim of providing a single comprehensive repository for reference to the various cryptography libraries and the comparative analysis of their features in IoT.
This paper establishes a novel analytical approach to quantify robustness of scheduling and battery management for battery supported cyber-physical systems. A dynamic schedulability test is introduced to determine whether tasks are schedulable within a finite time window. The test is used to measure robustness of a real-time scheduling algorithm by evaluating the strength of computing time perturbations that break schedulability at runtime. Robustness of battery management is quantified analytically by an adaptive threshold on the state of charge. The adaptive threshold significantly reduces the false alarm rate for battery management algorithms to decide when a battery needs to be replaced.
The introduction of Narrowband Internet of Things (NB-IoT) as a cellular IoT technology aims to support massive Machine-Type Communications applications. These applications are characterized by massive connections from a large number of low-complexity and low-power devices. One of the goals of NB-IoT is to improve coverage extension beyond existing cellular technologies. In order to do that, NB-IoT introduces transmission repetitions and different bandwidth allocation configurations in uplink. These new transmission approaches yield many transmission options in uplink. In this paper, we propose analytical expressions that describe the influence of these new approaches in the transmission. Our analysis is based on the Shannon theorem. The transmission is studied in terms of the required Signal to Noise Ratio, bandwidth utilization, and energy per transmitted bit. Additionally, we propose an uplink link adaptation algorithm that contemplates these new transmission approaches. The conducted evaluation summarizes the influence of these approaches. Furthermore, we present the resulting uplink link adaptation from our proposed algorithm sweeping the devices coverage.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
