Automatic Quantitative Analysis and Code Generator for Sensor Systems: The Example of Great Lakes Water Quality Monitoring. Nokovic, B. & Sekerinski, E. In Mandler, B., Marquez-Barja, J., Mitre Campista, M. E., Cagáňová, D., Chaouchi, H., Zeadally, S., Badra, M., Giordano, S., Fazio, M., Somov, A., & Vieriu, R., editors, Internet of Things. IoT Infrastructures: Second International Summit, IoT 360º 2015, volume 170, of Lecture Notes of the Institute for Computer Sciences, Social Informatics and Telecommunications Engineering, pages 313–319, 2016. Springer. URL: http://s-cubeconference.org/2015/show/program-final![Automatic Quantitative Analysis and Code Generator for Sensor Systems: The Example of Great Lakes Water Quality Monitoring [link]](https://bibbase.org/img/filetypes/link.svg "link")
Paper doi abstract bibtex 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 qual- ity 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.
@inproceedings{NokovicSekerinski16GreatLakes,
series = {Lecture {Notes} of the {Institute} for {Computer} {Sciences}, {Social} {Informatics} and {Telecommunications} {Engineering}},
title = {Automatic {Quantitative} {Analysis} and {Code} {Generator} for {Sensor} {Systems}: {The} {Example} of {Great} {Lakes} {Water} {Quality} {Monitoring}},
volume = {170},
isbn = {978-3-319-47075-7},
url = {http://dx.doi.org/10.1007/978-3-319-47075-7_35},
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 pState to analyze the power consumption of motes intended for water qual- ity 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.},
booktitle = {Internet of {Things}. {IoT} {Infrastructures}: {Second} {International} {Summit}, {IoT} 360º 2015},
publisher = {Springer},
author = {Nokovic, Bojan and Sekerinski, Emil},
editor = {Mandler, Benny and Marquez-Barja, Johann and Mitre Campista, Miguel Elias and Cagáňová, Dagmar and Chaouchi, Hakima and Zeadally, Sherali and Badra, Mohamad and Giordano, Stefano and Fazio, Maria and Somov, Andrey and Vieriu, Radu-Laurentiu},
year = {2016},
note = {URL: http://s-cubeconference.org/2015/show/program-final},
pages = {313--319},
}
Downloads: 0
{"_id":"wLcmkxBWLx85KG8Fv","bibbaseid":"nokovic-sekerinski-automaticquantitativeanalysisandcodegeneratorforsensorsystemstheexampleofgreatlakeswaterqualitymonitoring-2016","authorIDs":["5d5141906acb07da0100009c","5deb78019e04d1df010000e0","5df0c9af96fa76de0100004a","5df1e05078da84de01000007","5e0152666afa18de01000079","5e14924f08c265de01000191","5e159bdce8bfcff201000064","5e1c7d5192587bde010001a6","5e1e0b00f6dca7f201000020","5e2827e2e6485dde01000035","5e288b4067e11edf01000130","5e2f394178a7cedf010000dc","5e34df5862bc74de010000f4","5e3c065bea028bde0100018f","5e4f908242a908de010000e9","5e585f852c2732de010001b4","5e5948def5822adf01000075","5e5d99be5726ecdf010000d1","5e600cdf13e3aede010001f5","5e69048f8457bade010002a1","5e6acf2ad15181f301000141","92uEQKMDcvvBMsZhM","Ge6aoqtpksMCtyrhL","YfeH5nK5eMWgp3gGy","anKewCA9AWgtndQzB","cwnpJhAGnLcWDSWqt","dochF8eFSd3jy8jcD","e6xvbhubvq5PtsszN","mixtvxbFoDFYKhAQq","oAZuP8sa3gmYvdqKk","qz4iM7vyMs82Hvx8j","wsgyLi66Pkv72928T","xset8hhxmqR8QvHh5"],"author_short":["Nokovic, B.","Sekerinski, E."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","series":"Lecture Notes of the Institute for Computer Sciences, Social Informatics and Telecommunications Engineering","title":"Automatic Quantitative Analysis and Code Generator for Sensor Systems: The Example of Great Lakes Water Quality Monitoring","volume":"170","isbn":"978-3-319-47075-7","url":"http://dx.doi.org/10.1007/978-3-319-47075-7_35","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 pState to analyze the power consumption of motes intended for water qual- ity 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.","booktitle":"Internet of Things. IoT Infrastructures: Second International Summit, IoT 360º 2015","publisher":"Springer","author":[{"propositions":[],"lastnames":["Nokovic"],"firstnames":["Bojan"],"suffixes":[]},{"propositions":[],"lastnames":["Sekerinski"],"firstnames":["Emil"],"suffixes":[]}],"editor":[{"propositions":[],"lastnames":["Mandler"],"firstnames":["Benny"],"suffixes":[]},{"propositions":[],"lastnames":["Marquez-Barja"],"firstnames":["Johann"],"suffixes":[]},{"propositions":[],"lastnames":["Mitre","Campista"],"firstnames":["Miguel","Elias"],"suffixes":[]},{"propositions":[],"lastnames":["Cagáňová"],"firstnames":["Dagmar"],"suffixes":[]},{"propositions":[],"lastnames":["Chaouchi"],"firstnames":["Hakima"],"suffixes":[]},{"propositions":[],"lastnames":["Zeadally"],"firstnames":["Sherali"],"suffixes":[]},{"propositions":[],"lastnames":["Badra"],"firstnames":["Mohamad"],"suffixes":[]},{"propositions":[],"lastnames":["Giordano"],"firstnames":["Stefano"],"suffixes":[]},{"propositions":[],"lastnames":["Fazio"],"firstnames":["Maria"],"suffixes":[]},{"propositions":[],"lastnames":["Somov"],"firstnames":["Andrey"],"suffixes":[]},{"propositions":[],"lastnames":["Vieriu"],"firstnames":["Radu-Laurentiu"],"suffixes":[]}],"year":"2016","note":"URL: http://s-cubeconference.org/2015/show/program-final","pages":"313–319","bibtex":"@inproceedings{NokovicSekerinski16GreatLakes,\n\tseries = {Lecture {Notes} of the {Institute} for {Computer} {Sciences}, {Social} {Informatics} and {Telecommunications} {Engineering}},\n\ttitle = {Automatic {Quantitative} {Analysis} and {Code} {Generator} for {Sensor} {Systems}: {The} {Example} of {Great} {Lakes} {Water} {Quality} {Monitoring}},\n\tvolume = {170},\n\tisbn = {978-3-319-47075-7},\n\turl = {http://dx.doi.org/10.1007/978-3-319-47075-7_35},\n\tdoi = {10.1007/978-3-319-47075-7_35},\n\tabstract = {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 qual- ity 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.},\n\tbooktitle = {Internet of {Things}. {IoT} {Infrastructures}: {Second} {International} {Summit}, {IoT} 360º 2015},\n\tpublisher = {Springer},\n\tauthor = {Nokovic, Bojan and Sekerinski, Emil},\n\teditor = {Mandler, Benny and Marquez-Barja, Johann and Mitre Campista, Miguel Elias and Cagáňová, Dagmar and Chaouchi, Hakima and Zeadally, Sherali and Badra, Mohamad and Giordano, Stefano and Fazio, Maria and Somov, Andrey and Vieriu, Radu-Laurentiu},\n\tyear = {2016},\n\tnote = {URL: http://s-cubeconference.org/2015/show/program-final},\n\tpages = {313--319},\n}\n\n","author_short":["Nokovic, B.","Sekerinski, E."],"editor_short":["Mandler, B.","Marquez-Barja, J.","Mitre Campista, M. E.","Cagáňová, D.","Chaouchi, H.","Zeadally, S.","Badra, M.","Giordano, S.","Fazio, M.","Somov, A.","Vieriu, R."],"key":"NokovicSekerinski16GreatLakes","id":"NokovicSekerinski16GreatLakes","bibbaseid":"nokovic-sekerinski-automaticquantitativeanalysisandcodegeneratorforsensorsystemstheexampleofgreatlakeswaterqualitymonitoring-2016","role":"author","urls":{"Paper":"http://dx.doi.org/10.1007/978-3-319-47075-7_35"},"metadata":{"authorlinks":{"sekerinski, e":"https://bibbase.org/show?bib=https%3A%2F%2Fapi.krunk.cn%2Femil%2Fbib.php"}},"downloads":0},"bibtype":"inproceedings","biburl":"https://api.krunk.cn/emil/bib.php","creationDate":"2019-08-15T00:44:32.450Z","downloads":0,"keywords":[],"search_terms":["automatic","quantitative","analysis","code","generator","sensor","systems","example","great","lakes","water","quality","monitoring","nokovic","sekerinski"],"title":"Automatic Quantitative Analysis and Code Generator for Sensor Systems: The Example of Great Lakes Water Quality Monitoring","year":2016,"dataSources":["HEdahWqKBpmSGmDwq","MF5eGzpJnqf6bSAoG","ienufKdnmJs49AsjR","So4gmSWFmbQRNEuFs","ezsmw4w22u9JFLNYJ","CvQYP6Tmpapx74Mgr","RWydLHbBJqgdeh5jr"]}