nach oben

Erschienen in:

2019 | OriginalPaper | Buchkapitel

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

verfasst von : Wiktor B. Daszczuk

Erschienen in: Intelligent Methods and Big Data in Industrial Applications

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Zero-Overhead Monitoring of Remote Terminal Devices

Nächstes Kapitel Implementing the Bus Protocol of a Microprocessor in a Software-Defined Computer

We do not use the term “system state” to avoid ambiguity.

Lewerentz, C., Lindner, T. (eds.): Formal Development of Reactive Systems. Springer, Berlin, Heidelberg (1995). https://doi.org/10.1007/3-540-58867-1MATH

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_16CrossRef

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/

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-5CrossRef

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

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

Lötzbeyer, A., Mühlfeld, R.: Task description of a flexible production cell with real time properties, FZI Technical Report, University of Karlsruhe (1996)

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

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/bxw099CrossRef

10.

Dedan, http://staff.ii.pw.edu.pl/dedan/files/DedAn.zip

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.

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.

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_31CrossRef

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.

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.10CrossRef

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_9

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.

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-Z

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.

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.

Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666–677 (1978). https://doi.org/10.1145/359576.359585CrossRefMATH

22.

Milner, R.: A Calculus of Communicating Systems. Springer, Berlin, Heidelberg (1984). ISBN 0387102353MATH

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_9

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_42

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_13CrossRef

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:1021758401878CrossRefMATH

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.005MathSciNetCrossRefMATH

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.

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.

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_29CrossRef

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.

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/S0960129514000164MathSciNetCrossRefMATH

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_20

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_6CrossRef

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.197322CrossRef

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_10

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.pdf

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.

Barbey, S., Buchs, D., Péraire, C.: A Case Study for Testing Object-Oriented Software: A Production Cell. Swiss Federal Institute of Technology (1998)

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_27

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.

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.

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_13CrossRef

Titel: Asynchronous Specification of Production Cell Benchmark in Integrated Model of Distributed Systems
verfasst von: Wiktor B. Daszczuk
Verlag: Springer International Publishing
Buch: Intelligent Methods and Big Data in Industrial Applications
Print ISBN: 978-3-319-77603-3

Electronic ISBN: 978-3-319-77604-0

Copyright-Jahr: 2019
DOI: https://doi.org/10.1007/978-3-319-77604-0_9

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"