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.
* presented citation count is obtained through Internet information analysis and it is close to the number calculated by the Publish or Perish system.