Home > Research > Publications & Outputs > Formalising Sensor Topologies for Target Counting

Research

Links

Text available via DOI:

View graph of relations

Formalising Sensor Topologies for Target Counting

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSN › Conference contribution/Paper › peer-review

Published

Standard

Formalising Sensor Topologies for Target Counting. / Linker, Sven; Sevegnani, Michele.
First Workshop on Architectures, Languages and Paradigms for IoT. 2018. p. 43-57.

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSN › Conference contribution/Paper › peer-review

Harvard

Linker, S & Sevegnani, M 2018, Formalising Sensor Topologies for Target Counting. in First Workshop on Architectures, Languages and Paradigms for IoT. pp. 43-57. https://doi.org/10.4204/EPTCS.264.5

APA

Linker, S., & Sevegnani, M. (2018). Formalising Sensor Topologies for Target Counting. In First Workshop on Architectures, Languages and Paradigms for IoT (pp. 43-57) https://doi.org/10.4204/EPTCS.264.5

Vancouver

Linker S, Sevegnani M. Formalising Sensor Topologies for Target Counting. In First Workshop on Architectures, Languages and Paradigms for IoT. 2018. p. 43-57 doi: 10.4204/EPTCS.264.5

Author

Linker, Sven ; Sevegnani, Michele. / Formalising Sensor Topologies for Target Counting. First Workshop on Architectures, Languages and Paradigms for IoT. 2018. pp. 43-57

Bibtex

@inproceedings{c4301b62f61a4c23b9aa1cebb00132ae,
title = "Formalising Sensor Topologies for Target Counting",
abstract = "We present a formal model developed to reason about topologies created by sensor ranges. This model is used to formalise the topological aspects of an existing counting algorithm to estimate the number of targets in the area covered by the sensors. To that end, we present a first-order logic tailored to specify relations between parts of the space with respect to sensor coverage. The logic serves as a specification language for Hoare-style proofs of correctness of the topological computations of the algorithm, which uncovers ambiguities in their results. Subsequently, we extend the formal model as a step towards improving the estimation of the algorithm. Finally, we sketch how the model can be extended to take mobile sensors and temporal aspects into account. ",
author = "Sven Linker and Michele Sevegnani",
year = "2018",
month = feb,
day = "6",
doi = "10.4204/EPTCS.264.5",
language = "English",
pages = "43--57",
booktitle = "First Workshop on Architectures, Languages and Paradigms for IoT",

}

RIS

TY - GEN

T1 - Formalising Sensor Topologies for Target Counting

AU - Linker, Sven

AU - Sevegnani, Michele

PY - 2018/2/6

Y1 - 2018/2/6

N2 - We present a formal model developed to reason about topologies created by sensor ranges. This model is used to formalise the topological aspects of an existing counting algorithm to estimate the number of targets in the area covered by the sensors. To that end, we present a first-order logic tailored to specify relations between parts of the space with respect to sensor coverage. The logic serves as a specification language for Hoare-style proofs of correctness of the topological computations of the algorithm, which uncovers ambiguities in their results. Subsequently, we extend the formal model as a step towards improving the estimation of the algorithm. Finally, we sketch how the model can be extended to take mobile sensors and temporal aspects into account.

AB - We present a formal model developed to reason about topologies created by sensor ranges. This model is used to formalise the topological aspects of an existing counting algorithm to estimate the number of targets in the area covered by the sensors. To that end, we present a first-order logic tailored to specify relations between parts of the space with respect to sensor coverage. The logic serves as a specification language for Hoare-style proofs of correctness of the topological computations of the algorithm, which uncovers ambiguities in their results. Subsequently, we extend the formal model as a step towards improving the estimation of the algorithm. Finally, we sketch how the model can be extended to take mobile sensors and temporal aspects into account.

U2 - 10.4204/EPTCS.264.5

DO - 10.4204/EPTCS.264.5

M3 - Conference contribution/Paper

SP - 43

EP - 57

BT - First Workshop on Architectures, Languages and Paradigms for IoT

ER -