arXiv subjects

Samarjit Chakraborty

Publications and source records attributed to Samarjit Chakraborty.

43 records · Page 3Linked to original sources

arXiv2018

TTW: A Time-Triggered-Wireless Design for CPS [ Extended version ]

Wired field buses have proved their effectiveness to support Cyber-Physical Systems (CPS). However, in avionics, for ease of deployment, or for new functionality featuring mobile devices, there is a strong interest for wireless solutions. Low-power wireless protocols have been proposed, but requirements of a large class of CPS applications can still not be satisfied. This paper presents Time-Triggered-Wireless (TTW), a distributed low-power wireless system design that minimizes energy consumption and offers end-to-end timing predictability, adaptability, reliability, low latency. Our evaluation shows a reduction of communication latency by a factor 2x and of energy consumption by 33-40% compared to state-of-the-art approaches. This validates the suitability of TTW for wireless CPS applications and opens the way for implementation and real-world experience with industry partners.

cs.NI↗

arXiv2017

Neighbor discovery latency in BLE-like duty-cycled protocols

Neighbor discovery is the procedure using which two wireless devices initiate a first contact. In low power ad-hoc networks, radios are duty-cycled and the latency until a packet meets a reception phase of another device is determined by a random process. Most research considers slotted protocols, in which the points in time for reception are temporally coupled to beacon transmissions. In contrast, many recent protocols, such as ANT/ANT+ and Bluetooth Low Energy (BLE) use a slotless, periodic-interval based scheme for neighbor discovery. Here, one device periodically broadcasts packets, whereas the other device periodically listens to the channel. Both periods are independent from each other and drawn over continuous time. Such protocols provide 3 degrees of freedom (viz., the intervals for advertising and scanning and the duration of each scan phase). Though billions of existing BLE devices rely on these protocols, neither their expected latencies nor beneficial configurations with good latency-duty-cycle relations are known. Parametrizations for the participating devices are usually determined based on a "good guess". In this paper, we for the first time present a mathematical theory which can compute the neighbor discovery latencies for all possible parametrizations. Further, our theory shows that upper bounds on the latency can be guaranteed for all parametrizations, except for a finite number of singularities. Therefore, slotless, periodic interval-based protocols can be used in applications with deterministic latency demands, which have been reserved for slotted protocols until now. Our proposed theory can be used for analyzing the neighbor discovery latencies, for tweaking protocol parameters and for developing new protocols.

cs.NI↗

arXiv2017

Development and Verification of a Flight Stack for a High-Altitude Glider in Ada/SPARK 2014

SPARK 2014 is a modern programming language and a new state-of-the-art tool set for development and verification of high-integrity software. In this paper, we explore the capabilities and limitations of its latest version in the context of building a flight stack for a high-altitude unmanned glider. Towards that, we deliberately applied static analysis early and continuously during implementation, to give verification the possibility to steer the software design. In this process we have identified several limitations and pitfalls of software design and verification in SPARK, for which we give workarounds and protective actions to avoid them. Finally, we give design recommendations that have proven effective for verification, and summarize our experiences with this new language.

cs.SE↗

arXiv2017

Approaches for Software Verification of an Emergency Recovery System for Micro Air Vehicles

This paper describes the development and verification of a competitive parachute system for Micro Air Vehicles, in particular focusing on verification of the embedded software. We first introduce the overall solution including a system level failure analysis, and then show how we minimized the influence of faulty software. This paper demonstrates that with careful abstraction and little overapproximation, the entire code running on a microprocessor can be verified using bounded model checking, and that this is a useful approach for resource-constrained embedded systems. he resulting Emergency Recovery System is to our best knowledge the first of its kind that passed formal verification, and furthermore is superior to all other existing solutions (including commercially available ones) from an operational point of view.

cs.SE↗

arXiv2017

Security in Automotive Networks: Lightweight Authentication and Authorization

