Multimedia Tools and Applications

, Volume 74, Issue 16, pp 6151–6168 | Cite as

Advanced verification on WBAN and cloud computing for u-health environment

  • Minwoo Jung
  • Kabsu Han
  • Jeonghun ChoEmail author


The Wireless Body Area Network (WBAN) that can collect measured vital signs through sensors enables continuous monitoring of the elder and of chronic diseases. As smart devices become popular, development of the WBAN becomes easier. Our research implemented an integration platform that consists of WBAN and cloud computing based on the Transmission Control Protocol (TCP). We optimized the WBAN and the TCP as a sampling rate control. A sampling rate is the number of transfer data per second. The sampling rate is an important factor in the resolution of waveforms, though high sampling rates can cause a decline in network performance. A smart device performs three threads, such as Bluetooth, main, and TCP. The Bluetooth thread was implemented to collect vital signs from sensing nodes. The main thread performs computations for drawing waveforms and transmits data to the TCP thread. The TCP thread transmits vital signs to a server. We verified our proposed integration platform with formal verification and simulation. We expect to contribute to the platform development of WBAN and to cloud computing.


Wireless body area network Cloud computing u-Health Smart device Bluetooth 



This study was supported by the BK21 Plus project funded by the Ministry of Education, Korea (21A20131600011). This research was financially supported by the Ministry of Education (MOE) and National Research Foundation of Korea (NRF) through the Human Resource Training Project for Regional Innovation. (NO. 2011-05-대-05-024). This research was supported by the MKE (The Ministry of Knowledge Economy), Korea, under the CITRC (Convergence Information Technology Research Center) support program (NIPA-2013-H0401-13-1006) supervised by the NIPA (National IT Industry Promotion Agency). This work was supported by Ministry of Trade, Industry & Energy (MOTIE) and IDEC Platform center (IPC) for Smart car. This research was supported by the MSIP(Ministry of Science, ICT & Future Planning), Korea, under IT/SW Creative research program supervised by the NIPA(National IT Industry Promotion Agency) (NIPA-2013-ITAH0502130110690001000100100)


  1. 1.
    Baronti P, Pillai P, Chook VWC, Chessa S, Alberto Gotta Y, Fun H (2007) Wireless sensor networks: a survey on the state of the art and the 802.15.4 and ZigBee standards. Comput Commun 30(7):1655–1695CrossRefGoogle Scholar
  2. 2.
    Basu A, Bensalem S, Bozga M, Delahaye B, Legay A, Sifakis E (2010) Verification of an AFDX infrastructure using simulations and probabilities. Runtime Verification 6418:330–344CrossRefGoogle Scholar
  3. 3.
    Camara D, Loureiro AAF, Filali F (2007) Methodology for Formal Verification of Routing Protocols for Ad Hoc Wireless Networks. In: Proc. Global Telecommunication Conference, pp 705–709Google Scholar
  4. 4.
    Cavin D, Sasson Y, Schiper A (2002) On the accuracy of MANET simulators. In: Proc. the 2nd ACM International Workshop on Principles of Mobile Computing, pp 38–43Google Scholar
  5. 5.
    Corredor I, Martinez JF, Familiar MS (2011) Bringing pervasive embedded networks to the service cloud: a lightweight middleware approach. J Syst Archit 57(10):916–933zbMATHCrossRefGoogle Scholar
  6. 6.
    Demaille A, Hérault T, Peyronnet S (2006) Probabilistic verification of sensor networks. In: Proc. the 14th IEEE International Conference on Computer Sciences, Research, Innovation and Vision for the Future, pp 45–54Google Scholar
  7. 7.
    Duflot M, Kwiatkowska M, Norman G, Parker D (2006) A formal analysis of Bluetooth device discovery. Int J Softw Tools Technol Transfer 8(6):621–632CrossRefGoogle Scholar
  8. 8.
    Farella E, Pieracci A, Benini L, Rocchi L, Acquaviva A (2008) Interfacing human and computer with wireless body area sensor networks: the WiMoCA solution. Multimedia Tools Appl 38(3):337–363CrossRefGoogle Scholar
  9. 9.
    Fei H, Qiu M, Li J, Grant T, Taylor D, McCaleb S, Butler L, Hamner R (2011) A Review on cloud computing: design challenges in architecture and security. Comput Inf Technol 19(1):25–55Google Scholar
  10. 10.
    Fortino G, Parisi D, Pirrone V (2014) BodyCloud: a SaaS approach for community Body Sensor Networks. Futur Gener Comput Syst 35:62–79CrossRefGoogle Scholar
  11. 11.
    Heidemann J, Silva F, Intanagonwiwat C, Govindan R, Estrin D, Ganesan D (2001) Building efficient wireless sensor networks with low-level naming. In: Proc. the 18th ACM Symposium on Operating Systems Principles, pp 146–159Google Scholar
  12. 12.
    Jha SK, Clarke EM, Langmead CJ, Legay A, Platzer A, Zuliani P (2009) A Bayesian approach to model checking biological systems. Comput Methods Syst Biol 5688:218–234CrossRefGoogle Scholar
  13. 13.
    Jung MW, Cho J (2013) Analysis of transmission rate using Zigbee routing protocol for u-health. Ubiquit Inf Technol Appl 214(1):479–487CrossRefGoogle Scholar
  14. 14.
    Jung M, Cho J (2013) Performance Evaluation for Cloud Computing in u-Health Environment. In: Proc. IT Convergence and Security (ICITCS), pp 1–4Google Scholar
  15. 15.
    Jung M, Han K, Cho J (2013) Cloud Computing for u-Health and Automotive Environment. In: Proc. International Conference on Ubiquitous and Future Networks, pp 495–500Google Scholar
  16. 16.
    Kaur PD, Chana I (2014) Cloud based intelligent system for delivering health care as a service. Comput Methods Prog Biomed 113(1):346–359CrossRefGoogle Scholar
  17. 17.
    Kim KC (2013) An efficient processing of join queries for sensor networks using column-oriented databases. Int J Distrib Sensor Networks. doi: 10.1155/2013/345672 Google Scholar
  18. 18.
    Kim J, Chung K-Y (2011) Ontology-based healthcare context information model to implement ubiquitous environment. Multimedia Tools Appl. doi: 10.1007/s11042-011-0919-6 Google Scholar
  19. 19.
    Kotz D, Newport C, Gray RS, Liu J, Yuan Y, Elliott C (2004) Experimental evaluation of wireless. In: Proc. the 7th ACM International Symposium on Modeling, Analysis and Simulation for Wireless and Mobile Systems, pp 78–82Google Scholar
  20. 20.
    Kovachev D, Cao Y, Klamma R (2012) Building mobile multimedia services: a hybrid cloud computing approach. Multimedia Tools Appl. doi: 10.1007/s11042-012-1100-6 zbMATHGoogle Scholar
  21. 21.
    Kwiatkowska M, Norman G, Parker D (2009) PRISM: probabilistic model checking for performance and reliability analysis. ACM SIGMETRICS Perform Eval Rev 36(4):40–45CrossRefGoogle Scholar
  22. 22.
    Kwiatkowska M, Norman G, Sproston J (2002) Probabilistic model checking of the IEEE 802.11 wireless local area network protocol. In: Proc. the 2nd joint International Workshop on Process Algebra and Probabilistic Methods and Performance Modeling in Verification, pp 169–187Google Scholar
  23. 23.
    Kwiatkowska M, Norman G, Sproston J (2003) Probabilistic model checking of deadline properties in the IEEE 1394 FireWire root contention protocol. Form Asp Comput 14(3):295–318CrossRefGoogle Scholar
  24. 24.
    Kwon Y, Agha G (2006) Scalable modeling and performance evaluation of wireless sensor networks. In: Proc. the 12th IEEE Real-Time and Embedded Technology and Applications Symposium, pp 49–58Google Scholar
  25. 25.
    McIver AK (2006) Quantitative refinement and model checking for the analysis of probabilistic systems. In: Proc. the 14th International Symposium on Formal Methods, pp 131–146Google Scholar
  26. 26.
    McIver AK, Fehnker A (2006) Formal techniques for the analysis of wireless networks. In: Proc. the 2nd International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, pp 263–270Google Scholar
  27. 27.
    Pham HN, Pediaditakis D, Boulis A (2007) From simulation to real deployments in WSN and back. In: Proc. the 2007 International Symposium on a World of Wireless, Mobile and Multimedia Networks, pp 1–6Google Scholar
  28. 28.
    Rong C, Nguyen ST, Jaatun MG (2013) Beyond lighting: a survey on security challenges in cloud computing. Comput Electr Eng 39(1):47–54CrossRefGoogle Scholar
  29. 29.
    Schuts M, Zhu F, Heidarian F, Vaandrager F (2009) Modelling clock synchronization in the chess gMAC WSN protocol. In: Proc. the 1st Workshop on Quantitative Formal Methods: Theory and Applications, pp 41–54Google Scholar
  30. 30.
    Seada K, Zuniga M, Helmy A, Krishnamachari B (2004) Energy efficient forwarding strategies for geographic routing in lossy wireless sensor networks. In Proc. the 2nd International Conference on Embedded Networked Sensor Systems, pp 108–121Google Scholar
  31. 31.
    Sharma O, Lewis J, Miller A, Dearle A, Balasubramaniam D, Morrison R, Sventek J (2009) Towards verifying correctness for wireless sensor network applications using insense and spin, In: Proc. the 16th International SPIN Workshop on Model Checking Software, pp 223–240Google Scholar
  32. 32.
    Verma A (2012) Formal verification of device discovery mechanism using UPPAAL. Int J Comput Appl 58(19):32–37Google Scholar
  33. 33.
    Wu X, Wang Y, Liu G (2013) Energy-efficient routing algorithms based on OVSF code and priority in clustered wireless sensor networks. Int J Distrib Sensor Networks. doi: 10.1155/2013/620945 Google Scholar
  34. 34.
    Yin L, Dong M, Duan Y, Deng W, Zhao K, Guo J (2013) A high-performance training-free approach for hand gesture recognition with accelerometer. Multimedia Tools Appl. doi: 10.1007/s11042-013-1368-1 Google Scholar
  35. 35.
    Zuliani P, Platzer A, Clarke EM (2013) Bayesian statistical model checking with application to Simulink/Stateflow verification. Form Methods Syst Des 43(2):338–367zbMATHCrossRefGoogle Scholar
  36. 36.
    Zuniga M, Krishnamachari B (2004) Analyzing the transitional region in low power wireless links. In: Proc. the 1st IEEE Communications Society Conference on Sensor and Ad Hoc Communications and Networks, pp 517–526Google Scholar

Copyright information

© Springer Science+Business Media New York 2014

Authors and Affiliations

  1. 1.School of E/EKyungpook National UniversityDaeguSouth Korea

Personalised recommendations