Asynchronous Specification of Production Cell Benchmark in Integrated Model of Distributed Systems

Chapter
Part of the Studies in Big Data book series (SBD, volume 40)

Abstract

There are many papers concerning well-known Karlsruhe Production Cell benchmark. They focus on specification of the controller—which leads to a synthesis of working controller—or verification of its operation. The controller is modeled using various methods: programming languages, algebras or automata. Verification is based on testing, bisimulation or temporal model checking. Most models are synchronous. Asynchronous specifications use one- or multi-element buffers to relax the dependence of component subcontrollers. We propose the application of fully asynchronous IMDS (Integrated Model of Distributed Systems) formalism. In our model the subcontrollers do not use any common variables or intermediate states. We apply distributed negotiations between subcontrollers using a simple protocol. The verification is based on CTL (Computation Tree Logic) model checking integrated with IMDS.

Keywords

Production Cell Distributed system specification Distributed system verification Asynchronous systems Communication duality 

References

  1. 1.
    Lewerentz, C., Lindner, T. (eds.): Formal Development of Reactive Systems. Springer, Berlin, Heidelberg (1995).  https://doi.org/10.1007/3-540-58867-1MATHGoogle Scholar
  2. 2.
    Rust, H.: A production cell with timing. In: Operational Semantics for Timed Systems, pp. 173–201. Springer, Berlin, Heidelberg (2005).  https://doi.org/10.1007/978-3-540-32008-1_16CrossRefGoogle Scholar
  3. 3.
    Flordal, H., Malik, R.: Modular nonblocking verification using conflict equivalence. In: 8th International Workshop on Discrete Event Systems, pp. 100–106. IEEE (2006). http://ieeexplore.ieee.org/document/1678415/
  4. 4.
    Larsen, P.G., Fitzgerald, J.S., Riddle, S.: Practice-oriented courses in formal methods using VDM++. Form. Asp. Comput. 21(3), 245–257 (2009). https://link.springer.com/article/10.1007%2Fs00165-008-0068-5CrossRefGoogle Scholar
  5. 5.
    El-Ansary, A., Elgazzar, M.M.: Real-time system using the behavioral patterns analysis (BPA). Int. J. Innov. Res. Adv. Eng. 1(10), 233–245 (2014). http://www.ijirae.com/volumes/vol1/issue10/39.NVEC10091.pdf
  6. 6.
    Zimmermann, A.: Model-based design and control of a production cell. In: Stochastic Discrete Event Systems: Modeling, Evaluation, Applications, pp. 325–340. Springer, Berlin, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-74173-2_16
  7. 7.
    Lötzbeyer, A., Mühlfeld, R.: Task description of a flexible production cell with real time properties, FZI Technical Report, University of Karlsruhe (1996)Google Scholar
  8. 8.
    Chrobot, S., Daszczuk, W.B.: Communication dualism in distributed systems with Petri net interpretation. Theor. Appl. Inform. 18(4), 261–278 (2006). https://taai.iitis.pl/taai/article/view/250/taai-vol.18-no.4-pp.261
  9. 9.
    Daszczuk, W.B.: Communication and resource deadlock analysis using IMDS formalism and model checking. Comput. J. 60(5), 729–750 (2017).  https://doi.org/10.1093/comjnl/bxw099CrossRefGoogle Scholar
  10. 10.
  11. 11.
    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
  12. 12.
    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
  13. 13.
    Heiner, M., Heisel, M.: Modeling safety-critical systems with Z and Petri nets. In: Felici, M., Kanoun, K., Pasquini, A. (eds.) SAFECOMP ’99 Proceedings of the 18th International Conference on Computer Safety, Reliability and Security, Toulouse, France, 27–29 September 1999. LNCS, vol. 1698, pp. 361–374. Springer, Berlin, Heidelberg (1999). https://link.springer.com/chapter/10.1007%2F3-540-48249-0_31CrossRefGoogle Scholar
  14. 14.
    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—ESEC/FSE 2013, Sankt Petersburg, Russia, 18–26 August 2013, pp. 433–443. ACM Press, New York, NY (2013).  https://doi.org/10.1145/2491411.2491445
  15. 15.
    Garavel, H., Serwe, W.: The unheralded value of the multiway rendezvous: illustration with the production cell benchmark. Electron. Proc. Theor. Comput. Sci. 244, 230–270 (2017).  https://doi.org/10.4204/EPTCS.244.10CrossRefGoogle Scholar
  16. 16.
    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–7 November 2014. Communications in Computer and Information Science, vol. 476, pp. 127–141. Springer, Berlin, Heidelberg (2015).  https://doi.org/10.1007/978-3-319-17581-2_9Google Scholar
  17. 17.
    Ma, C., Wonham, W.M.: The production cell example. Chapter 5. In: Nonblocking Supervisory Control of State Tree Structures. LNCIS, vol. 317, pp. 127–144. Springer, Berlin, Heidelberg (2005).  https://doi.org/10.1007/11382119_5
  18. 18.
    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–697 (1999). https://doi.org/10.1002/(SICI)1097-024X(19990710)29:8<677::AID-SPE251>3.0.CO;2-ZGoogle Scholar
  19. 19.
    Sokolsky, O., Lee, I., Ben-Abdallah, H.: Specification and Analysis of Real-Time Systems with PARAGON (equivalence checking), Philadelphia, PA (1999). https://www.cis.upenn.edu/~sokolsky/ase99.pdf
  20. 20.
    Ramakrishnan, S., McGregor, J.: Modelling and testing OO distributed systems with temporal logic formalisms. In: 8th International IASTED Conference Applied Informatics’ 2000, Innsbruck, Austria, 14–17 February 2000 (2000). https://research.monash.edu/en/publications/modelling-and-testing-oo-distributed-systems-with-temporal-logic-
  21. 21.
    Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666–677 (1978).  https://doi.org/10.1145/359576.359585CrossRefMATHGoogle Scholar
  22. 22.
    Milner, R.: A Calculus of Communicating Systems. Springer, Berlin, Heidelberg (1984). ISBN 0387102353MATHGoogle Scholar
  23. 23.
    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’05), San Francisco, CA, 23–26 August 2005. LNCS, vol. 3653, pp. 66–80. Springer, Berlin, Heidelberg (2005).  https://doi.org/10.1007/11539452_9Google Scholar
  24. 24.
    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–13 September 1996. LNCS, vol. 1135, pp. 208–227. Springer, Berlin, Heidelberg (1996).  https://doi.org/10.1007/3-540-61648-9_42Google Scholar
  25. 25.
    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–12 July 2003. LNCS, vol. 2725, pp. 122–125. Springer, Berlin, Heidelberg (2003). https://link.springer.com/chapter/10.1007%2F978-3-540-45069-6_13CrossRefGoogle Scholar
  26. 26.
    Burns, A.: How to verify a safe real-time system—the application of model checking and timed automata to the production cell case study. Real-Time Syst. 24(2), 135–151 (2003).  https://doi.org/10.1023/A:1021758401878CrossRefMATHGoogle Scholar
  27. 27.
    Benghazi Akhlaki, K., Capel Tuñón, 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–56 (2007).  https://doi.org/10.1016/j.scico.2006.08.005MathSciNetCrossRefMATHGoogle Scholar
  28. 28.
    Barbey, S., Buchs, D., Péraire, C.: Modelling the Production Cell Case Study using the Fusion Method. Lausanne, Switzerland (1998). https://infoscience.epfl.ch/record/54618/files/Barbey98–298..ps.gz
  29. 29.
    Cattel, T.: Process control design using SPIN. In: Spin Workshop, 16 Oct 1995, Montreal, Canada (1995). http://spinroot.com/spin/Workshops/ws95/cattel.pdf
  30. 30.
    Schröter, C., Schwoon, S., Esparza, J.: The model-checking kit. In: 24th International Conference ICATPN 2003: Eindhoven, The Netherlands, 23–27 June 2003. LNCS, vol. 2697, pp. 463–472. Springer, Berlin, Heidelberg (2003).  https://doi.org/10.1007/3-540-44919-1_29CrossRefGoogle Scholar
  31. 31.
    Björnander, S., Seceleanu, C., Lundqvist, K., Pettersson, P.: ABV—a verifier for the architecture analysis and design language (AADL). In: 6th IEEE International Conference on Engineering of Complex Computer Systems, Las Vegas, USA, 27–29 April 2011, pp. 355–360. IEEE (2011).  https://doi.org/10.1109/iceccs.2011.43
  32. 32.
    Capecchi, S., Giachino, E., Yoshida, N.: Global escape in multiparty sessions. Math. Struct. Comput. Sci. 26(02), 156–205 (2016).  https://doi.org/10.1017/S0960129514000164MathSciNetCrossRefMATHGoogle Scholar
  33. 33.
    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–29 September 1999. LNCS, vol. 1704, pp. 267–279. Springer, Berlin, Heidelberg (1999).  https://doi.org/10.1007/3-540-48153-2_20Google Scholar
  34. 34.
    Grosu, R., Broy, M., Selic, B., Stefănescu, G.: What is behind UML-RT? In: Kilov, H., Rumpe, B., Simmonds, I. (eds.) Behavioral Specifications of Businesses and Systems, pp. 75–90. Springer US, Boston, MA (1999).  https://doi.org/10.1007/978-1-4615-5229-1_6CrossRefGoogle Scholar
  35. 35.
    Žic, J.J.: Time-constrained buffer specifications in CSP + T and timed CSP. ACM Trans. Program. Lang. Syst. 16(6), 1661–1674 (1994).  https://doi.org/10.1145/197320.197322CrossRefGoogle Scholar
  36. 36.
    Ehlers, R., Mattmüller, 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–10 September 2010. LNCS, vol. 6246, pp. 107–121. Springer, Berlin, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-15297-9_10Google Scholar
  37. 37.
    Ben-Abdallah, H., Lee, I.: A graphical language for specifying and analyzing real-time systems. Integr. Comput. Aided. Eng. 5(4), 279–302 (1998). ftp://ftp.cis.upenn.edu/pub/rtg/Paper/Full_Postscript/icae97.pdfGoogle Scholar
  38. 38.
    Beyer, D., Rust, H.: Modeling a production cell as a distributed real-time system with cottbus timed automata. In: König, H., Langendörfer, P. (eds.) Formale Beschreibungstechniken für verteilte Systeme, 8. GI/ITG-Fachgespräch, Cottbus, 4–5 June 1998. Shaker Verlag, München, Germany (1998). https://www.sosy-lab.org/~dbeyer/Publications/1998-FBT.Modeling_a_Production_Cell_as_a_Distributed_Real-Time_System_with.Cottbus_Timed_Automata.pdf
  39. 39.
    Barbey, S., Buchs, D., Péraire, C.: A Case Study for Testing Object-Oriented Software: A Production Cell. Swiss Federal Institute of Technology (1998)Google Scholar
  40. 40.
    Waeselynck, H., Thévenod-Fosse, P.: A case study in statistical testing of reusable concurrent objects. In: Third European Dependable Computing Conference Prague, Czech Republic, 15–17 September 1999, LNCS, vol. 1667, pp. 401–418. Springer, Berlin, Heidelberg (1999).  https://doi.org/10.1007/3-540-48254-7_27Google Scholar
  41. 41.
    Daszczuk, W.B.: Evaluation of temporal formulas based on “checking by spheres.” In: Proceedings Euromicro Symposium on Digital Systems Design, Warsaw, Poland, 4–6 September 2001, pp. 158–164. IEEE Computer Socity, New York, NY (2001).  https://doi.org/10.1109/dsd.2001.952267
  42. 42.
    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–1301 (2016). http://www.autobusy-test.com.pl/images/stories/Do_pobrania/2016/nr%206/logistyka/10_l_czejdo_bhattacharya_baszun_daszczuk.pdf
  43. 43.
    Lee, G.M., Crespi, N., Choi, J.K., Boussard, M.: Internet of Things. In: Evolution of Telecommunication Services. LNCS, vol. 7768, pp. 257–282. Springer, Berlin Heidelberg (2013).  https://doi.org/10.1007/978-3-642-41569-2_13CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2019

Authors and Affiliations

  1. 1.Warsaw University of Technology, Institute of Computer ScienceWarsawPoland

Personalised recommendations