Asynchronous Specification of Production Cell Benchmark in Integrated Model of Distributed Systems
Wiktor B. Daszczuk
AbstractThere 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.
|Publication size in sheets||0.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 English||Production Cell, Distributed system specification, Distributed sys-tem verification, Asynchronous systems, Communication duality.|
|Score|| = 15.0, 26-06-2018, BookChapterSeriesAndMatConf|
= 15.0, 26-06-2018, BookChapterSeriesAndMatConf
|Citation count*||2 (2018-05-10)|
* presented citation count is obtained through Internet information analysis and it is close to the number calculated by the Publish or Perish system.