Sökning: L773:1433 2779 OR L773:1433 2787 >
Modeling and analyz...
Modeling and analyzing real-time wireless sensor and actuator networks using actors and model checking
-
- Khamespanah, Ehsan (författare)
- Univ Tehran, Sch ECE, Tehran, Iran.;Reykjavik Univ, Sch Comp Sci, Reykjavik, Iceland.;Reykjavik Univ, CRESS, Reykjavik, Iceland.
-
- Sirjani, Marjan (författare)
- Mälardalens högskola,Inbyggda system,Reykjavik Univ, Sch Comp Sci, Reykjavik, Iceland
-
- Mechitov, Kirill (författare)
- Univ Illinois, OSL, Champaign, IL USA.
-
visa fler...
-
- Agha, Gul (författare)
- Univ Illinois, OSL, Champaign, IL USA.
-
visa färre...
-
Univ Tehran, Sch ECE, Tehran, Iran;Reykjavik Univ, Sch Comp Sci, Reykjavik, Iceland.;Reykjavik Univ, CRESS, Reykjavik, Iceland. Inbyggda system (creator_code:org_t)
- 2017-11-20
- 2018
- Engelska.
-
Ingår i: International Journal on Software Tools for Technology Transfer. - : SPRINGER HEIDELBERG. - 1433-2779 .- 1433-2787. ; 20:5, s. 547-561
- Relaterad länk:
-
https://urn.kb.se/re...
-
visa fler...
-
https://doi.org/10.1...
-
visa färre...
Abstract
Ämnesord
Stäng
- 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.
Ämnesord
- TEKNIK OCH TEKNOLOGIER -- Elektroteknik och elektronik -- Annan elektroteknik och elektronik (hsv//swe)
- ENGINEERING AND TECHNOLOGY -- Electrical Engineering, Electronic Engineering, Information Engineering -- Other Electrical Engineering, Electronic Engineering, Information Engineering (hsv//eng)
Nyckelord
- Sensor network
- Schedulability analysis
- Actor
- Timed Rebeca
- Model checking
Publikations- och innehållstyp
- ref (ämneskategori)
- art (ämneskategori)
Hitta via bibliotek
Till lärosätets databas