With the increasing amount of interconnections between vehicles, the attack surface of internal vehicle networks is rising steeply. Although these networks are shielded against external attacks, they often do not have any internal security to protect against malicious components or adversaries who breach the network perimeter. To secure the in-vehicle network, all communicating components must be authenticated, and only authorized components should be allowed to send and receive messages. This is achieved using an authentication framework. Cryptography is widely used to authenticate communicating parties and provide secure communication channels (e.g., Internet communication). However, the real-time performance requirements of in-vehicle networks restrict the types of cryptographic algorithms and protocols that may be used. In particular, asymmetric cryptography is computationally infeasible during vehicle operation. In this work, we address the challenges of designing authentication protocols for automotive systems. We present Lightweight Authentication for Secure Automotive Networks (LASAN), a full lifecycle authentication approach. We describe the core LASAN protocols and show how they protect the internal vehicle network while complying with the real-time constraints and low computational resources of this domain. Unlike previous work, we also explain how this framework can be integrated into all aspects of the automotive lifecycle, including manufacturing, vehicle maintenance, and software updates. We evaluate LASAN in two different ways: First, we analyze the security properties of the protocols using established protocol verification techniques based on formal methods. Second, we evaluate the timing requirements of LASAN and compare these to other frameworks using a new highly modular discrete event simulator for in-vehicle networks, which we have developed for this evaluation.

cs.CR↗

arXiv2016

Slotless Protocols for Fast and Energy-Efficient Neighbor Discovery

In mobile ad-hoc networks, neighbor discovery protocols are used to find surrounding devices and to establish a first contact between them. Since the clocks of the devices are not synchronized and their energy-budgets are limited, usually duty-cycled, asynchronous discovery protocols are applied. Only if two devices are awake at the same point in time, they can rendezvous. Currently, time-slotted protocols, which subdivide time into multiple intervals with equal lengths (slots), are considered to be the most efficient discovery schemes. In this paper, we break away from the assumption of slotted time. We propose a novel, continuous-time discovery protocol, which temporally decouples beaconing and listening. Each device periodically sends packets with a certain interval, and periodically listens for a given duration with a different interval. By optimizing these interval lengths, we show that this scheme can, to the best of our knowledge, outperform all known protocols such as DISCO, U-Connect or Searchlight significantly. For example, Searchlight takes up to 740 % longer than our proposed technique to discover a device with the same duty-cycle. Further, our proposed technique can also be applied in widely-used asymmetric purely interval-based protocols such as ANT or Bluetooth Low Energy.

cs.NI↗

arXiv2014

Precise Energy Modeling for the Bluetooth Low Energy Protocol

Bluetooth Low Energy (BLE) is a wireless protocol well suited for ultra-low-power sensors running on small batteries. BLE is described as a new protocol in the official Bluetooth 4.0 specification. To design energy-efficient devices, the protocol provides a number of parameters that need to be optimized within an energy, latency and throughput design space. To minimize power consumption, the protocol parameters have to be optimized for a given application. Therefore, an energy-model that can predict the energy consumption of a BLE-based wireless device for different parameter value settings, is needed. As BLE differs from the original Bluetooth significantly, models for Bluetooth cannot be easily applied to the BLE protocol. Since the last one year, there have been a couple of proposals on energy models for BLE. However, none of them can model all the operating modes of the protocol. This paper presents a precise energy model of the BLE protocol, that allows the computation of a device's power consumption in all possible operating modes. To the best of our knowledge, our proposed model is not only one of the most accurate ones known so far (because it accounts for all protocol parameters), but it is also the only one that models all the operating modes of BLE. Furthermore, we present a sensitivity analysis of the different parameters on the energy consumption and evaluate the accuracy of the model using both discrete event simulation and actual measurements. Based on this model, guidelines for system designers are presented, that help choosing the right parameters for optimizing the energy consumption for a given application.

cs.NI↗