Model Checking a Self-Adaptive Camera Network with Physical Disturbances
Nayak Seetanadi, Gautham LU ; Årzén, Karl-Erik LU
and Maggio, Martina
LU
(2019)
16th IEEE International Conference on Autonomic Computing
p.95-104
- Abstract
- The paper describes the design and verification of a self-adaptive system, composed of multiple smart cameras connected to a monitoring station, that determines the allocation of network bandwidth to the cameras. The design of such a system poses significant challenges, since multiple control strategies are active in the system simultaneously. In fact, the cameras adjust the quality of their streams to the available bandwidth, that is at the same time allocated by the monitoring station. Model checking has proven successful to verify properties of this complex system, when the effect of actions happening in the physical environment was neglected. Extending the verification models to include disturbances from the physical environment is... (More)
- The paper describes the design and verification of a self-adaptive system, composed of multiple smart cameras connected to a monitoring station, that determines the allocation of network bandwidth to the cameras. The design of such a system poses significant challenges, since multiple control strategies are active in the system simultaneously. In fact, the cameras adjust the quality of their streams to the available bandwidth, that is at the same time allocated by the monitoring station. Model checking has proven successful to verify properties of this complex system, when the effect of actions happening in the physical environment was neglected. Extending the verification models to include disturbances from the physical environment is however nontrival due to the state explosion problem. In this paper we show a comparison between the previously developed deterministic model and two alternatives for disturbance handling: a probabilistic and a nondeterministic model. We verify properties for the three models, discovering that the nondeterministic model scales better when the number of cameras increase and is more representative of the dynamic physical environment. We then focus on the nondeterministic model and study, using stochastic games, the behavior of the system when the players (cameras and network manager) collaborate or compete to reach their own objectives. (Less)
Please use this url to cite or link to this publication:
https://lup.lub.lu.se/record/065c6564-d4ba-4217-a2fd-ef72b90c5dd6
- author
- Nayak Seetanadi, Gautham
LU
; Årzén, Karl-Erik
LU
and Maggio, Martina
LU
- organization
- publishing date
- 2019-04-08
- type
- Chapter in Book/Report/Conference proceeding
- publication status
- published
- subject
- host publication
- IEEE International Conference on Autonomic Computing
- article number
- 8831206
- pages
- 95 - 104
- publisher
- IEEE - Institute of Electrical and Electronics Engineers Inc.
- conference name
- 16th IEEE International Conference on Autonomic Computing
- conference location
- Umeå, Sweden
- conference dates
- 2019-06-16 - 2019-06-20
- external identifiers
-
- scopus:85073217655
- ISBN
- 978-172812411-7
- DOI
- 10.1109/ICAC.2019.00021
- language
- English
- LU publication?
- yes
- id
- 065c6564-d4ba-4217-a2fd-ef72b90c5dd6
- date added to LUP
- 2019-04-10 15:36:48
- date last changed
- 2024-01-01 01:50:53
@inproceedings{065c6564-d4ba-4217-a2fd-ef72b90c5dd6,
abstract = {{The paper describes the design and verification of a self-adaptive system, composed of multiple smart cameras connected to a monitoring station, that determines the allocation of network bandwidth to the cameras. The design of such a system poses significant challenges, since multiple control strategies are active in the system simultaneously. In fact, the cameras adjust the quality of their streams to the available bandwidth, that is at the same time allocated by the monitoring station. Model checking has proven successful to verify properties of this complex system, when the effect of actions happening in the physical environment was neglected. Extending the verification models to include disturbances from the physical environment is however nontrival due to the state explosion problem. In this paper we show a comparison between the previously developed deterministic model and two alternatives for disturbance handling: a probabilistic and a nondeterministic model. We verify properties for the three models, discovering that the nondeterministic model scales better when the number of cameras increase and is more representative of the dynamic physical environment. We then focus on the nondeterministic model and study, using stochastic games, the behavior of the system when the players (cameras and network manager) collaborate or compete to reach their own objectives.}},
author = {{Nayak Seetanadi, Gautham and Årzén, Karl-Erik and Maggio, Martina}},
booktitle = {{IEEE International Conference on Autonomic Computing}},
isbn = {{978-172812411-7}},
language = {{eng}},
month = {{04}},
pages = {{95--104}},
publisher = {{IEEE - Institute of Electrical and Electronics Engineers Inc.}},
title = {{Model Checking a Self-Adaptive Camera Network with Physical Disturbances}},
url = {{https://lup.lub.lu.se/search/files/62893576/icac19_paper41.pdf}},
doi = {{10.1109/ICAC.2019.00021}},
year = {{2019}},
}