Research Article
Automatically Quantitative Analysis and Code Generator for Sensor Systems: The Example of Great Lakes Water Quality Monitoring
@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
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.