Schedulability analysis of distributed real-time sensor network applications using actor-based model checking

Ehsan Khamespanah, Kirill Mechitov, Marjan Sirjani, Gul Agha

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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’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.

Original languageEnglish (US)
Title of host publicationModel Checking Software - 23rd International Symposium, SPIN 2016 Co-located with ETAPS 2016, Proceedings
EditorsDragan Bošnački, Anton Wijs
PublisherSpringer-Verlag Berlin Heidelberg
Pages165-181
Number of pages17
ISBN (Print)9783319325811
DOIs
StatePublished - Jan 1 2016
Event23rd International Symposium on Model Checking Software, SPIN 2016 Co-located with 19th European Joint Conferences on Theory and Practice of Software, ETAPS 2016 - Eindhoven, Netherlands
Duration: Apr 7 2016Apr 8 2016

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9641
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other23rd International Symposium on Model Checking Software, SPIN 2016 Co-located with 19th European Joint Conferences on Theory and Practice of Software, ETAPS 2016
CountryNetherlands
CityEindhoven
Period4/7/164/8/16

Keywords

  • Actor
  • Model checking
  • Schedulability analysis
  • Sensor network
  • Timed Rebeca

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Schedulability analysis of distributed real-time sensor network applications using actor-based model checking'. Together they form a unique fingerprint.

  • Cite this

    Khamespanah, E., Mechitov, K., Sirjani, M., & Agha, G. (2016). Schedulability analysis of distributed real-time sensor network applications using actor-based model checking. In D. Bošnački, & A. Wijs (Eds.), Model Checking Software - 23rd International Symposium, SPIN 2016 Co-located with ETAPS 2016, Proceedings (pp. 165-181). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9641). Springer-Verlag Berlin Heidelberg. https://doi.org/10.1007/978-3-319-32582-8_11