{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T16:21:42Z","timestamp":1761582102881,"version":"3.37.3"},"reference-count":39,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2021,6,18]],"date-time":"2021-06-18T00:00:00Z","timestamp":1623974400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,6,18]],"date-time":"2021-06-18T00:00:00Z","timestamp":1623974400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/100010663","name":"H2020 European Research Council","doi-asserted-by":"publisher","award":["780089"],"award-info":[{"award-number":["780089"]}],"id":[{"id":"10.13039\/100010663","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Software Qual J"],"published-print":{"date-parts":[[2022,6]]},"DOI":"10.1007\/s11219-021-09559-w","type":"journal-article","created":{"date-parts":[[2021,6,18]],"date-time":"2021-06-18T05:02:46Z","timestamp":1623992566000},"page":"367-388","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Learning and analysis of sensors behavior in IoT systems using statistical model checking"],"prefix":"10.1007","volume":"30","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5070-2591","authenticated-orcid":false,"given":"Salim","family":"Chehida","sequence":"first","affiliation":[]},{"given":"Abdelhakim","family":"Baouya","sequence":"additional","affiliation":[]},{"given":"Saddek","family":"Bensalem","sequence":"additional","affiliation":[]},{"given":"Marius","family":"Bozga","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,6,18]]},"reference":[{"issue":"1","key":"9559_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3158668","volume":"28","author":"G Agha","year":"2018","unstructured":"Agha, G., & Palmskog, K. (2018). A Survey of Statistical Model Checking. ACM Transactions on Modeling and Computer Simulation, 28(1), 1\u201339. https:\/\/doi.org\/10.1145\/3158668","journal-title":"ACM Transactions on Modeling and Computer Simulation"},{"key":"9559_CR2","doi-asserted-by":"publisher","first-page":"101608","DOI":"10.1016\/j.scs.2019.101608","volume":"49","author":"F Al-Turjman","year":"2019","unstructured":"Al-Turjman, F., & Malekloo, A. (2019). Smart parking in IoT-enabled cities: A survey. Sustainable Cities and Society, 49, 101608.","journal-title":"Sustainable Cities and Society"},{"issue":"1","key":"9559_CR3","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1006\/inco.1993.1025","volume":"104","author":"R Alur","year":"1993","unstructured":"Alur, R., & Henzinger, T. (1993). Real-Time Logics: Complexity and Expressiveness. Information and Computation, 104(1), 35\u201377. https:\/\/doi.org\/10.1006\/inco.1993.1025","journal-title":"Information and Computation"},{"key":"9559_CR4","doi-asserted-by":"crossref","unstructured":"Alvarez Carmona, M. A., Carrasco Ochoa, J. A., & Martinez Trinidad, J. F. (2013). Combining techniques to find the number of bins for discretization. In: 2013 32nd International Conference of the Chilean Computer Science Society (SCCC), pp 54\u201357. https:\/\/doi.org\/10.1109\/SCCC.2013.11","DOI":"10.1109\/SCCC.2013.11"},{"key":"9559_CR5","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1016\/j.peva.2015.04.003","volume":"90","author":"P Ballarini","year":"2015","unstructured":"Ballarini, P., Barbot, B., Duflot, M., Haddad, S., & Pekergin, N. (2015). Hasl: A new approach for performance evaluation and model checking from concepts to experimentation. Performance Evaluation, 90, 53\u201377.","journal-title":"Performance Evaluation"},{"key":"9559_CR6","doi-asserted-by":"crossref","unstructured":"Barbier, M., Renzaglia, A., Quilbeuf, J., Rummelhard, L., Paigwar, A., Laugier, C., Legay, A., Ibanez-Guzman, J., & Simonin, O. (2019). Validation of perception and decision-making systems for autonomous driving via statistical model checking. In: 2019 IEEE Intelligent Vehicles Symposium (IV), pp 252\u2013259.","DOI":"10.1109\/IVS.2019.8813793"},{"issue":"3","key":"9559_CR7","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1109\/MS.2011.27","volume":"28","author":"A Basu","year":"2011","unstructured":"Basu, A., Bensalem, S., Bozga, M., Combaz, J., Jaber, M., Nguyen, T. H., & Sifakis, J. (2011). Rigorous Component-Based System Design Using the BIP Framework. IEEE Software, 28(3), 41\u201348.","journal-title":"IEEE Software"},{"key":"9559_CR8","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/978-3-030-36537-0_5","volume-title":"Graphical Models for Security","author":"D Beaulaton","year":"2019","unstructured":"Beaulaton, D., Said, N. B., Cristescu, I., & Sadou, S. (2019). Security Analysis of IoT Systems Using Attack Trees. In M. Albanese, R. Horne, & C. W. Probst (Eds.), Graphical Models for Security (Vol. 11720, pp. 68\u201394). Cham: Springer International Publishing."},{"issue":"2","key":"9559_CR9","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1145\/335191.335388","volume":"29","author":"MM Breunig","year":"2000","unstructured":"Breunig, M. M., Kriegel, H. P., Ng, R. T., & Sander, J. (2000). LOF: identifying density-based local outliers. ACM SIGMOD Record, 29(2), 93\u2013104. https:\/\/doi.org\/10.1145\/335191.335388","journal-title":"ACM SIGMOD Record"},{"key":"9559_CR10","first-page":"399","volume-title":"Shepperd M, Brito e Abreu F, Rodrigues da Silva A","author":"S Chehida","year":"2020","unstructured":"Chehida, S., Baouya, A., Bensalem, S., & Bozga, M. (2020). Applied statistical model checking for a sensor behavior analysis. In R. P\u00e9rez-Castillo (Ed.), Shepperd M, Brito e Abreu F, Rodrigues da Silva A (pp. 399\u2013411). Springer International Publishing, Cham: Quality of Information and Communications Technology."},{"key":"9559_CR11","unstructured":"COSMOS. (2015). Cosmos tool. http:\/\/www.lsv.ens-cachan.fr\/Software\/cosmos\/"},{"key":"9559_CR12","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1016\/j.procs.2020.03.021","volume":"170","author":"A Daissaoui","year":"2020","unstructured":"Daissaoui, A., Boulmakoul, A., Karim, L., & Lbath, A. (2020). IoT and Big Data Analytics for Smart Buildings: A Survey. Procedia Computer Science, 170, 161\u2013168. https:\/\/doi.org\/10.1016\/j.procs.2020.03.021","journal-title":"Procedia Computer Science"},{"key":"9559_CR13","doi-asserted-by":"publisher","unstructured":"David, A., Larsen, K. G., Legay, A., Miku\u010dionis, M., & Poulsen, D. B. (2015a). Uppaal SMC tutorial. International Journal on Software Tools for Technology Transfer 17(4), 397\u2013415.\u00a0https:\/\/doi.org\/10.1007\/s10009-014-0361-y","DOI":"10.1007\/s10009-014-0361-y"},{"issue":"3","key":"9559_CR14","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/s10009-014-0323-4","volume":"17","author":"A David","year":"2015","unstructured":"David, A., Larsen, K. G., Legay, A., Mikucionis, M., Poulsen, D. B., & Sedwards, S. (2015b). Statistical model checking for biological systems. International Journal on Software Tools for Technology Transfer, 17(3), 351\u2013367. https:\/\/doi.org\/10.1007\/s10009-014-0323-4","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"9559_CR15","doi-asserted-by":"crossref","unstructured":"Dougherty, J., Kohavi, R., & Sahami, M. (1995). Supervised and unsupervised discretization of continuous features. In: Prieditis A, Russell S (eds) Machine Learning Proceedings 1995, Morgan Kaufmann, San Francisco (CA), pp 194 \u2013 202. https:\/\/doi.org\/10.1016\/B978-1-55860-377-6.50032-3","DOI":"10.1016\/B978-1-55860-377-6.50032-3"},{"key":"9559_CR16","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1016\/j.jss.2016.01.026","volume":"115","author":"JM Franco","year":"2016","unstructured":"Franco, J. M., Correia, F., Barbosa, R., Zenha-Rela, M., Schmerl, B., & Garlan, D. (2016). Improving self-adaptation planning through software architecture-based stochastic modeling. Journal of Systems and Software, 115, 42\u201360. https:\/\/doi.org\/10.1016\/j.jss.2016.01.026","journal-title":"Journal of Systems and Software"},{"key":"9559_CR17","unstructured":"Giannoni, F., Mancini, M., & Marinelli, F. (2018). Anomaly Detection Models for IoT Time Series Data. https:\/\/arxiv.org\/abs\/1812.00890"},{"issue":"9\u201310","key":"9559_CR18","doi-asserted-by":"publisher","first-page":"1641","DOI":"10.1016\/S0167-8655(03)00003-5","volume":"24","author":"Z He","year":"2003","unstructured":"He, Z., Xu, X., & Deng, S. (2003). Discovering cluster-based local outliers. Pattern Recognition Letters, 24(9\u201310), 1641\u20131650. https:\/\/doi.org\/10.1016\/S0167-8655(03)00003-5","journal-title":"Pattern Recognition Letters"},{"key":"9559_CR19","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/978-3-540-24622-0_8","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"T H\u00e9rault","year":"2004","unstructured":"H\u00e9rault, T., Lassaigne, R., Magniette, F., & Peyronnet, S. (2004). Approximate probabilistic model checking. Verification, Model Checking, and Abstract Interpretation (pp. 73\u201384). Berlin Heidelberg, Berlin, Heidelberg: Springer."},{"key":"9559_CR20","doi-asserted-by":"crossref","unstructured":"Hill, D. J, Minsker, B. S., & Amir, E. (2009). Real-time Bayesian anomaly detection in streaming environmental data: Real-time bayesia anomaly detection. Water Resources Research 45(4). https:\/\/doi.org\/10.1029\/2008WR006956","DOI":"10.1029\/2008WR006956"},{"key":"9559_CR21","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., & Parker, D. (2011). Prism 4.0: Verification of probabilistic real-time systems. In G. Gopalakrishnan & S. Qadeer (Eds.), Computer Aided Verification (pp. 585\u2013591). Heidelberg: Springer, Berlin Heidelberg, Berlin."},{"key":"9559_CR22","unstructured":"Malhotra, P., Vig, L., Shroff, G., & Agarwal, P. (2015). Long short term memory networks for anomaly detection in time series. In: European Symposium on Artificial Neural Networks, Computational Intelligence and Machine Learning. Bruges, Belgium."},{"key":"9559_CR23","doi-asserted-by":"crossref","unstructured":"Mediouni, B. L., Nouri, A., Bozga, M., Dellabani, M., Legay, A., & Bensalem, S. (2018). SBIP 2.0: Statistical Model Checking Stochastic Real-time Systems. In: ATVA 2018 - 16th International Symposium Automated Technology for Verification and Analysis, Springer, Los Angeles, CA, United States, pp 536\u2013542. https:\/\/doi.org\/10.1007\/978-3-030-01090-4_33","DOI":"10.1007\/978-3-030-01090-4_33"},{"key":"9559_CR24","doi-asserted-by":"crossref","unstructured":"Mercaldo, F., Martinelli, F., & Santone, A. (2019). Real-Time SCADA Attack Detection by Means of Formal Methods. In: 2019 IEEE 28th International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises (WETICE), IEEE, Napoli, Italy, pp 231\u2013236. https:\/\/doi.org\/10.1109\/WETICE.2019.00057","DOI":"10.1109\/WETICE.2019.00057"},{"key":"9559_CR25","unstructured":"MRMC. (2011). Mrmc tool.\u00a0http:\/\/www.mrmc-tool.org"},{"issue":"5","key":"9559_CR26","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1109\/MCC.2016.108","volume":"3","author":"A Naskos","year":"2016","unstructured":"Naskos, A., Gounaris, A., Mouratidis, H., & Katsaros, P. (2016). Online Analysis of Security Risks in Elastic Cloud Applications. IEEE Cloud Computing, 3(5), 26\u201333. https:\/\/doi.org\/10.1109\/MCC.2016.108","journal-title":"IEEE Cloud Computing"},{"issue":"2","key":"9559_CR27","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/s10009-014-0313-6","volume":"17","author":"A Nouri","year":"2015","unstructured":"Nouri, A., Bensalem, S., Bozga, M., Delahaye, B., Jegourel, C., & Legay, A. (2015). Statistical model checking QoS properties of systems with SBIP. International Journal on Software Tools for Technology Transfer, 17(2), 171\u2013185.","journal-title":"International Journal on Software Tools for Technology Transfer"},{"issue":"3\/4","key":"9559_CR28","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1504\/IJCCBS.2018.096439","volume":"8","author":"A Nouri","year":"2018","unstructured":"Nouri, A., Mediouni, B. L., Bozga, M., Combaz, J., Bensalem, S., & Legay, A. (2018). Performance evaluation of stochastic real-time systems with the SBIP framework. International Journal of Critical Computer-Based Systems, 8(3\/4), 340.","journal-title":"International Journal of Critical Computer-Based Systems"},{"issue":"8","key":"9559_CR29","doi-asserted-by":"publisher","first-page":"2355","DOI":"10.1016\/j.tele.2018.10.005","volume":"35","author":"C Park","year":"2018","unstructured":"Park, C., Kim, Y., & Jeong, M. (2018). Influencing factors on risk perception of IoT-based home energy management services. Telematics and Informatics, 35(8), 2355\u20132365.","journal-title":"Telematics and Informatics"},{"key":"9559_CR30","doi-asserted-by":"crossref","unstructured":"Pnueli, A. (1977). The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, IEEE Computer Society, USA, pp 46\u201357. https:\/\/doi.org\/10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"issue":"4","key":"9559_CR31","doi-asserted-by":"publisher","first-page":"1211","DOI":"10.1109\/TASE.2015.2471842","volume":"12","author":"J Saives","year":"2015","unstructured":"Saives, J., Pianon, C., & Faraut, G. (2015). Activity Discovery and Detection of Behavioral Deviations of an Inhabitant From Binary Sensors. IEEE Transactions on Automation Science and Engineering, 12(4), 1211\u20131224. https:\/\/doi.org\/10.1109\/TASE.2015.2471842","journal-title":"IEEE Transactions on Automation Science and Engineering"},{"issue":"4","key":"9559_CR32","doi-asserted-by":"publisher","first-page":"515","DOI":"10.1007\/s10462-013-9395-x","volume":"43","author":"N Shahid","year":"2015","unstructured":"Shahid, N., Naqvi, I. H., & Qaisar, S. B. (2015). One-class support vector machines: analysis of outlier detection for wireless sensor networks in harsh environments. Artificial Intelligence Review, 43(4), 515\u2013563. https:\/\/doi.org\/10.1007\/s10462-013-9395-x","journal-title":"Artificial Intelligence Review"},{"key":"9559_CR33","doi-asserted-by":"crossref","unstructured":"Stewart, W. J. (2009). Probability, Markov chains, queues, and simulation: the mathematical basis of performance modeling. Princeton University Press.","DOI":"10.1515\/9781400832811"},{"key":"9559_CR34","doi-asserted-by":"publisher","first-page":"547","DOI":"10.1016\/j.comcom.2019.12.006","volume":"150","author":"Z Tao","year":"2020","unstructured":"Tao, Z. (2020). Advanced Wavelet Sampling Algorithm for IoT based environmental monitoring and management. Computer Communications, 150, 547\u2013555. https:\/\/doi.org\/10.1016\/j.comcom.2019.12.006","journal-title":"Computer Communications"},{"key":"9559_CR35","first-page":"101","volume-title":"Discretization Methods","author":"Y Yang","year":"2010","unstructured":"Yang, Y., Webb, G. I., & Wu, X. (2010). Discretization Methods (pp. 101\u2013116). US, Boston, MA: Springer."},{"issue":"1","key":"9559_CR36","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1109\/TNET.2008.923716","volume":"17","author":"Yi Xie","year":"2009","unstructured":"Xie, Yi., & Shun-Zheng, Yu. (2009). A Large-Scale Hidden Semi-Markov Model for Anomaly Detection on User Browsing Behaviors. IEEE\/ACM Transactions on Networking, 17(1), 54\u201365. https:\/\/doi.org\/10.1109\/TNET.2008.923716","journal-title":"IEEE\/ACM Transactions on Networking"},{"key":"9559_CR37","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1007\/11513988_43","volume-title":"Computer Aided Verification","author":"HLS Younes","year":"2005","unstructured":"Younes, H. L. S. (2005). Ymer: A statistical model checker. Computer Aided Verification (pp. 429\u2013433). Berlin Heidelberg: Springer."},{"key":"9559_CR38","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/3-540-45657-0_17","volume-title":"Computer Aided Verification","author":"HLS Younes","year":"2002","unstructured":"Younes, H. L. S., & Simmons, R. G. (2002). Probabilistic verification of discrete event systems using acceptance sampling. In E. Brinksma & K. G. Larsen (Eds.), Computer Aided Verification (pp. 223\u2013235). Berlin Heidelberg: Springer."},{"key":"9559_CR39","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1155\/2014\/879736","volume":"2014","author":"Y Yu","year":"2014","unstructured":"Yu, Y., Zhu, Y., Li, S., & Wan, D. (2014). Time Series Outlier Detection Based on Sliding Window Prediction. Mathematical Problems in Engineering, 2014, 1\u201314. https:\/\/doi.org\/10.1155\/2014\/879736","journal-title":"Mathematical Problems in Engineering"}],"container-title":["Software Quality Journal"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11219-021-09559-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11219-021-09559-w\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11219-021-09559-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,6,27]],"date-time":"2022-06-27T08:14:46Z","timestamp":1656317686000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11219-021-09559-w"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,6,18]]},"references-count":39,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2022,6]]}},"alternative-id":["9559"],"URL":"https:\/\/doi.org\/10.1007\/s11219-021-09559-w","relation":{},"ISSN":["0963-9314","1573-1367"],"issn-type":[{"type":"print","value":"0963-9314"},{"type":"electronic","value":"1573-1367"}],"subject":[],"published":{"date-parts":[[2021,6,18]]},"assertion":[{"value":"28 April 2021","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"18 June 2021","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare that they have no conflict of interest.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflicts of interest"}},{"value":"This article does not contain any studies involving animals or human participants performed by any of the authors","order":3,"name":"Ethics","group":{"name":"EthicsHeading","label":"Ethical approval"}}]}}