{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T14:20:43Z","timestamp":1725978043557},"publisher-location":"Cham","reference-count":43,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319776033"},{"type":"electronic","value":"9783319776040"}],"license":[{"start":{"date-parts":[[2018,5,19]],"date-time":"2018-05-19T00:00:00Z","timestamp":1526688000000},"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":[[2019]]},"DOI":"10.1007\/978-3-319-77604-0_9","type":"book-chapter","created":{"date-parts":[[2018,5,18]],"date-time":"2018-05-18T02:57:28Z","timestamp":1526612248000},"page":"115-129","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Asynchronous Specification of Production Cell Benchmark in Integrated Model of Distributed Systems"],"prefix":"10.1007","author":[{"given":"Wiktor B.","family":"Daszczuk","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,5,19]]},"reference":[{"key":"9_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58867-1","volume-title":"Formal Development of Reactive Systems","year":"1995","unstructured":"Lewerentz, C., Lindner, T. (eds.): Formal Development of Reactive Systems. Springer, Berlin, Heidelberg (1995). \nhttps:\/\/doi.org\/10.1007\/3-540-58867-1"},{"key":"9_CR2","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-540-32008-1_16","volume-title":"Operational Semantics for Timed Systems","author":"Heinrich Rust","year":"2005","unstructured":"Rust, H.: A production cell with timing. In: Operational Semantics for Timed Systems, pp. 173\u2013201. Springer, Berlin, Heidelberg (2005). \nhttps:\/\/doi.org\/10.1007\/978-3-540-32008-1_16"},{"key":"9_CR3","unstructured":"Flordal, H., Malik, R.: Modular nonblocking verification using conflict equivalence. In: 8th International Workshop on Discrete Event Systems, pp. 100\u2013106. IEEE (2006). \nhttp:\/\/ieeexplore.ieee.org\/document\/1678415\/"},{"issue":"3","key":"9_CR4","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/s00165-008-0068-5","volume":"21","author":"Peter Gorm Larsen","year":"2008","unstructured":"Larsen, P.G., Fitzgerald, J.S., Riddle, S.: Practice-oriented courses in formal methods using VDM++. Form. Asp. Comput. 21(3), 245\u2013257 (2009). \nhttps:\/\/link.springer.com\/article\/10.1007%2Fs00165-008-0068-5","journal-title":"Formal Aspects of Computing"},{"key":"9_CR5","unstructured":"El-Ansary, A., Elgazzar, M.M.: Real-time system using the behavioral patterns analysis (BPA). Int. J. Innov. Res. Adv. Eng. 1(10), 233\u2013245 (2014). http:\/\/www.ijirae.com\/volumes\/vol1\/issue10\/39.NVEC10091.pdf"},{"key":"9_CR6","doi-asserted-by":"publisher","unstructured":"Zimmermann, A.: Model-based design and control of a production cell. In: Stochastic Discrete Event Systems: Modeling, Evaluation, Applications, pp. 325\u2013340. Springer, Berlin, Heidelberg (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-74173-2_16","DOI":"10.1007\/978-3-540-74173-2_16"},{"key":"9_CR7","unstructured":"L\u00f6tzbeyer, A., M\u00fchlfeld, R.: Task description of a flexible production cell with real time properties, FZI Technical Report, University of Karlsruhe (1996)"},{"key":"9_CR8","unstructured":"Chrobot, S., Daszczuk, W.B.: Communication dualism in distributed systems with Petri net interpretation. Theor. Appl. Inform. 18(4), 261\u2013278 (2006). \nhttps:\/\/taai.iitis.pl\/taai\/article\/view\/250\/taai-vol.18-no.4-pp.261"},{"issue":"5","key":"9_CR9","doi-asserted-by":"publisher","first-page":"729","DOI":"10.1093\/comjnl\/bxw099","volume":"60","author":"WB Daszczuk","year":"2017","unstructured":"Daszczuk, W.B.: Communication and resource deadlock analysis using IMDS formalism and model checking. Comput. J. 60(5), 729\u2013750 (2017). \nhttps:\/\/doi.org\/10.1093\/comjnl\/bxw099","journal-title":"Comput. J."},{"key":"9_CR10","unstructured":"Dedan, \nhttp:\/\/staff.ii.pw.edu.pl\/dedan\/files\/DedAn.zip"},{"key":"9_CR11","unstructured":"Daszczuk, W.B.: Verification of Temporal Properties in Concurrent Systems. PhD Thesis, Warsaw University of Technology (2003). https:\/\/repo.pw.edu.pl\/docstore\/download\/WEiTI-0b7425b5-2375-417b-b0fa-b1f61aed0623\/Daszczuk.pdf"},{"key":"9_CR12","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A Tutorial on Uppaal 4.0. Aalborg University Report, Aalborg, Denmark (2006). http:\/\/www.it.uu.se\/research\/group\/darts\/papers\/texts\/new-tutorial.pdf"},{"key":"9_CR13","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/3-540-48249-0_31","volume-title":"Computer Safety, Reliability and Security","author":"Monika Heiner","year":"1999","unstructured":"Heiner, M., Heisel, M.: Modeling safety-critical systems with Z and Petri nets. In: Felici, M., Kanoun, K., Pasquini, A. (eds.) SAFECOMP \u201999 Proceedings of the 18th International Conference on Computer Safety, Reliability and Security, Toulouse, France, 27\u201329 September 1999. LNCS, vol. 1698, pp. 361\u2013374. Springer, Berlin, Heidelberg (1999). \nhttps:\/\/link.springer.com\/chapter\/10.1007%2F3-540-48249-0_31"},{"key":"9_CR14","doi-asserted-by":"publisher","unstructured":"Greenyer, J., Brenner, C., Cordy, M., Heymans, P., Gressi, E.: Incrementally synthesizing controllers from scenario-based product line specifications. In: Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering\u2014ESEC\/FSE 2013, Sankt Petersburg, Russia, 18\u201326 August 2013, pp. 433\u2013443. ACM Press, New York, NY (2013). \nhttps:\/\/doi.org\/10.1145\/2491411.2491445","DOI":"10.1145\/2491411.2491445"},{"key":"9_CR15","doi-asserted-by":"publisher","first-page":"230","DOI":"10.4204\/EPTCS.244.10","volume":"244","author":"H Garavel","year":"2017","unstructured":"Garavel, H., Serwe, W.: The unheralded value of the multiway rendezvous: illustration with the production cell benchmark. Electron. Proc. Theor. Comput. Sci. 244, 230\u2013270 (2017). \nhttps:\/\/doi.org\/10.4204\/EPTCS.244.10","journal-title":"Electron. Proc. Theor. Comput. Sci."},{"key":"9_CR16","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/978-3-319-17581-2_9","volume-title":"Communications in Computer and Information Science","author":"Jaco Jacobs","year":"2015","unstructured":"Jacobs, J., Simpson, A.: A formal model of SysML blocks using CSP for assured systems engineering. In: Formal Techniques for Safety-Critical Systems, Third International Workshop, FTSCS 2014, Luxembourg, 6\u20137 November 2014. Communications in Computer and Information Science, vol. 476, pp. 127\u2013141. Springer, Berlin, Heidelberg (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-17581-2_9"},{"key":"9_CR17","doi-asserted-by":"publisher","unstructured":"Ma, C., Wonham, W.M.: The production cell example. Chapter 5. In: Nonblocking Supervisory Control of State Tree Structures. LNCIS, vol. 317, pp. 127\u2013144. Springer, Berlin, Heidelberg (2005). \nhttps:\/\/doi.org\/10.1007\/11382119_5","DOI":"10.1007\/11382119_5"},{"issue":"8","key":"9_CR18","first-page":"677","volume":"29","author":"A. F. Zorzo","year":"1999","unstructured":"Zorzo, A.F., Romanovsky, A., Xu, J., Randell, B., Stroud, R.J., Welch, I.S.: Using coordinated atomic actions to design safety-critical systems: a production cell case study. Softw. Pract. Exp. 29(8), 677\u2013697 (1999). https:\/\/doi.org\/10.1002\/(SICI)1097-024X(19990710)29:8<677::AID-SPE251>3.0.CO;2-Z","journal-title":"Software: Practice and Experience"},{"key":"9_CR19","unstructured":"Sokolsky, O., Lee, I., Ben-Abdallah, H.: Specification and Analysis of Real-Time Systems with PARAGON (equivalence checking), Philadelphia, PA (1999). \nhttps:\/\/www.cis.upenn.edu\/~sokolsky\/ase99.pdf"},{"key":"9_CR20","unstructured":"Ramakrishnan, S., McGregor, J.: Modelling and testing OO distributed systems with temporal logic formalisms. In: 8th International IASTED Conference Applied Informatics\u2019 2000, Innsbruck, Austria, 14\u201317 February 2000 (2000). https:\/\/research.monash.edu\/en\/publications\/modelling-and-testing-oo-distributed-systems-with-temporal-logic-"},{"issue":"8","key":"9_CR21","doi-asserted-by":"publisher","first-page":"666","DOI":"10.1145\/359576.359585","volume":"21","author":"CAR Hoare","year":"1978","unstructured":"Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666\u2013677 (1978). \nhttps:\/\/doi.org\/10.1145\/359576.359585","journal-title":"Commun. ACM"},{"key":"9_CR22","isbn-type":"print","volume-title":"A Calculus of Communicating Systems","author":"R Milner","year":"1984","unstructured":"Milner, R.: A Calculus of Communicating Systems. Springer, Berlin, Heidelberg (1984). ISBN 0387102353","ISBN":"http:\/\/id.crossref.org\/isbn\/0387102353"},{"key":"9_CR23","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/11539452_9","volume-title":"Lecture Notes in Computer Science","author":"Franck Cassez","year":"2005","unstructured":"Cassez, F., David, A., Fleury, E., Larsen, K.G., Lime, D.: Efficient on-the-fly algorithms for the analysis of timed games. In: 16th International Conference on Concurrency Theory (CONCUR\u201905), San Francisco, CA, 23\u201326 August 2005. LNCS, vol. 3653, pp. 66\u201380. Springer, Berlin, Heidelberg (2005). \nhttps:\/\/doi.org\/10.1007\/11539452_9"},{"key":"9_CR24","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/3-540-61648-9_42","volume-title":"Lecture Notes in Computer Science","author":"Henning Dierks","year":"1996","unstructured":"Dierks, H.: The production cell: a verified real-time system. In: 4th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems FTRTFT 1996: Uppsala, Sweden, 9\u201313 September 1996. LNCS, vol. 1135, pp. 208\u2013227. Springer, Berlin, Heidelberg (1996). \nhttps:\/\/doi.org\/10.1007\/3-540-61648-9_42"},{"key":"9_CR25","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-540-45069-6_13","volume-title":"Computer Aided Verification","author":"Dirk Beyer","year":"2003","unstructured":"Beyer, D., Lewerentz, C., Noack, A.: Rabbit: a tool for BDD-based verification of real-time systems. In: Computer Aided Verification, CAV 2003, Boulder, CO, 8\u201312 July 2003. LNCS, vol. 2725, pp. 122\u2013125. Springer, Berlin, Heidelberg (2003). \nhttps:\/\/link.springer.com\/chapter\/10.1007%2F978-3-540-45069-6_13"},{"issue":"2","key":"9_CR26","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1023\/A:1021758401878","volume":"24","author":"A Burns","year":"2003","unstructured":"Burns, A.: How to verify a safe real-time system\u2014the application of model checking and timed automata to the production cell case study. Real-Time Syst. 24(2), 135\u2013151 (2003). \nhttps:\/\/doi.org\/10.1023\/A:1021758401878","journal-title":"Real-Time Syst."},{"issue":"1","key":"9_CR27","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/j.scico.2006.08.005","volume":"65","author":"K Benghazi Akhlaki","year":"2007","unstructured":"Benghazi Akhlaki, K., Capel Tu\u00f1\u00f3n, M.I., Holgado Terriza, J.A., Mendoza Morales, L.E.: A methodological approach to the formal specification of real-time systems by transformation of UML-RT design models. Sci. Comput. Program. 65(1), 41\u201356 (2007). \nhttps:\/\/doi.org\/10.1016\/j.scico.2006.08.005","journal-title":"Sci. Comput. Program."},{"key":"9_CR28","unstructured":"Barbey, S., Buchs, D., P\u00e9raire, C.: Modelling the Production Cell Case Study using the Fusion Method. Lausanne, Switzerland (1998). \nhttps:\/\/infoscience.epfl.ch\/record\/54618\/files\/Barbey98\u2013298..ps.gz"},{"key":"9_CR29","unstructured":"Cattel, T.: Process control design using SPIN. In: Spin Workshop, 16 Oct 1995, Montreal, Canada (1995). \nhttp:\/\/spinroot.com\/spin\/Workshops\/ws95\/cattel.pdf"},{"key":"9_CR30","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1007\/3-540-44919-1_29","volume-title":"Applications and Theory of Petri Nets 2003","author":"Claus Schr\u00f6ter","year":"2003","unstructured":"Schr\u00f6ter, C., Schwoon, S., Esparza, J.: The model-checking kit. In: 24th International Conference ICATPN 2003: Eindhoven, The Netherlands, 23\u201327 June 2003. LNCS, vol. 2697, pp. 463\u2013472. Springer, Berlin, Heidelberg (2003). \nhttps:\/\/doi.org\/10.1007\/3-540-44919-1_29"},{"key":"9_CR31","doi-asserted-by":"publisher","unstructured":"Bj\u00f6rnander, S., Seceleanu, C., Lundqvist, K., Pettersson, P.: ABV\u2014a verifier for the architecture analysis and design language (AADL). In: 6th IEEE International Conference on Engineering of Complex Computer Systems, Las Vegas, USA, 27\u201329 April 2011, pp. 355\u2013360. IEEE (2011). \nhttps:\/\/doi.org\/10.1109\/iceccs.2011.43","DOI":"10.1109\/iceccs.2011.43"},{"issue":"02","key":"9_CR32","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1017\/S0960129514000164","volume":"26","author":"S Capecchi","year":"2016","unstructured":"Capecchi, S., Giachino, E., Yoshida, N.: Global escape in multiparty sessions. Math. Struct. Comput. Sci. 26(02), 156\u2013205 (2016). \nhttps:\/\/doi.org\/10.1017\/S0960129514000164","journal-title":"Math. Struct. Comput. Sci."},{"key":"9_CR33","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/3-540-48153-2_20","volume-title":"Lecture Notes in Computer Science","author":"J\u00fcrgen Ruf","year":"1999","unstructured":"Ruf, J., Kropf, T.: Modeling and checking networks of communicating real-time processes. In: CHARME 1999: Correct Hardware Design and Verification Methods, BadHerrenalb, Germany, 27\u201329 September 1999. LNCS, vol. 1704, pp. 267\u2013279. Springer, Berlin, Heidelberg (1999). \nhttps:\/\/doi.org\/10.1007\/3-540-48153-2_20"},{"key":"9_CR34","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/978-1-4615-5229-1_6","volume-title":"Behavioral Specifications of Businesses and Systems","author":"Radu Grosu","year":"1999","unstructured":"Grosu, R., Broy, M., Selic, B., Stef\u0103nescu, G.: What is behind UML-RT? In: Kilov, H., Rumpe, B., Simmonds, I. (eds.) Behavioral Specifications of Businesses and Systems, pp. 75\u201390. Springer US, Boston, MA (1999). \nhttps:\/\/doi.org\/10.1007\/978-1-4615-5229-1_6"},{"issue":"6","key":"9_CR35","doi-asserted-by":"publisher","first-page":"1661","DOI":"10.1145\/197320.197322","volume":"16","author":"JJ \u017dic","year":"1994","unstructured":"\u017dic, J.J.: Time-constrained buffer specifications in CSP + T and timed CSP. ACM Trans. Program. Lang. Syst. 16(6), 1661\u20131674 (1994). \nhttps:\/\/doi.org\/10.1145\/197320.197322","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"9_CR36","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-642-15297-9_10","volume-title":"Lecture Notes in Computer Science","author":"R\u00fcdiger Ehlers","year":"2010","unstructured":"Ehlers, R., Mattm\u00fcller, R., Peter, H.-J.: Combining symbolic representations for solving timed games. In: Chatterjee, K., Henzinger, T.A. (eds.) 8th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2010, Klosterneuburg, Austria, 8\u201310 September 2010. LNCS, vol. 6246, pp. 107\u2013121. Springer, Berlin, Heidelberg (2010). \nhttps:\/\/doi.org\/10.1007\/978-3-642-15297-9_10"},{"key":"9_CR37","unstructured":"Ben-Abdallah, H., Lee, I.: A graphical language for specifying and analyzing real-time systems. Integr. Comput. Aided. Eng. 5(4), 279\u2013302 (1998). ftp:\/\/ftp.cis.upenn.edu\/pub\/rtg\/Paper\/Full_Postscript\/icae97.pdf"},{"key":"9_CR38","unstructured":"Beyer, D., Rust, H.: Modeling a production cell as a distributed real-time system with cottbus timed automata. In: K\u00f6nig, H., Langend\u00f6rfer, P. (eds.) Formale Beschreibungstechniken f\u00fcr verteilte Systeme, 8. GI\/ITG-Fachgespr\u00e4ch, Cottbus, 4\u20135 June 1998. Shaker Verlag, M\u00fcnchen, Germany (1998). \nhttps:\/\/www.sosy-lab.org\/~dbeyer\/Publications\/1998-FBT.Modeling_a_Production_Cell_as_a_Distributed_Real-Time_System_with.Cottbus_Timed_Automata.pdf"},{"key":"9_CR39","unstructured":"Barbey, S., Buchs, D., P\u00e9raire, C.: A Case Study for Testing Object-Oriented Software: A Production Cell. Swiss Federal Institute of Technology (1998)"},{"key":"9_CR40","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/3-540-48254-7_27","volume-title":"Lecture Notes in Computer Science","author":"H\u00e9l\u00e8ne Waeselynck","year":"1999","unstructured":"Waeselynck, H., Th\u00e9venod-Fosse, P.: A case study in statistical testing of reusable concurrent objects. In: Third European Dependable Computing Conference Prague, Czech Republic, 15\u201317 September 1999, LNCS, vol. 1667, pp. 401\u2013418. Springer, Berlin, Heidelberg (1999). \nhttps:\/\/doi.org\/10.1007\/3-540-48254-7_27"},{"key":"9_CR41","doi-asserted-by":"publisher","unstructured":"Daszczuk, W.B.: Evaluation of temporal formulas based on \u201cchecking by spheres.\u201d In: Proceedings Euromicro Symposium on Digital Systems Design, Warsaw, Poland, 4\u20136 September 2001, pp. 158\u2013164. IEEE Computer Socity, New York, NY (2001). \nhttps:\/\/doi.org\/10.1109\/dsd.2001.952267","DOI":"10.1109\/dsd.2001.952267"},{"key":"9_CR42","unstructured":"Czejdo, B., Bhattacharya, S., Baszun, M., Daszczuk, W.B.: Improving resilience of autonomous moving platforms by real-time analysis of their cooperation. Autobusy-TEST 17(6), 1294\u20131301 (2016). \nhttp:\/\/www.autobusy-test.com.pl\/images\/stories\/Do_pobrania\/2016\/nr%206\/logistyka\/10_l_czejdo_bhattacharya_baszun_daszczuk.pdf"},{"key":"9_CR43","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/978-3-642-41569-2_13","volume-title":"Evolution of Telecommunication Services","author":"Gyu Myoung Lee","year":"2013","unstructured":"Lee, G.M., Crespi, N., Choi, J.K., Boussard, M.: Internet of Things. In: Evolution of Telecommunication Services. LNCS, vol. 7768, pp. 257\u2013282. Springer, Berlin Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-41569-2_13"}],"container-title":["Studies in Big Data","Intelligent Methods and Big Data in Industrial Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-77604-0_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,5,18]],"date-time":"2018-05-18T03:00:14Z","timestamp":1526612414000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-77604-0_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,5,19]]},"ISBN":["9783319776033","9783319776040"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-77604-0_9","relation":{},"ISSN":["2197-6503","2197-6511"],"issn-type":[{"type":"print","value":"2197-6503"},{"type":"electronic","value":"2197-6511"}],"subject":[],"published":{"date-parts":[[2018,5,19]]}}}