| 1. |
- Khamespanah, Ehsan, et al.
(författare)
-
Modeling and analyzing real-time wireless sensor and actuator networks using actors and model checking
- 2018
-
Ingår i: International Journal on Software Tools for Technology Transfer. - : SPRINGER HEIDELBERG. - 1433-2779 .- 1433-2787. ; 20:5, s. 547-561
-
Tidskriftsartikel (refereegranskat)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.
|
|
| 2. |
- Khamespanah, Ehsan, et al.
(författare)
-
Schedulability Analysis of Distributed Real-Time Sensor Network Applications Using Actor-Based Model Checking
- 2016
-
Ingår i: Model Checking Software - 23rd International Symposium SPIN 2016. - Cham : Springer International Publishing. - 9783319325811 ; , s. 165-181
-
Konferensbidrag (refereegranskat)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.
|
|
| 3. |
- Sirjani, Marjan, et al.
(författare)
-
A compositional approach for modeling and timing analysis of wireless sensor and actuator networks
- 2017
-
Ingår i: ACM SIGBED Review. - : Association for Computing Machinery (ACM). - 1551-3688. ; 14:3, s. 49-56
-
Tidskriftsartikel (refereegranskat)abstract
- Wireless sensor and actuator networks (WSAN) are created through the integration of multiple nodes which acquire data and perform reaction based on them. In a general overview, sensor nodes of WSANs are responsible for data acquisition and sending them to a central node. The central node stores all the received data and performs reactions. Timing verification of WSAN applications to ensure schedulability of tasks is a challenge, and is generally performed by worst-case analysis. This process is error-prone and inherently conservative. On the other hand, using model checking for analyzing WSAN applications results in state space explosion even for middle-sized configurations. The reason is the necessity of considering the interleaving of the large number of sensors in WSANs. In this paper, we show how to build an actor-based model of WSAN applications, starting from sensor node-level and moving towards the full system, and we show how this compositional modeling improves analysability and modifiability. Realtime extension of actor model is appropriate for modeling WSAN applications where we have many concurrent and asynchronous processes, and interdependent realtime deadlines. We demonstrate the approach using a case study of a distributed realtime data acquisition system for high-frequency sensing, where Timed Rebeca is used for modeling. We use model checking to check the intra/inter-sensor node schedulability.
|
|
