{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T11:28:46Z","timestamp":1746012526981,"version":"3.37.3"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319747804"},{"type":"electronic","value":"9783319747811"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","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":[[2018]]},"DOI":"10.1007\/978-3-319-74781-1_20","type":"book-chapter","created":{"date-parts":[[2018,2,1]],"date-time":"2018-02-01T10:22:24Z","timestamp":1517480544000},"page":"284-299","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Injecting Formal Verification in FMI-Based Co-simulations of Cyber-Physical Systems"],"prefix":"10.1007","author":[{"given":"Lu\u00eds Diogo","family":"Couto","sequence":"first","affiliation":[]},{"given":"Stylianos","family":"Basagiannis","sequence":"additional","affiliation":[]},{"given":"El Hassan","family":"Ridouane","sequence":"additional","affiliation":[]},{"given":"Alie El-Din","family":"Mady","sequence":"additional","affiliation":[]},{"given":"Miran","family":"Hasanagic","sequence":"additional","affiliation":[]},{"given":"Peter Gorm","family":"Larsen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,2,2]]},"reference":[{"key":"20_CR1","unstructured":"Amalio, N., Cavalcanti, A., Miyazawa, A., Payne, R., Woodcock, J.: Foundations of the SysML for CPS modelling. Technical report, INTO-CPS Deliverable, D2.2a, December 2016"},{"key":"20_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/978-3-540-87698-4_29","volume-title":"Computer Safety, Reliability, and Security","author":"C Bernardeschi","year":"2008","unstructured":"Bernardeschi, C., Masci, P., Pfeifer, H.: Early prototyping of wireless sensor network algorithms in PVS. In: Harrison, M.D., Sujan, M.-A. (eds.) SAFECOMP 2008. LNCS, vol. 5219, pp. 346\u2013359. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-87698-4_29"},{"key":"20_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/978-3-642-05118-0_8","volume-title":"Stabilization, Safety, and Security of Distributed Systems","author":"C Bernardeschi","year":"2009","unstructured":"Bernardeschi, C., Masci, P., Pfeifer, H.: Analysis of wireless sensor network protocols in dynamic scenarios. In: Guerraoui, R., Petit, F. (eds.) SSS 2009. LNCS, vol. 5873, pp. 105\u2013119. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-05118-0_8"},{"key":"20_CR4","unstructured":"Blochwitz, T.: Functional Mock-up Interface for Model Exchange and Co-Simulation, July 2014. https:\/\/www.fmi-standard.org\/downloads"},{"key":"20_CR5","unstructured":"Brosse, E., Quadri, I.: SysML and FMI in INTO-CPS. Technical report, INTO-CPS Deliverable, D4.2c, December 2016"},{"key":"20_CR6","doi-asserted-by":"crossref","unstructured":"Derler, P., Lee, E.A., Sangiovanni-Vincentelli, A.L.: Addressing modeling challenges in cyber-physical systems. Technical report UCB\/EECS-2011-17, EECS Department, University of California, Berkeley, March 2011. http:\/\/www.eecs.berkeley.edu\/Pubs\/TechRpts\/2011\/EECS-2011-17.html","DOI":"10.21236\/ADA538841"},{"issue":"6","key":"20_CR7","doi-asserted-by":"crossref","first-page":"621","DOI":"10.1007\/s10009-006-0014-x","volume":"8","author":"M Duflot","year":"2006","unstructured":"Duflot, M., Kwiatkowska, M.Z., Norman, G., Parker, D.: A formal analysis of bluetooth device discovery. STTT 8(6), 621\u2013632 (2006)","journal-title":"STTT"},{"key":"20_CR8","unstructured":"Elmqvist, H., Mattsson, S.E.: An introduction to the physical modelling of language modelica. In: Proceedings of the 9th European Simulation Symposium, Technical report, October 1997"},{"key":"20_CR9","doi-asserted-by":"crossref","unstructured":"Fitzgerald, J., Gamble, C., Larsen, P.G., Pierce, K., Woodcock, J.: Cyber-physical systems design: formal foundations, methods and integrated tool chains. In: FormaliSE: FME Workshop on Formal Methods in Software Engineering, ICSE 2015, Florence, Italy, May 2015","DOI":"10.1109\/FormaliSE.2015.14"},{"key":"20_CR10","doi-asserted-by":"crossref","unstructured":"Fitzgerald, J., Gamble, C., Payne, R., Larsen, P.G., Basagiannis, S., Mady, A.E.D.: Collaborative model-based systems engineering for cyber-physical systems - a case study in building automation. In: Proceedings of INCOSE International Symposium on Systems Engineering, Edinburgh, Scotland, July 2016","DOI":"10.1002\/j.2334-5837.2016.00195.x"},{"key":"20_CR11","unstructured":"Fitzgerald, J., Gamble, C., Payne, R., Pierce, K.: Method Guidelines 2. Technical report, INTO-CPS Deliverable, D3.2a, December 2016"},{"issue":"5","key":"20_CR12","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"GJ Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"3","key":"20_CR13","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1080\/14399776.2006.10781259","volume":"7","author":"C Kleijn","year":"2006","unstructured":"Kleijn, C.: Modelling and simulation of fluid power systems with 20-sim. Int. J. Fluid Power 7(3), 57\u201360 (2006)","journal-title":"Int. J. Fluid Power"},{"key":"20_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/11560548_14","volume-title":"Correct Hardware Design and Verification Methods","author":"L Lamport","year":"2005","unstructured":"Lamport, L.: Real-time model checking is really simple. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 162\u2013175. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11560548_14"},{"issue":"1","key":"20_CR15","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1668862.1668864","volume":"35","author":"PG Larsen","year":"2010","unstructured":"Larsen, P.G., Battle, N., Ferreira, M., Fitzgerald, J., Lausdahl, K., Verhoef, M.: The overture initiative - integrating tools for VDM. SIGSOFT Softw. Eng. Notes 35(1), 1\u20136 (2010). https:\/\/doi.org\/10.1145\/1668862.1668864","journal-title":"SIGSOFT Softw. Eng. Notes"},{"key":"20_CR16","doi-asserted-by":"crossref","unstructured":"Larsen, P.G., Fitzgerald, J., Woodcock, J., Fritzson, P., Brauer, J., Kleijn, C., Lecomte, T., Pfeil, M., Green, O., Basagiannis, S., Sadovykh, A.: Integrated tool chain for model-based design of cyber-physical systems: the INTO-CPS project. In: CPS Data Workshop, Vienna, Austria, April 2016","DOI":"10.1109\/CPSData.2016.7496424"},{"key":"20_CR17","unstructured":"Larsen, P.G., Lausdahl, K., Battle, N., Fitzgerald, J., Wolff, S., Sahara, S., Verhoef, M., Tran-J\u00f8rgensen, P.W.V., Oda, T.: The VDM-10 language manual. Technical report TR-2010-06, The Overture Open Source Initiative, April 2010"},{"key":"20_CR18","unstructured":"MathWorks, October 2011. Simulink official website: http:\/\/www.mathworks.com\/"},{"issue":"2\u20133","key":"20_CR19","doi-asserted-by":"crossref","first-page":"254","DOI":"10.1016\/j.tcs.2008.09.022","volume":"410","author":"PC \u00d6lveczky","year":"2009","unstructured":"\u00d6lveczky, P.C., Thorvaldsen, S.: Formal modeling, performance estimation, and model checking of wireless sensor network algorithms in real-time maude. Theor. Comput. Sci. 410(2\u20133), 254\u2013280 (2009)","journal-title":"Theor. Comput. Sci."},{"key":"20_CR20","unstructured":"Ouy, J., Lecomte, T., Christiansen, M.P., Henriksen, A.V., Green, O., Hallerstede, S., Larsen, P.G., ger, C.J., Basagiannis, S., Couto, L.D., din Mady, A.E., Ridouanne, H., Poy, H.M., Alcala, J.V., K\u00f6nig, C., Balcu, N.: Case Studies 2, Public Version. Technical report, INTO-CPS Public Deliverable, D1.2a, December 2016"},{"key":"20_CR21","unstructured":"Philips Semiconductors Corporation: SCC2691 UART data sheet. Technical report, May 2006"},{"key":"20_CR22","unstructured":"Timothy, S.: A survey of control technologies in the building automation industry. In: Proceedings of the IFAC 16th World Congress, Prague, Czech Republic, pp. 13\u201396 (2005)"},{"key":"20_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/11813040_11","volume-title":"FM 2006: Formal Methods","author":"M Verhoef","year":"2006","unstructured":"Verhoef, M., Larsen, P.G., Hooman, J.: Modeling and validating distributed embedded real-time systems with VDM++. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 147\u2013162. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11813040_11"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-74781-1_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,10]],"date-time":"2019-10-10T00:19:43Z","timestamp":1570666783000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-74781-1_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319747804","9783319747811"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-74781-1_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}