Process models in general, and those specifying process-oriented software in particular, should be formally verified. While activity-oriented process models have been verified against object life cycles, formally specified semantic specifications of actions were not involved. Hence, previous approaches for the verification of process models did not make use ofdeclarativelyrepresented knowledge of actions. This paper presents a new approach for verification of consistency between process models, object life cycles, and context-dependent semantic action specifications. This approach involves declarative specifications of all the actions of a process, which also depend on the context of use of the actions. These context-dependent specifications define the ‘logic’ of the process flow, which is grounded in (extended) object life cycles. Since asubtypingrelation is enforced, reuse is facilitated through substitutability. Our extension of object life cycles makes them applicable to processes including non-monotonicity, and even to model communication based on physical interaction in cyber-physical systems. As a consequence, this formal consistency verification ensures that all the involved specifications ‘fit together’, both procedurally and logically.

Formal design verification receives increased importance since the complexity of safety-critical technical applications steadily increases. In this paper, we describe an approach for symbolic model checking of collaborative robotic systems against safety properties. In particular, the methodology presented enables verification even under system modifications and adaptive behavior generally represented as variability. Architectural, behavioral and environmental models are correspondingly abstracted to reach a balance of generality and verifiability with reasonable effort. To demonstrate the proposed method, we use the model of a collaborative assembly use case and formally verify the existence of mechanical clamping hazards between the robot’s moving end effector and static environment objects.

Feature-based systems may have interacting features, where undesired feature interaction(s) may even lead to safety-critical behavior in cyber-physical systems. Automotive systems are such systems, where more and more features are currently being integrated, which have to be coordinated. Automated and formal verification of the resulting behavior against safetyrelevant properties is important, and it should not be restricted to the cyber-part (inside the software implementing the features.)In order to address this problem, we investigate coordination of physical feature interactions in this context using model checking. In particular, we created and used a qualitative model for formal verification against a property in time logic. This model is intended to be minimalist, in particular the logical model based on a physical model (including speed and distance). This logical model defines the essence of operations in the dedicated environment. As a result, we formally verified the high-level logic of a composite feature to be used in automotive systems against a formalized accident property. In summary, we employ minimalist qualitative models for model checking (safety-critical) cyberphysical feature coordination. Such a verified qualitative model may provide a reference model for both quantitative models and real software implementations.