Modeling and analyzing real-time wireless sensor and actuator networks using actors and model checking

Ehsan Khamespanah, Marjan Sirjani, Kirill Mechitov, Gul A Agha

Research output: Contribution to journalArticle

Abstract

Programmers often use informal worst-case analysis and debugging to ensure that schedulers 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 behaviors are specified using a Java-based actor language extended with operators for real-time scheduling and delay representation. We show how the abstraction mechanism and the compositionality of actors in 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)
Pages (from-to)547-561
Number of pages15
JournalInternational Journal on Software Tools for Technology Transfer
Volume20
Issue number5
DOIs
StatePublished - Oct 1 2018

Fingerprint

Model checking
Actuators
Sensors
Data acquisition
Scheduling

Keywords

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

ASJC Scopus subject areas

  • Software
  • Information Systems

Cite this

Modeling and analyzing real-time wireless sensor and actuator networks using actors and model checking. / Khamespanah, Ehsan; Sirjani, Marjan; Mechitov, Kirill; Agha, Gul A.

In: International Journal on Software Tools for Technology Transfer, Vol. 20, No. 5, 01.10.2018, p. 547-561.

Research output: Contribution to journalArticle

@article{897834fdd29e4c568fa5f557e43c027f,
title = "Modeling and analyzing real-time wireless sensor and actuator networks using actors and model checking",
abstract = "Programmers often use informal worst-case analysis and debugging to ensure that schedulers 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 behaviors are specified using a Java-based actor language extended with operators for real-time scheduling and delay representation. We show how the abstraction mechanism and the compositionality of actors in 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.",
keywords = "Actor, Model checking, Schedulability analysis, Sensor network, Timed Rebeca",
author = "Ehsan Khamespanah and Marjan Sirjani and Kirill Mechitov and Agha, {Gul A}",
year = "2018",
month = "10",
day = "1",
doi = "10.1007/s10009-017-0480-3",
language = "English (US)",
volume = "20",
pages = "547--561",
journal = "International Journal on Software Tools for Technology Transfer",
issn = "1433-2779",
publisher = "Springer Verlag",
number = "5",

}

TY - JOUR

T1 - Modeling and analyzing real-time wireless sensor and actuator networks using actors and model checking

AU - Khamespanah, Ehsan

AU - Sirjani, Marjan

AU - Mechitov, Kirill

AU - Agha, Gul A

PY - 2018/10/1

Y1 - 2018/10/1

N2 - Programmers often use informal worst-case analysis and debugging to ensure that schedulers 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 behaviors are specified using a Java-based actor language extended with operators for real-time scheduling and delay representation. We show how the abstraction mechanism and the compositionality of actors in 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.

AB - Programmers often use informal worst-case analysis and debugging to ensure that schedulers 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 behaviors are specified using a Java-based actor language extended with operators for real-time scheduling and delay representation. We show how the abstraction mechanism and the compositionality of actors in 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.

KW - Actor

KW - Model checking

KW - Schedulability analysis

KW - Sensor network

KW - Timed Rebeca

UR - http://www.scopus.com/inward/record.url?scp=85034566338&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85034566338&partnerID=8YFLogxK

U2 - 10.1007/s10009-017-0480-3

DO - 10.1007/s10009-017-0480-3

M3 - Article

AN - SCOPUS:85034566338

VL - 20

SP - 547

EP - 561

JO - International Journal on Software Tools for Technology Transfer

JF - International Journal on Software Tools for Technology Transfer

SN - 1433-2779

IS - 5

ER -