mdh.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Modeling and analyzing real-time wireless sensor and actuator networks using actors and model checking
Univ Tehran, Sch ECE, Tehran, Iran.;Reykjavik Univ, Sch Comp Sci, Reykjavik, Iceland.;Reykjavik Univ, CRESS, Reykjavik, Iceland..
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems. Reykjavik Univ, Sch Comp Sci, Reykjavik, Iceland.
Univ Illinois, OSL, Champaign, IL USA..
Univ Illinois, OSL, Champaign, IL USA..
2018 (English)In: International Journal on Software Tools for Technology Transfer (STTT), ISSN 1433-2779, E-ISSN 1433-2787, Vol. 20, no 5, p. 547-561Article in journal (Refereed) Published
Abstract [en]

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.

Place, publisher, year, edition, pages
SPRINGER HEIDELBERG , 2018. Vol. 20, no 5, p. 547-561
Keywords [en]
Sensor network, Schedulability analysis, Actor, Timed Rebeca, Model checking
National Category
Other Electrical Engineering, Electronic Engineering, Information Engineering
Identifiers
URN: urn:nbn:se:mdh:diva-40736DOI: 10.1007/s10009-017-0480-3ISI: 000441949300005Scopus ID: 2-s2.0-85034566338OAI: oai:DiVA.org:mdh-40736DiVA, id: diva2:1246061
Conference
23rd International SPIN Symposium on Model Checking of Software (SPIN), APR 07-08, 2016, Eindhoven, NETHERLANDS
Available from: 2018-09-06 Created: 2018-09-06 Last updated: 2018-11-28Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records BETA

Sirjani, Marjan

Search in DiVA

By author/editor
Sirjani, Marjan
By organisation
Embedded Systems
In the same journal
International Journal on Software Tools for Technology Transfer (STTT)
Other Electrical Engineering, Electronic Engineering, Information Engineering

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 9 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf