Anmerkungen:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Beschreibung:
Coordinated atomic actions (CAAs) have been used in a semi-formal way for the design of the production cell case study. This paper presents a formal specification and verification of the production cell building on this design. However, this report is not intended to present yet another formalization of the production cell case study but rather as an approach to formalizing a CAA based system design in order to formally verify its properties. Each CAA is modeled as an atomic state transition characterized by its pre- and postconditions. In order for such transitions to become enabled, conditions are formalized requiring all associated roles to be activated. Activation of roles is performed by controllers, which are again modeled in terms of state transitions. The state space of the production cell can be viewed as being finite; hence, the production cell is specified as a finite state transition system and the formal verification of the CAA-design is carried out using model-checking.