@inproceedings{20473c1f61be400fa54498e2366ce559,
title = "Schedulability analysis of distributed real-time sensor network applications using actor-based model checking",
abstract = "Programmers often use informal worst-case analysis and debugging to ensure schedules that satisfy real-time requirements. Not only can this process be tedious and error-prone, it is inherently conservative and thus likely to lead to an inefficient use of resources. We propose to use model checking to find a schedule which optimizes the use of resources while satisfying real-time requirements. Specifically, we represent a Wireless sensor and actuator network (WSAN) as a collection of actors whose behavior is specified using a C-based actor language extended with operators for real-time scheduling and delay representation. We show how the abstraction and compositionality properties of the actor model may be used to incrementally build a model of a WSAN{\textquoteright}s behavior from node-level and network models. We demonstrate the approach with a case study of a distributed real-time data acquisition system for high frequency sensing using Timed Rebeca modeling language and the Afra model checking tool.",
keywords = "Actor, Model checking, Schedulability analysis, Sensor network, Timed Rebeca",
author = "Ehsan Khamespanah and Kirill Mechitov and Marjan Sirjani and Gul Agha",
note = "Funding Information: The work on this paper has been supported in part by the project “Timed Asynchronous Reactive Objects in Distributed Systems: TARO” (nr. 110020021) of the Icelandic Research Fund, by Air Force ResearchLaboratory and the Air Force Office of Scientific Research under agreement number FA8750-11-2-0084, and by National Science Foundation under grant number CCF-1438982. The U.S. Government is authorized to reproduce and distribute reprints for Governmental purposes notwithstanding any copyright notation thereon. The authors acknowledge the helpful comments by the anonymous referees and by Karl Palmskog. Publisher Copyright: {\textcopyright} Springer International Publishing Switzerland 2016.; 23rd International Symposium on Model Checking Software, SPIN 2016 Co-located with 19th European Joint Conferences on Theory and Practice of Software, ETAPS 2016 ; Conference date: 07-04-2016 Through 08-04-2016",
year = "2016",
doi = "10.1007/978-3-319-32582-8_11",
language = "English (US)",
isbn = "9783319325811",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer",
pages = "165--181",
editor = "Dragan Bo{\v s}na{\v c}ki and Anton Wijs",
booktitle = "Model Checking Software - 23rd International Symposium, SPIN 2016 Co-located with ETAPS 2016, Proceedings",
address = "Germany",
}