| 550 |
@InProceedings{2017:Camara:RTSS,
AUTHOR = {Seetanandi, Gautham Nayak and C\'{a}mara, Javier and Almeida, Luis and Årz\'{e}n, Karl-Erik and Maggio, Martina},
TITLE = {Event-Driven Bandwidth Allocation with Formal Guarantees for Camera Networks},
YEAR = {2017},
MONTH = {5-8 December},
BOOKTITLE = {Proceedings of the 2017 IEEE Real-Time Systems Symposium},
ADDRESS = {Paris, France},
PDF = {http://acme.able.cs.cmu.edu/pubs/uploads/pdf/RTSS17_Gautham.pdf},
ABSTRACT = {Modern computing systems are often formed by
multiple components that interact with each other through the
use of shared resources (e.g., CPU, network bandwidth, storage).
In this paper, we consider a representative scenario of one such
system in the context of an Internet of Things application. The
system consists of a network of self-adaptive cameras that share
a communication channel, transmitting streams of frames to a
central node. The cameras can modify a quality parameter to
adapt the amount of information encoded and to affect their
bandwidth requirements and usage. A critical design choice for
such a system is scheduling channel access, i.e., how to determine
the amount of channel capacity that should be used by each of the
cameras at any point in time. Two main issues have to be considered
for the choice of a bandwidth allocation scheme: (i) camera
adaptation and network access scheduling may interfere with
one another, (ii) bandwidth distribution should be triggered only
when necessary, to limit additional overhead. This paper proposes
the first formally verified event-triggered adaptation scheme for
bandwidth allocation, designed to minimize additional overhead
in the network. Desired properties of the system are verified using
model checking. The paper also describes experimental results
obtained with an implementation of the scheme.
},
KEYWORDS = {Formal Methods, Self-adaptation}
}
|
|
