{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,22]],"date-time":"2025-05-22T04:20:12Z","timestamp":1747887612595,"version":"3.41.0"},"publisher-location":"Cham","reference-count":17,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319167657"},{"type":"electronic","value":"9783319167664"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-16766-4_8","type":"book-chapter","created":{"date-parts":[[2015,3,29]],"date-time":"2015-03-29T00:00:49Z","timestamp":1427587249000},"page":"73-81","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Cloud-Based Framework for Practical Model-Checking of Industrial Automation Applications"],"prefix":"10.1007","author":[{"given":"Sandeep","family":"Patil","sequence":"first","affiliation":[]},{"given":"Dmitrii","family":"Drozdov","sequence":"additional","affiliation":[]},{"given":"Victor","family":"Dubinin","sequence":"additional","affiliation":[]},{"given":"Valeriy","family":"Vyatkin","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,3,28]]},"reference":[{"key":"8_CR1","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Logic of Programs Workshop (1982)"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Clarke, E.: Characterizing correctness properties of parallel programs using fixpoints. In: de Bakker, J., van Leeuwen, J. (eds.) Automata, Languages and Programming, vol. 85, pp. 169\u2013181. Springer, Heidelberg (1980)","DOI":"10.1007\/3-540-10003-2_69"},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/978-3-540-69850-0_8","volume-title":"25 Years of Model Checking","author":"L Fix","year":"2008","unstructured":"Fix, L.: Fifteen years of formal property verification in intel. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol. 5000, pp. 139\u2013144. Springer, Heidelberg (2008)"},{"key":"8_CR4","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1145\/307988.307989","volume":"4","author":"C Kern","year":"1999","unstructured":"Kern, C., Greenstreet, M.R.: Formal verification in hardware design: a survey. ACM Trans. Des. Autom. Electron. Syst. 4, 123\u2013193 (1999)","journal-title":"ACM Trans. Des. Autom. Electron. Syst."},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"Hanisch, H.-M., Hirsch, M., Missal, D., Preu\u00dfe, S., Gerber, C.: One decade of IEC 61499 modeling and verification-results and open issues. In: 13th IFAC Symposium on Information Control Problems in Manufacturing. V.A. Trapeznikov Institute of Control Sciences, Russia (2009)","DOI":"10.3182\/20090603-3-RU-2001.0306"},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"Vyatkin, V., Hanisch, H.M.: Formal modeling and verification in the software engineering framework of IEC 61499: a way to self-verifying systems. In: Proceedings of the 8th IEEE International Conference on Emerging Technologies and Factory Automation, vol. 2, pp. 113\u2013118 (2001)","DOI":"10.1109\/ETFA.2001.997677"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A Cimatti","year":"2002","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359\u2013364. Springer, Heidelberg (2002)"},{"key":"8_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/3-540-44577-3_12","volume-title":"Informatics","author":"E Clarke","year":"2001","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Progress on the state explosion problem in model checking. In: Wilhelm, R. (ed.) Informatics: 10 Years Back, 10 Years Ahead. LNCS, vol. 2000, pp. 176\u2013194. Springer, Heidelberg (2001)"},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154\u2013169. Springer, Heidelberg (2000)"},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"Patil, S., Bhadra, S., Vyatkin, V.: Closed-loop formal verification framework with non-determinism, configurable by meta-modelling. In: IECON 2011 - 37th Annual Conference on IEEE Industrial Electronics Society, pp. 3770\u20133775 (2011)","DOI":"10.1109\/IECON.2011.6119923"},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"Patil, S., Dubinin, V., Pang, C., Vyatkin, V.: Neutralizing semantic ambiguities of function block architecture by modeling with ASM. In: 9th International Andrei Ershov Memorial Conference, PSI 2014, Peterhof, St. Petersburg, Russia (2014)","DOI":"10.1007\/978-3-662-46823-4_7"},{"key":"8_CR12","unstructured":"Hanisch, H.-M., L\u00fcder, A.: Modular modeling of closed-loop systems. In: Proc of Colloquium on Petri Net Technologies for Modeling Communication Based Systems, Berlin, Germany, pp. 103-126 (2000)"},{"key":"8_CR13","doi-asserted-by":"publisher","first-page":"1435","DOI":"10.1109\/TSMCB.2004.825915","volume":"34","author":"L Pinzon","year":"2004","unstructured":"Pinzon, L., Jafari, M.A., Hanisch, H.M., Peng, Z.: Modeling admissible behavior using event signals. IEEE Transactions on Systems, Man, and Cybernetics, Part B: Cybernetics 34, 1435\u20131448 (2004)","journal-title":"IEEE Transactions on Systems, Man, and Cybernetics, Part B: Cybernetics"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"Patil, S., Vyatkin, V., Sorouri, M.: Formal verification of Intelligent Mechatronic Systems with decentralized control logic. In: 2012 IEEE 17th Conference on Emerging Technologies & Factory Automation (ETFA), pp. 1\u20137 (2012)","DOI":"10.1109\/ETFA.2012.6489678"},{"key":"8_CR15","unstructured":"Wimmel, G.: A BDD-based Model Checker for the PEP Tool, Major Individual Project Report, Dept. (1997)"},{"key":"8_CR16","unstructured":"Cadence SMV Model Checker (March 4). http:\/\/www.kenmcmil.com\/smv.html"},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"Sorouri, M., Patil, S., Vyatkin, V.: Distributed control patterns for intelligent mechatronic systems. In: 2012 10th IEEE International Conference on Industrial Informatics (INDIN), pp. 259\u2013264 (2012)","DOI":"10.1109\/INDIN.2012.6301149"}],"container-title":["IFIP Advances in Information and Communication Technology","Technological Innovation for Cloud-Based Engineering Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-16766-4_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T18:11:32Z","timestamp":1747851092000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-16766-4_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319167657","9783319167664"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-16766-4_8","relation":{},"ISSN":["1868-4238","1868-422X"],"issn-type":[{"type":"print","value":"1868-4238"},{"type":"electronic","value":"1868-422X"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"28 March 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}