Skip to main content
SpringerLink
Log in

Automatically Quantitative Analysis and Code Generator for Sensor Systems: The Example of Great Lakes Water Quality Monitoring

  • Conference paper
  • First Online:
Internet of Things. IoT Infrastructures (IoT360 2015)

Included in the following conference series:

Abstract

In model-driven development of embedded systems, one would ideally automate both the code generation from the model and the analysis of the model for functional correctness, liveness, timing guarantees, and quantitative properties. Characteristically for embedded systems, analyzing quantitative properties like resource consumption and performance requires a model of the environment as well. We use pState to analyze the power consumption of motes intended for water quality monitoring of recreational beaches in Lake Ontario. We show how system properties can be analyzed by model checking rather than by classical approach based on a functional breakdown and spreadsheet calculation. From the same model, it is possible to generate a framework of executable code to be run on the sensor’s microcontroller. The goal of model checking approach is an improvement of engineering efficiency.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. McMaster: MacWater, June 2015. http://macwater.org/

  2. Damaso, A., Freitas, D., Rosa, N., Silva, B., Maciel, P.: Evaluating the power consumption of wireless sensor network applications using models. Sensors 13(3), 3473 (2013). http://www.mdpi.com/1424-8220/13/3/3473

    Article  Google Scholar 

  3. Negri, L., Sami, M., Tran, Q.D., Zanetti, D.: Flexible power modeling for wireless systems: power modeling and optimization of two bluetooth implementations. In: Cantarella, J. (ed.) Proceedings of 6th IEEE International Symposium on World of Wireless Mobile and Multimedia Networks, pp. 408–416. IEEE Computer Society (2005)

    Google Scholar 

  4. Negri, L., Chiarini, A.: Power simulation of communication protocols with StateC. In: Vachoux, A. (ed.) Applications of Specification and Design Languages for SoCs, pp. 277–294. Springer, Berlin (2006)

    Chapter  Google Scholar 

  5. Mura, M., Paolieri, M., Fabbri, F., Negri, L., Sami, M.G.: Power modeling, power analysis for IEEE 802.15.4: a concurrent state machine approach. In: Consumer Communications and Networking Conference, pp. 660–664 (2007)

    Google Scholar 

  6. Rusli, M., Harris, R., Punchihewa, A.: Markov chain-based analytical model of opportunistic routing protocol for wireless sensor networks. In: TENCON 2010–2010 IEEE Region 10 Conference, pp. 257–262 (2010)

    Google Scholar 

  7. Cano, C., Sfairopoulou, A., Bellalta, B., Barceló, J., Oliver, M.: Analytical model of the LPL with wake up after transmissions MAC protocol for WSNs. In: International Symposium on Wireless Communication Systems (ISWCS 2009), Siena, Italy, September 2009

    Google Scholar 

  8. Leopold, M.: Sensor network motes: portability and performance. Ph.D. dissertation, Department of Computer Science, University of Copenhagen (2007)

    Google Scholar 

  9. Nokovic, B., Sekerinski, E.: pState: a probabilistic statecharts translator. In: 2013 2nd Mediterranean Conference on Embedded Computing (MECO), pp. 29–32 (2013)

    Google Scholar 

  10. Nokovic, B., Sekerinski, E.: Verification and code generation for timed transitions in pCharts. In: Proceedings of the International C* Conference on Computer Scienceand Software Engineering, Series, C3S2E 2014. ACM, New York (2014)

    Google Scholar 

  11. Nokovic, B., Sekerinski, E.: Analysis and implementation of embedded system models: example of tags in item management application. In: W01 1st Workshop on Model-Implementation Fidelity (MiFi), Grenoble, France, p. 10 (2015)

    Google Scholar 

  12. Nokovic, B., Sekerinski, E.: A holistic approach to embedded systems development. In: 2nd Workshop on Formal-IDE, Oslo, Norway, p. 14 (2015)

    Google Scholar 

  13. Libelium: Waspmote, July 2014. http://www.libelium.com/

  14. Katoen, J.-P., Zapreev, I.S., Hahn, E.M., Hermanns, H., Jansen, D.N.: The ins and outs of the probabilistic model checker MRMC. Perform. Eval. 68(2), 90–104 (2011)

    Article  Google Scholar 

  15. Hartmanns, A.: Modest - a unified language for quantitative models. In: 2012 Forum on Specification and Design Languages (FDL), pp. 44–51, September 2012

    Google Scholar 

  16. Younes, H.L.S.: Ymer: a statistical model checker. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 429–433. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  17. Sen, K., Viswanathan, M., Agha, G.A.: VESTA: a statistical model-checker and analyzer for probabilistic systems. In: QEST, pp. 251–252 (2005)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computing and Software Department, McMaster University, Hamilton, Canada

    Bojan Nokovic & Emil Sekerinski

Authors
  1. Bojan Nokovic
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Emil Sekerinski
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Bojan Nokovic .

Editor information

Editors and Affiliations

  1. IBM Research , Haifa, Israel

    Benny Mandler

  2. CONNECT Centre, Trinity College, University of Dublin, Dublin, Ireland

    Johann Marquez-Barja

  3. GTA/PEE-COPPE/DEL-Poli, Universidade Federal do Rio de Janeiro (UFRJ), Rio de Janeiro, Rio de Janeiro, Brazil

    Miguel Elias Mitre Campista

  4. Faculty of Materials Science and Technology in Trnava, Slovak University of Technology in Bratislava, Trnava, Slovakia

    Dagmar Cagáňová

  5. Institut Télécom SudParis , Evry, France

    Hakima Chaouchi

  6. College of Communication and Information, University of Kentucky, Lexington, Kentucky, USA

    Sherali Zeadally

  7. College of Technological Innovation, Zayed University, Dubai, United Arab Emirates

    Mohamad Badra

  8. University of Pisa, Pisa, Holy See (Vatican City State)

    Stefano Giordano

  9. DICIEAMA Department, University of Messina, Messina, Italy

    Maria Fazio

  10. CREATE-NET , Trento, Italy

    Andrey Somov

  11. University of Trento , Trento, Italy

    Radu-Laurentiu Vieriu

Rights and permissions

Reprints and permissions

Copyright information

© 2016 ICST Institute for Computer Sciences, Social Informatics and Telecommunications Engineering

About this paper

Cite this paper

Nokovic, B., Sekerinski, E. (2016). Automatically Quantitative Analysis and Code Generator for Sensor Systems: The Example of Great Lakes Water Quality Monitoring. In: Mandler, B., et al. Internet of Things. IoT Infrastructures. IoT360 2015. Lecture Notes of the Institute for Computer Sciences, Social Informatics and Telecommunications Engineering, vol 170. Springer, Cham. https://doi.org/10.1007/978-3-319-47075-7_35

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-47075-7_35

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-47074-0

  • Online ISBN: 978-3-319-47075-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation