{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T07:12:11Z","timestamp":1743145931069,"version":"3.40.3"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319563893"},{"type":"electronic","value":"9783319563909"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-56390-9_3","type":"book-chapter","created":{"date-parts":[[2017,4,6]],"date-time":"2017-04-06T01:23:59Z","timestamp":1491441839000},"page":"44-65","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Model-Based Engineering and Spatiotemporal Analysis of Transport Systems"],"prefix":"10.1007","author":[{"given":"Simon","family":"Hordvik","sequence":"first","affiliation":[]},{"given":"Kristoffer","family":"\u00d8seth","sequence":"additional","affiliation":[]},{"given":"Henrik Heggelund","family":"Svendsen","sequence":"additional","affiliation":[]},{"given":"Jan Olaf","family":"Blech","sequence":"additional","affiliation":[]},{"given":"Peter","family":"Herrmann","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,4,7]]},"reference":[{"key":"3_CR1","unstructured":"AMQP.org: Advanced message queuing protocol (AMQP) (2016). \n                  www.amqp.org\/\n                  \n                . Accessed 01 Feb 2016"},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"Blech, J.O., Peake, I., Schmidt, H., Kande, M., Ramaswamy, S., Sudarsan, S.D., Narayanan, V.: Collaborative engineering through integration of architectural, social and spatial models. In: Proceedings of Emerging Technologies and Factory Automation (ETFA). IEEE Computer (2014)","DOI":"10.1109\/ETFA.2014.7005271"},{"key":"3_CR3","unstructured":"Blech, J.O., Schmidt, H.: Towards modeling and checking the spatial and interaction behavior of widely distributed systems. In: Improving Systems and Software Engineering Conference (2013)"},{"key":"3_CR4","unstructured":"Blech, J.O., Schmidt, H.: BeSpaceD: towards a tool framework and methodology for the specification and verification of spatial behavior of distributed software component systems. Technical report. \n                  arXiv:1404.3537\n                  \n                 (2014)"},{"key":"3_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"485","DOI":"10.1007\/978-3-642-28756-5_35","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Caires","year":"2012","unstructured":"Caires, L., Vieira, H.T.: SLMC: a tool for model checking concurrent systems against dynamical spatial logic specifications. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 485\u2013491. Springer, Heidelberg (2012). doi:\n                  10.1007\/978-3-642-28756-5_35"},{"key":"3_CR6","unstructured":"CHESS-Consortium: Chess modeling language and editor v1. 0.2 (2010)"},{"key":"3_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/3-540-49646-7_22","volume-title":"Computer Safety, Reliability and Security","author":"A Cimatti","year":"1998","unstructured":"Cimatti, A., Giunchiglia, F., Mongardi, G., Romano, D., Torielli, F., Traverso, P.: Model checking safety critical software with SPIN: an application to a railway interlocking system. In: Ehrenberger, W. (ed.) SAFECOMP 1998. LNCS, vol. 1516, pp. 284\u2013293. Springer, Heidelberg (1998). doi:\n                  10.1007\/3-540-49646-7_22"},{"key":"3_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/978-3-662-46681-0_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Cimatti","year":"2015","unstructured":"Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: HyComp: an SMT-based model checker for hybrid systems. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 52\u201367. Springer, Heidelberg (2015). doi:\n                  10.1007\/978-3-662-46681-0_4"},{"key":"3_CR9","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/BF01386390","volume":"1","author":"EW Dijkstra","year":"1959","unstructured":"Dijkstra, E.W.: A note on two problems in connexion with graphs. Numer. Math. 1, 269\u2013271 (1959)","journal-title":"Numer. Math."},{"key":"3_CR10","unstructured":"ERTMS Project: ERTMS in brief. \n                  http:\/\/www.ertms.net\/?page_id=40\n                  \n                . Accessed 14 Aug 2015"},{"key":"3_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-540-31954-2_17","volume-title":"Hybrid Systems: Computation and Control","author":"G Frehse","year":"2005","unstructured":"Frehse, G.: PHAVer: algorithmic verification of hybrid systems past HyTech. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 258\u2013273. Springer, Heidelberg (2005). doi:\n                  10.1007\/978-3-540-31954-2_17"},{"key":"3_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1007\/3-540-08755-9_9","volume-title":"Operating Systems","author":"JN Gray","year":"1978","unstructured":"Gray, J.N.: Notes on data base operating systems. In: Bayer, R., Graham, R.M., Seegm\u00fcller, G. (eds.) Operating Systems. LNCS, vol. 60, pp. 393\u2013481. Springer, Heidelberg (1978). doi:\n                  10.1007\/3-540-08755-9_9"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"Han, F., Blech, J.O., Herrmann, P., Schmidt, H.: Towards verifying safety properties of real-time probability systems. In: 11th International Workshop on Formal Engineering approaches to Software Components and Architectures (FESCA). EPTCS (2014)","DOI":"10.4204\/EPTCS.147.1"},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"Han, F., Blech, J.O., Herrmann, P., Schmidt, H.: Model-based engineering and analysis of space-aware systems communicating via IEEE 802.11. In: 39th Annual International Computers, Software & Applications Conference (COMPSAC), pp. 638\u2013646. IEEE Computer (2015)","DOI":"10.1109\/COMPSAC.2015.46"},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"Han, F., Herrmann, P., Le, H.: Modeling and verifying real-time properties of reactive systems. In: 18th International Conference on Engineering of Complex Computer Systems (ICECCS), pp. 14\u201323. IEEE Computer (2013)","DOI":"10.1109\/ICECCS.2013.13"},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"Herrmann, P., Blech, J.O.: Formal model-based development in industrial automation with reactive blocks. In: 3rd Workshop on Human-Oriented Formal Methods (2016, to appear)","DOI":"10.1007\/978-3-319-50230-4_19"},{"issue":"1","key":"3_CR17","doi-asserted-by":"publisher","first-page":"40","DOI":"10.4018\/IJWSR.2016010103","volume":"13","author":"P Herrmann","year":"2016","unstructured":"Herrmann, P., Blech, J.O., Han, F., Schmidt, H.: A model-based tool chain to verify spatial behavior of cyber-physical systems. Int. J. Web Serv. Res. (IJWSR) 13(1), 40\u201352 (2016)","journal-title":"Int. J. Web Serv. Res. (IJWSR)"},{"key":"3_CR18","doi-asserted-by":"crossref","unstructured":"Herrmann, P., Svae, A., Svendsen, H.H., Blech, J.O.: Collaborative model-based development of a remote train monitoring system. In: Proceedings of Evaluation of Novel Approaches to Software Engineering, COLAFORM Track (2016)","DOI":"10.5220\/0005929403830390"},{"key":"3_CR19","unstructured":"Hordvik, S.E., \u00d8seth, K.: Control software for an autonomous cyber-physical train system. Master\u2019s thesis, Norwegian University of Science and Technology (NTNU) (2015)"},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"Hordvik, S., \u00d8seth, K., Blech, J.O., Herrmann, P.: A methodology for model-based development and safety analysis of transport systems. In: 11th International Conference on Evaluation of Novel Approaches to Software Engineering (ENASE) (2016)","DOI":"10.5220\/0005828800910101"},{"key":"3_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"571","DOI":"10.1007\/978-3-642-04425-0_44","volume-title":"Model Driven Engineering Languages and Systems","author":"FA Kraemer","year":"2009","unstructured":"Kraemer, F.A., Herrmann, P.: Automated encapsulation of UML activities for incremental development and verification. In: Sch\u00fcrr, A., Selic, B. (eds.) MODELS 2009. LNCS, vol. 5795, pp. 571\u2013585. Springer, Heidelberg (2009). doi:\n                  10.1007\/978-3-642-04425-0_44"},{"key":"3_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-642-13464-7_3","volume-title":"Formal Techniques for Distributed Systems","author":"FA Kraemer","year":"2010","unstructured":"Kraemer, F.A., Herrmann, P.: Reactive semantics for distributed UML activities. In: Hatcliff, J., Zucca, E. (eds.) FMOODS\/FORTE -2010. LNCS, vol. 6117, pp. 17\u201331. Springer, Heidelberg (2010). doi:\n                  10.1007\/978-3-642-13464-7_3"},{"key":"3_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1613","DOI":"10.1007\/11914952_41","volume-title":"On the Move to Meaningful Internet Systems 2006: CoopIS, DOA, GADA, and ODBASE","author":"FA Kraemer","year":"2006","unstructured":"Kraemer, F.A., Herrmann, P., Br\u00e6k, R.: Aligning UML 2.0 state machines and temporal logic for the efficient execution of services. In: Meersman, R., Tari, Z. (eds.) OTM 2006. LNCS, vol. 4276, pp. 1613\u20131632. Springer, Heidelberg (2006). doi:\n                  10.1007\/11914952_41"},{"issue":"12","key":"3_CR24","doi-asserted-by":"publisher","first-page":"2068","DOI":"10.1016\/j.jss.2009.06.057","volume":"82","author":"FA Kraemer","year":"2009","unstructured":"Kraemer, F.A., Sl\u00e5tten, V., Herrmann, P.: Tool support for the rapid composition, analysis and implementation of reactive services. J. Syst. Softw. 82(12), 2068\u20132080 (2009)","journal-title":"J. Syst. Softw."},{"key":"3_CR25","doi-asserted-by":"crossref","unstructured":"Lee, E.: Cyber physical systems: design challenges. In: 11th IEEE International Symposium on Object Oriented Real-Time Distributed Computing (ISORC), pp. 363\u2013369. IEEE Computer (2008)","DOI":"10.1109\/ISORC.2008.25"},{"key":"3_CR26","unstructured":"McKenna, A., Nanty, A.: BlueBrick \u2013 Version 1.8.0. (2015). \n                  www.bluebrick.lswproject.com\/help_en.html\n                  \n                . Accessed 02 Feb 2016"},{"key":"3_CR27","unstructured":"MQTT.org: Message queuing telemetry transport (MQTT). \n                  www.mqtt.org\/\n                  \n                . Accessed 14 Aug 2015"},{"key":"3_CR28","unstructured":"Overskeid, K.M.: Personal rapid transit (PRT) system using lego mindstorms. Master\u2019s thesis, Norwegian University of Science and Technology (NTNU) (2015)"},{"key":"3_CR29","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-540-71070-7_15","volume-title":"Automated Reasoning","author":"A Platzer","year":"2008","unstructured":"Platzer, A., Quesel, J.-D.: KeYmaera: a hybrid theorem prover for hybrid systems (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 171\u2013178. Springer, Heidelberg (2008). doi:\n                  10.1007\/978-3-540-71070-7_15"},{"key":"3_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-642-10373-5_13","volume-title":"Formal Methods and Software Engineering","author":"A Platzer","year":"2009","unstructured":"Platzer, A., Quesel, J.-D.: European train control system: a case study in formal verification. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol. 5885, pp. 246\u2013265. Springer, Heidelberg (2009). doi:\n                  10.1007\/978-3-642-10373-5_13"},{"key":"3_CR31","unstructured":"Presburger, M.: \u00dcber die Vollst\u00e4ndigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In: Comptes rendues du ler Congres des Math. des Pays Slaves, Warsaw, pp. 192\u2013201 (1929). 395"},{"key":"3_CR32","doi-asserted-by":"crossref","unstructured":"Sl\u00e5tten, V., Kraemer, F., Herrmann, P.: Towards automatic generation of formal specifications to validate and verify reliable distributed system: a method exemplified by an industrial case study. In: 10th International Conference on Generative Programming and Component Engineering (GPCE 2011), pp. 147\u2013156. ACM (2011)","DOI":"10.1145\/2047862.2047888"},{"key":"3_CR33","unstructured":"Svae, A.: Remote monitoring of lego-mindstorm trains. Project thesis, Norwegian University of Science and Technology, Trondheim (2016)"},{"key":"3_CR34","unstructured":"Svendsen, H.H.: Model-based engineering of a distributed, autonomous control system for interacting trains, deployed on a lego mindstorms platform. Project thesis, Norwegian University of Science and Technology, Trondheim (2016)"},{"key":"3_CR35","unstructured":"Svendsen, H.H.: Self-localization of lego trains in a modular framework. Master\u2019s thesis, Norwegian University of Science and Technology, Trondheim (2016)"},{"key":"3_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1007\/978-3-319-21690-4_34","volume-title":"Computer Aided Verification","author":"A Tiwari","year":"2015","unstructured":"Tiwari, A.: Time-aware abstractions in HybridSal. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 504\u2013510. Springer, Cham (2015). doi:\n                  10.1007\/978-3-319-21690-4_34"},{"key":"3_CR37","unstructured":"UNIFE Project: UNIFE. \n                  http:\/\/www.unife.org\/\n                  \n                . Accessed 14 Aug 2015"},{"key":"3_CR38","volume-title":"Raspberry Pi User Guide","author":"E Upton","year":"2014","unstructured":"Upton, E., Halfacree, G.: Raspberry Pi User Guide. Wiley, Hoboken (2014)"}],"container-title":["Communications in Computer and Information Science","Evaluation of Novel Approaches to Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-56390-9_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T23:24:33Z","timestamp":1558394673000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-56390-9_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319563893","9783319563909"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-56390-9_3","relation":{},"ISSN":["1865-0929","1865-0937"],"issn-type":[{"type":"print","value":"1865-0929"},{"type":"electronic","value":"1865-0937"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"7 April 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ENASE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Evaluation of Novel Approaches to Software Engineering","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rome","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2016","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2016","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 April 2016","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"enase2016","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.enase.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}