文章詳目資料

Journal of Computers EIMEDLINEScopus

  • 加入收藏
  • 下載文章
篇名 Performability Evaluation Low-Powered Sensor Node by Stochastic Model Checking
卷期 28:2
作者 Niu, JunJin, Guang
頁次 177-187
關鍵字 markov processesperformance evaluationstochastic model checkingwireless sen-sor networkEIMEDLINEScopus
出刊日期 201704
DOI 10.3966/199115592017042802013

中文摘要

英文摘要

Wireless Sensor Network (WSN) applications, there may be many low-powered sensor nodes which can communicate with each other by wireless techniques. Due to limited power supply, the satisfiability of performability properties, which include energy constraints especially, must be confirmed in design phase. This will help one to avoid implementing impracticable designs. A typical performability property may be as follows: the probability that the energy consumption of a sensor node is smaller than 5 if it operates correctly in 1 hour is bigger than 0.90. Stochastic model checking is a successful and well established technique for formally verifying performability properties of systems which exhibit stochastic behavior. This paper introduces continuous time Markov Chain (CTMC) enhanced with reward structures to model the dynamic behavior of a sensor node. The performability specification which includes energy constraints can be depicted by continuous stochastic reward logic (CSRL). Our main contribution is a verification approach of sensor nodes’ performability properties, which include energy constraints especially, based on stochastic model checking technique. Moreover, we show the applicability of the approach and provide some experimental results by stochastic model checker MRMC.

本卷期文章目次

相關文獻