Internet of Things. IoT Infrastructures. Second International Summit, IoT 360° 2015, Rome, Italy, October 27-29, 2015, Revised Selected Papers, Part II

Research Article

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

Download
282 downloads
  • @INPROCEEDINGS{10.1007/978-3-319-47075-7_35,
        author={Bojan Nokovic and Emil Sekerinski},
        title={Automatically Quantitative Analysis and Code Generator for Sensor Systems: The Example of Great Lakes Water Quality Monitoring},
        proceedings={Internet of Things. IoT Infrastructures. Second International Summit, IoT 360° 2015, Rome, Italy, October 27-29, 2015, Revised Selected Papers, Part II},
        proceedings_a={IOT360},
        year={2017},
        month={6},
        keywords={Water quality monitoring Probabilistic model checking Validation Verification},
        doi={10.1007/978-3-319-47075-7_35}
    }
    
  • Bojan Nokovic
    Emil Sekerinski
    Year: 2017
    Automatically Quantitative Analysis and Code Generator for Sensor Systems: The Example of Great Lakes Water Quality Monitoring
    IOT360
    Springer
    DOI: 10.1007/978-3-319-47075-7_35
Bojan Nokovic1,*, Emil Sekerinski1,*
  • 1: McMaster University
*Contact email: nokovib@mcmaster.ca, emil@mcmaster.ca

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 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.