{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T22:10:33Z","timestamp":1648678233028},"reference-count":52,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2014,3,18]],"date-time":"2014-03-18T00:00:00Z","timestamp":1395100800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Supercomput"],"published-print":{"date-parts":[[2014,9]]},"DOI":"10.1007\/s11227-014-1157-2","type":"journal-article","created":{"date-parts":[[2014,3,18]],"date-time":"2014-03-18T01:34:48Z","timestamp":1395106488000},"page":"1254-1283","source":"Crossref","is-referenced-by-count":3,"title":["On design and formal verification of SNSP: a novel real-time communication protocol for safety-critical applications"],"prefix":"10.1007","volume":"69","author":[{"given":"Rui","family":"Zhou","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Chanjuan","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rong","family":"Min","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Qi","family":"Yu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fei","family":"Gu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Qingguo","family":"Zhou","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jason C.","family":"Hung","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kuan-Ching","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xuan","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2014,3,18]]},"reference":[{"key":"1157_CR1","doi-asserted-by":"crossref","first-page":"86","DOI":"10.1007\/BFb0024530","volume":"563","author":"H Kopetz","year":"1991","unstructured":"Kopetz H (1991) Event-triggered versus time-triggered real-time systems, operating systems of the 90s and beyond. Lecture Notes Comput Sci 563:86\u2013101","journal-title":"Lecture Notes Comput Sci"},{"key":"1157_CR2","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4419-8237-7","volume-title":"Real-time systems: design principles for distributed embedded applications","author":"H Kopetz","year":"2011","unstructured":"Kopetz H (2011) Real-time systems: design principles for distributed embedded applications, 2nd edn. Springer, Germany","edition":"2"},{"key":"1157_CR3","doi-asserted-by":"crossref","unstructured":"Trawczynski D, Sosnowski J, Zalewski J (2007) The effect of large clock drifts on performance of event and time triggered network interfaces. In: 2nd international conference on dependability of computer systems (DepCoS-RELCOMEX \u201907), Szklarska, pp 344\u2013351","DOI":"10.1109\/DEPCOS-RELCOMEX.2007.48"},{"key":"1157_CR4","doi-asserted-by":"crossref","unstructured":"Kopetz H (1992) Sparse time versus dense time in distributed real-time systems. In: Proceedings of 12th international conference on distributed computing systems, Yokohama, pp 460\u2013467","DOI":"10.1109\/ICDCS.1992.235008"},{"issue":"13","key":"1157_CR5","first-page":"1","volume":"3","author":"A Sinha","year":"2013","unstructured":"Sinha A, Lobiyal DK (2013) Performance evaluation of data aggregation for cluster-based wireless sensor network. Human Centric Comput Inf Sci 3(13):1\u201317","journal-title":"Human Centric Comput Inf Sci"},{"key":"1157_CR6","unstructured":"Li CJ, McGuire N, Zhou QG (2009) A new real-time network protocol-node order protocol. In: Proceedings of 11th real time Linux workshop, Dresden"},{"key":"1157_CR7","unstructured":"Correll K, Barendt N, Branicky M (2005) Design consideration for software only implementations of the ieee 1588 precision time protocol. In: Conference on IEEE 1588 standard for a precision clock synchronization protocol for networked measurement and control systems, Winterthur, pp 1\u20136"},{"key":"1157_CR8","unstructured":"Hartwich F, M\u00fcller B, F\u00fchrer T, Hugel R (2002) Timing in the TTCAN network. In: Proceedings of the 8th international CAN conference (iCC\u201902), Las Vegas, pp 1\u20138"},{"issue":"2","key":"1157_CR9","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1016\/S0141-9331(01)00148-X","volume":"26","author":"G Leen","year":"2002","unstructured":"Leen G, Heffernan D (2002) TTCAN: a new time-triggered controller area network. Microprocessors Microsyst 26(2):77\u201394","journal-title":"Microprocessors Microsyst"},{"key":"1157_CR10","doi-asserted-by":"crossref","unstructured":"Kopetz H, Grunsteidl G (1993) TTP\u2014a time-triggered protocol for fault-tolerant real-time systems,. In: The twenty-third international symposium on fault-tolerant computing (FTCS-23), Toulouse, pp 524\u2013533","DOI":"10.1109\/FTCS.1993.627355"},{"key":"1157_CR11","doi-asserted-by":"crossref","unstructured":"Zaidi S, Boutekkouk F (2013) Design and simulation of the timed triggered protocol (TTP) using agents. In: Proceeding of 2013 AASRI conference on intelligent systems and control, vol 4, Vancouver. Published in AASRI Procedia, pp 110\u2013117","DOI":"10.1016\/j.aasri.2013.10.018"},{"key":"1157_CR12","unstructured":"Karlsson A (2002) X-by-wire systems and time-triggered protocols, Master Thesis. Uppsala University, Sweden"},{"key":"1157_CR13","unstructured":"Koptez H (2001) A comparison of TTP\/C and FlexRay, Research Report, Technische Universit\u00e4t Wien, Austria. http:\/\/citeseerx.ist.psu.edu\/viewdoc\/download?doi=10.1.1.87.2330&rep=rep1&type=pdf . Accessed 19 Feb 2014"},{"key":"1157_CR14","unstructured":"ROBERT BOSCH GmbH (1991) CAN Specification Version 2.0. http:\/\/esd.cs.ucr.edu\/webres\/can20.pdf . Accessed 19 Feb 2014"},{"issue":"6","key":"1157_CR15","doi-asserted-by":"crossref","first-page":"1241","DOI":"10.1109\/41.808018","volume":"46","author":"E Tovar","year":"1999","unstructured":"Tovar E, Vasques F (1999) Real-time fieldbus communications using profibus networks. IEEE Trans Ind Electron 46(6):1241\u20131251","journal-title":"IEEE Trans Ind Electron"},{"key":"1157_CR16","unstructured":"Berwanger J, Peller M, Griessbach R (2000) Byteflight\u2014a new protocol for safety critical applications. In: Seoul 2000 FISITA world automotive congress, Seoul, pp 1\u20137"},{"key":"1157_CR17","doi-asserted-by":"crossref","unstructured":"Cena G, Valenzano A (2004) Performance analysis of byteflight networks. In: Proceedings of 2004 IEEE international workshop on factory communication systems, Vienna, pp 157\u2013166","DOI":"10.1109\/WFCS.2004.1377701"},{"key":"1157_CR18","unstructured":"Ethernet POWERLINK Standardization Group (2008) Ethernet POWERLINK communication profile specification EPSG DS 301 V1.1.0. http:\/\/www.ethernet-powerlink.org"},{"issue":"8","key":"1157_CR19","doi-asserted-by":"crossref","first-page":"1163","DOI":"10.1016\/0967-0661(95)00112-8","volume":"3","author":"K Tindell","year":"1995","unstructured":"Tindell K, Burns A, Wellings A (1995) Calculating controller area network (can) message response times. Control Eng Pract 3(8):1163\u20131169","journal-title":"Control Eng Pract"},{"issue":"3","key":"1157_CR20","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1007\/s11241-007-9012-7","volume":"35","author":"RI Davis","year":"2007","unstructured":"Davis RI, Burns A, Bril RJ, Lukkien JJ (2007) Controller area network (CAN) schedulability analysis: refuted, revisited and revised. Real Time Syst 35(3):239\u2013272","journal-title":"Real Time Syst"},{"issue":"3","key":"1157_CR21","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1023\/B:TIME.0000029051.60313.06","volume":"27","author":"S Zhang","year":"2004","unstructured":"Zhang S, Burns A, Chen J, Lee E (2004) Hard real-time communication with the timed token protocol: current state and challenging problems. Real Time Syst 27(3):271\u2013295","journal-title":"Real Time Syst"},{"issue":"1\u20133","key":"1157_CR22","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1007\/s11241-007-9040-3","volume":"39","author":"T Pop","year":"2008","unstructured":"Pop T, Pop P, Eles P, Peng Z, Andrei A (2008) Timing analysis of the FlexRay communication protocol. Real Time Syst 39(1\u20133):205\u2013235","journal-title":"Real Time Syst"},{"key":"1157_CR23","doi-asserted-by":"crossref","unstructured":"Wang Z, Song YQ, Chen JM, Sun YX (2002) Real time characteristics of ethernet and its improvement. In: Proceedings of the 4th world congress on intelligent control and automation, vol 2, Shanghai, pp 1311\u20131318","DOI":"10.1109\/WCICA.2002.1020794"},{"key":"1157_CR24","unstructured":"Alves M, Tovar E, Vasques F (2000) Ethernet goes real-time: a survey on research and technological developments, Technical Report. Polytechnic Institute of Porto. http:\/\/www.cister.isep.ipp.pt\/docs\/ethernet+goes+real%252Dtime%253A+a+survey+on+research+and+technological+developments\/68\/view.pdf . Accessed 19 Feb 2014"},{"issue":"6","key":"1157_CR25","doi-asserted-by":"crossref","first-page":"1102","DOI":"10.1109\/JPROC.2005.849721","volume":"93","author":"J-D Decotignie","year":"2005","unstructured":"Decotignie J-D (2005) Ethernet-based real-time and industrial communications. Proc IEEE 93(6):1102\u20131117","journal-title":"Proc IEEE"},{"key":"1157_CR26","doi-asserted-by":"crossref","unstructured":"Kopetz h, Ademaj A, Grillinger P, Steinhammer K (2005) The time-triggered Ethernet (TTE) design. In: Eighth IEEE international symposium on object-oriented real-time distributed computing (ISORC 2005), Seattle, pp 22\u201333","DOI":"10.1109\/ISORC.2005.56"},{"issue":"2","key":"1157_CR27","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1109\/90.993301","volume":"10","author":"MA Smith","year":"2002","unstructured":"Smith MA, Ramakrishnan KK (2002) Formal specification and verification of safety and performance of TCP selective acknowledgment. IEEE\/ACM Trans Netw 10(2):193\u2013207","journal-title":"IEEE\/ACM Trans Netw"},{"issue":"6","key":"1157_CR28","doi-asserted-by":"crossref","first-page":"1814","DOI":"10.1109\/TNET.2012.2187924","volume":"20","author":"A Wang","year":"2012","unstructured":"Wang A, Jia L, Zhou W, Ren Y, Loo BT, Rexford J, Nigam V, Scedrov A, Talcott C (2012) FSR: formal analysis and implementation toolkit for safe interdomain routing. IEEE\/ACM Trans Netw 20(6):1814\u20131827","journal-title":"IEEE\/ACM Trans Netw"},{"key":"1157_CR29","unstructured":"Thong TV (2012) Formal verification of secure ad-hoc network routing protocols using deductive model-checking, Technical Report. Budapest University of Technology and Economics, Budapest"},{"key":"1157_CR30","unstructured":"de Renesse R, Aghvami AH (2004) Formal verification of ad-hoc routing protocols. Using SPIN model checker. In: Proceedings of IEEE MELECON 2004, Dubrovnik, pp 1177\u20131182"},{"key":"1157_CR31","doi-asserted-by":"crossref","unstructured":"Deng Y, Grumbach S, Monin J-F (2011) A framework for verifying data-centric protocols. In: Bruni R, Dingel J (eds) FMOODS\/FORTE 2011, ser. LNCS, vol 6722. Springer, Reykjavik, pp 106\u2013120","DOI":"10.1007\/978-3-642-21461-5_7"},{"key":"1157_CR32","doi-asserted-by":"crossref","unstructured":"Chen M, Monin J-F (2012) Formal verification of netlog protocols. In: Proceedings of 2012 sixth international symposium on theoretical aspects of software engineering, Beijing, pp 43\u201350","DOI":"10.1109\/TASE.2012.19"},{"key":"1157_CR33","doi-asserted-by":"crossref","unstructured":"Zhou R, Min R, Yu Q, Li CJ, Sheng Y, Zhou QG, Wang X, Li KC (2014) Formal verification of fault-tolerant and recovery mechanisms for safe node sequence protocol. In: The 28th IEEE international conference on advanced information networking and applications (AINA-2014), Victoria","DOI":"10.1109\/AINA.2014.99"},{"key":"1157_CR34","unstructured":"Wei Y-H, Leng Q, Han S, Mok AK, Zhang WL, Tomizuka M (2013) RT-WiFi: real-time high-speed communication protocol for wireless cyber-physical control applications. In: 2013 IEEE 34th real-time systems symposium (RTSS 2013), Vancouver, pp 140\u2013149"},{"key":"1157_CR35","doi-asserted-by":"crossref","unstructured":"Edlinger R, Zauner M, Rokitansky W (2013) RRTLAN\u2014a real-time robot communication protocol stack with multi threading option. In: 2013 IEEE international symposium on safety, security, and rescue robotics (SSRR), Linkoping, pp 1\u20135","DOI":"10.1109\/SSRR.2013.6719319"},{"key":"1157_CR36","unstructured":"Tran AT, Kim MK (2012) A real-time communication protocol considering load balancing in Ad hoc network. In: Proceeding of 2012 7th international forum on strategic technology (IFOST), Tomsk, pp 1\u20134"},{"issue":"1","key":"1157_CR37","first-page":"15","volume":"4","author":"M Yoon","year":"2013","unstructured":"Yoon M, Kim Y-K, Chang J-W (2013) An energy-efficient routing protocol using message success rate in wireless sensor networks. J Converg 4(1):15\u201322","journal-title":"J Converg"},{"issue":"3","key":"1157_CR38","doi-asserted-by":"crossref","first-page":"382","DOI":"10.1145\/357172.357176","volume":"4","author":"L Lamport","year":"1982","unstructured":"Lamport L, Shostak R, Pease M (1982) The Byzantine generals problem. ACM Trans Program Lang Syst 4(3):382\u2013401","journal-title":"ACM Trans Program Lang Syst"},{"key":"1157_CR39","doi-asserted-by":"crossref","unstructured":"Bauer G, Kopetz H, Puschner P (2001) Assumption coverage under different failure modes in the time-triggered architecture. In: Proceedings of 8th IEEE international conference on emerging technologies and factory automation, Antibes-Juan les Pins, pp 333\u2013341","DOI":"10.1109\/ETFA.2001.996386"},{"key":"1157_CR40","volume-title":"Design and verification of computer protocols","author":"GJ Holzmann","year":"1990","unstructured":"Holzmann GJ (1990) Design and verification of computer protocols. Prentice Hall, USA"},{"key":"1157_CR41","volume-title":"Fault-tolerant real-time systems: the problem of replica determinism","author":"S Poledna","year":"1996","unstructured":"Poledna S (1996) Fault-tolerant real-time systems: the problem of replica determinism. Kluwer Academic Publishers, USA"},{"key":"1157_CR42","unstructured":"European Committee for Electrotechnical Standardization (CENELEC)(2001) Railway applications-communication, signalling and processing systems-part 1: Safety-related communication in closed transmission systems, BS EN 50159\u20131, Std"},{"key":"1157_CR43","doi-asserted-by":"crossref","unstructured":"Tovar E, Vasques F (1998) Scheduling real-time communications with P-NET. IEE colloquium on real-time systems (Digest No. 1998\/306), York, pp 9\/1\u20139\/5","DOI":"10.1049\/ic:19980530"},{"issue":"2","key":"1157_CR44","doi-asserted-by":"crossref","first-page":"205","DOI":"10.3745\/JIPS.2013.9.2.205","volume":"9","author":"S Park","year":"2013","unstructured":"Park S, Jung IY, Eom H, Yeom HY (2013) An analysis of replication enhancement for a high availability cluster. J Inf Process Syst 9(2):205\u2013216","journal-title":"J Inf Process Syst"},{"key":"1157_CR45","doi-asserted-by":"crossref","unstructured":"Broster I, Burns A (2003) An analysable bus-guardian for event-triggered communication. In: 24th IEEE real-time systems symposium (RTSS 2003), Cancun, pp 410\u2013419","DOI":"10.1109\/REAL.2003.1253288"},{"key":"1157_CR46","doi-asserted-by":"crossref","unstructured":"Temple C (1998) Avoiding the babbling-idiot failure in a time-triggered communication system. Twenty-eighth annual international symposium on fault-tolerant computing. Munich, pp 218\u2013227","DOI":"10.1109\/FTCS.1998.689473"},{"key":"1157_CR47","doi-asserted-by":"crossref","unstructured":"Rushby J (2002) An overview of formal verification for the time-triggered architecture. In: Proceedings of the 7th international symposium on formal techniques in real-time and fault-tolerant systems: co-sponsored by IFIP WG 2.2, Oldenburg, published in Lecture Notes in Computer Science, vol 2469, pp 83\u2013105","DOI":"10.1007\/3-540-45739-9_7"},{"key":"1157_CR48","volume-title":"The SPIN model checker: primer and reference manual","author":"GJ Holzmann","year":"2003","unstructured":"Holzmann GJ (2003) The SPIN model checker: primer and reference manual. Addison-Wesley, USA"},{"key":"1157_CR49","unstructured":"Li CJ, McGuire N, Zhou QG, Yang MQ (2010) Using spin model checking for node sequence protocol verification. In: Proceedings of 12th real-time Linux workshop, Nairobi"},{"issue":"3","key":"1157_CR50","doi-asserted-by":"crossref","first-page":"382","DOI":"10.1145\/357172.357176","volume":"4","author":"L Lamport","year":"1982","unstructured":"Lamport L, Shostak R, Pease M (1982) The Byzantine general problem. ACM Trans Program Lang Syst 4(3):382\u2013401","journal-title":"ACM Trans Program Lang Syst"},{"key":"1157_CR51","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511810275","volume-title":"Logic in Computer science: modelling and reasoning about systems","author":"M Huth","year":"2004","unstructured":"Huth M, Ryan M (2004) Logic in Computer science: modelling and reasoning about systems, 2nd edn. Cambridge University Press, UK","edition":"2"},{"key":"1157_CR52","unstructured":"Schwarz M (2002) Implementation of a TTP\/C cluster based on commercial gigabit ethernet components, Master Thesis. Technische Universit\u00e4t Wien, Vienna"}],"container-title":["The Journal of Supercomputing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11227-014-1157-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11227-014-1157-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11227-014-1157-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,8]],"date-time":"2019-08-08T14:41:57Z","timestamp":1565275317000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11227-014-1157-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,3,18]]},"references-count":52,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2014,9]]}},"alternative-id":["1157"],"URL":"https:\/\/doi.org\/10.1007\/s11227-014-1157-2","relation":{},"ISSN":["0920-8542","1573-0484"],"issn-type":[{"value":"0920-8542","type":"print"},{"value":"1573-0484","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,3,18]]}}}