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

Wiktor B. Daszczuk

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 autom-ata. 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 pro-pose the application of fully asynchronous IMDS (Integrated Model of Distrib-uted Systems) formalism. In our model the subcontrollers do not use any com-mon variables or intermediate states. We apply distributed negotiations between subcontrollers using a simple protocol. The verification is based on CTL (Com-putation Tree Logic) model checking integrated with IMDS.
Author Wiktor B. Daszczuk (FEIT / IN)
Wiktor B. Daszczuk,,
- The Institute of Computer Science
Pages115-129
Publication size in sheets0.7
Book Bembenik Robert, Skonieczny Łukasz, Protaziuk Grzegorz M., Kryszkiewicz Marzena, Rybiński Henryk (eds.): Intelligent Methods and Big Data in Industrial Applications, Studies in Big Data, vol. 40, 2018, Springer International Publishing, ISBN 978-3-319-77603-3, [978-3-319-77604-0], 376 p., DOI:10.1007/978-3-319-77604-0
Keywords in EnglishProduction Cell, Distributed system specification, Distributed sys-tem verification, Asynchronous systems, Communication duality.
DOIDOI:10.1007/978-3-319-77604-0_9
URL https://www.springer.com/la/book/9783319776033
Languageen angielski
File
PCell4.pdf 993.7 KB
Score (nominal)15
ScoreMinisterial score = 15.0, 26-06-2018, BookChapterSeriesAndMatConf
Ministerial score (2013-2016) = 15.0, 26-06-2018, BookChapterSeriesAndMatConf
Citation count*2 (2018-05-10)
Cite
Share Share

Get link to the record


* presented citation count is obtained through Internet information analysis and it is close to the number calculated by the Publish or Perish system.
Back