TY - GEN
T1 - Event-Driven Bandwidth Allocation with Formal Guarantees for Camera Networks
AU - Seetanadi, Gautham Nayak
AU - Camara Moreno, Javier
AU - Almeida, Luis
AU - Arzen, Karl Erik
AU - Maggio, Martina
PY - 2018/1/31
Y1 - 2018/1/31
N2 - 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.
AB - 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.
KW - Bandwidth-distribution
KW - Model-checking
KW - Real-Time-Systems
UR - http://www.scopus.com/inward/record.url?scp=85046350517&partnerID=8YFLogxK
U2 - 10.1109/RTSS.2017.00030
DO - 10.1109/RTSS.2017.00030
M3 - Conference contribution
AN - SCOPUS:85046350517
VL - 2018-January
T3 - IEEE Real-Time Systems Symposium (RTSS)
SP - 243
EP - 254
BT - Proceedings - 2017 IEEE Real-Time Systems Symposium, RTSS 2017
PB - IEEE
T2 - 38th IEEE Real-Time Systems Symposium, RTSS 2017
Y2 - 5 October 2017 through 8 October 2017
ER -
