{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,5,4]],"date-time":"2024-05-04T12:33:11Z","timestamp":1714825991874},"reference-count":20,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2014,4,27]],"date-time":"2014-04-27T00:00:00Z","timestamp":1398556800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2014,8]]},"DOI":"10.1007\/s10009-014-0311-8","type":"journal-article","created":{"date-parts":[[2014,4,26]],"date-time":"2014-04-26T13:30:10Z","timestamp":1398519010000},"page":"421-435","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Quantitative modelling and analysis of a Chinese smart grid: a stochastic model checking case study"],"prefix":"10.1007","volume":"16","author":[{"given":"Ender","family":"Y\u00fcksel","sequence":"first","affiliation":[]},{"given":"Hanne Riis","family":"Nielson","sequence":"additional","affiliation":[]},{"given":"Flemming","family":"Nielson","sequence":"additional","affiliation":[]},{"given":"Huibiao","family":"Zhu","sequence":"additional","affiliation":[]},{"given":"Heqing","family":"Huang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,4,27]]},"reference":[{"key":"311_CR1","doi-asserted-by":"crossref","unstructured":"Lee, E.A.: Cyber physical systems: design challenges. In: Proceedings of the 2008 11th IEEE Symposium on Object Oriented Real-Time Distributed Computing, ISORC \u201908, pp. 363\u2013369. IEEE Computer Society, Washington, DC, USA (2008). doi: 10.1109\/ISORC.2008.25","DOI":"10.1109\/ISORC.2008.25"},{"key":"311_CR2","doi-asserted-by":"crossref","unstructured":"Xiao, K., Ren, S., Kwiat, K.: Retrofitting cyber physical systems for survivability through external coordination. In: Proceedings of the Proceedings of the 41st Annual Hawaii International Conference on System Sciences, HICSS \u201908, pp. 465. IEEE Computer Society, Washington, DC, USA (2008). doi: 10.1109\/HICSS.2008.377","DOI":"10.1109\/HICSS.2008.377"},{"key":"311_CR3","doi-asserted-by":"crossref","unstructured":"Morris, T.H., Srivastava, A.K., Reaves, B., Pavurapu, K., Abdelwahed, S., Vaughn, R., McGrew, W., Dandass, Y.: Engineering future cyber-physical energy systems: Challenges, research needs, and roadmap. In: North American Power Symposium (NAPS), vol. 2009, pp. 1\u20136 (2009). doi: 10.1109\/NAPS.2009.5484019","DOI":"10.1109\/NAPS.2009.5484019"},{"key":"311_CR4","doi-asserted-by":"crossref","unstructured":"Fuchs, A., Weber, D.: Analysis of the SYM2 smart meter remote software download using formal methods reasoning. In: Proceedings of the International Workshop on Security and Dependability for Resource Constrained Embedded Systems, SD4RCES \u201911, pp. 3:1\u20133:12. ACM, New York, NY, USA (2011). doi: 10.1145\/2349913.2349916","DOI":"10.1145\/2349913.2349916"},{"key":"311_CR5","doi-asserted-by":"crossref","unstructured":"Hackenberg, G., Irlbeck, M., Koutsoumpas, V., Bytschkow, D.: Applying formal software engineering techniques to smart grids. In: Proceedings of the ICSE 2012 International Workshop on Software Engineering Challenges for the Smart Grid, SE4SG\u201912. ACM, New York, NY, USA (2012)","DOI":"10.1109\/SE4SG.2012.6225719"},{"key":"311_CR6","doi-asserted-by":"crossref","unstructured":"Martins, J., Platzer, A., Leite, J.: Statistical model checking for distributed probabilistic-control hybrid automata with smart grid applications. In: Qin, S., Qiu, Z. (eds.) Formal Methods and Software Engineering. Lecture Notes in Computer Science, vol. 6991, pp. 131\u2013146. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-24559-6_11"},{"key":"311_CR7","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) Proc. 23rd International Conference on Computer Aided Verification (CAV\u201911), LNCS, vol. 6806, pp. 585\u2013591. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"311_CR8","doi-asserted-by":"crossref","unstructured":"Yuksel, E., Zhu, H., Nielson, H.R., Huang, H., Nielson, F.: Modelling and analysis of smart grid: a stochastic model checking case study. In: 2012 Sixth International Symposium on Theoretical Aspects of Software Engineering (TASE), pp. 25\u201332. IEEE (2012). doi: 10.1109\/TASE.2012.44","DOI":"10.1109\/TASE.2012.44"},{"key":"311_CR9","doi-asserted-by":"crossref","unstructured":"Y\u00fcksel, E., Nielson, H.R., Nielson, F., Zhu, H., Huang, H.: Modelling chinese smart grid: a Stochastic Model Checking Case Study. Tech. Rep. IMM-Technical Report-2012-02, DTU Informatics (2012)","DOI":"10.1109\/TASE.2012.44"},{"key":"311_CR10","doi-asserted-by":"crossref","unstructured":"Pottie, G.J., Kaiser, W.J.: Wireless integrated network sensors. Commun. ACM 43, 51\u201358 (2000). doi: 10.1145\/332833.332838","DOI":"10.1145\/332833.332838"},{"key":"311_CR11","unstructured":"Wireless medium access control and physical layer specifications for low-rate wireless personal area networks. IEEE (Std. 802.15.4-2006) (2006)"},{"key":"311_CR12","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Stochastic model checking. In: Bernardo, M., Hillston, J. (eds.) Formal Methods for the Design of Computer, Communication, and Software Systems, Lecture Notes in Computer Science, vol. 4486, pp. 220\u2013270. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-72522-0_6"},{"key":"311_CR13","doi-asserted-by":"crossref","unstructured":"Aziz, A., Sanwal, K., Singhal, V., Brayton, R.K.: Verifying continuous time markov chains. In: CAV \u201996: Proceedings of the 8th International Conference on Computer Aided Verification, pp. 269\u2013276. Springer, London (1996)","DOI":"10.1007\/3-540-61474-5_75"},{"key":"311_CR14","unstructured":"Baier, C., Haverkort, B., Hermanns, H., Katoen, J.P.: Model-checking algorithms for continuous-time markov chains. IEEE Trans. Softw. Eng. 29(6), 524\u2013541 (2003). 10.1109\/TSE.2003.1205180"},{"key":"311_CR15","doi-asserted-by":"crossref","unstructured":"Katoen, J.P., Zapreev, I.S., Hahn, E.M., Hermanns, H., Jansen, D.N.: The ins and outs of the probabilistic model checker MRMC. In: Proceedings of the 2009 Sixth International Conference on the Quantitative Evaluation of Systems, QEST \u201909, pp. 167\u2013176. IEEE Computer Society, Washington, DC, USA (2009). doi: 10.1109\/QEST.2009.11","DOI":"10.1109\/QEST.2009.11"},{"key":"311_CR16","unstructured":"Mccanne, S., Floyd, S., Fall, K.: The network simulator. http:\/\/nsnam.isi.edu\/nsnam"},{"key":"311_CR17","unstructured":"OPNET Technologies Inc: OPNET simulator. http:\/\/www.opnet.com"},{"key":"311_CR18","unstructured":"The PRISM model checker website. http:\/\/www.prismmodelchecker.org\/"},{"key":"311_CR19","unstructured":"The formal models for the modelling and analysis of the chinese smart grid. http:\/\/www2.imm.dtu.dk\/people\/ender\/csg\/"},{"key":"311_CR20","unstructured":"Y\u00fcksel, E.: Qualitative and quantitative security analyses for zigbee wireless sensor networks. Ph.D. thesis, Technical University of Denmark, Department of Informatics and Mathematical Modeling, Language-Based Technology, Kgs. Lyngby, Denmark (2011)"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-014-0311-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-014-0311-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-014-0311-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,9]],"date-time":"2019-08-09T22:40:28Z","timestamp":1565390428000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-014-0311-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,4,27]]},"references-count":20,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2014,8]]}},"alternative-id":["311"],"URL":"https:\/\/doi.org\/10.1007\/s10009-014-0311-8","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,4,27]]}}}