MBF WorkflowModel-Based Formal Specification and Verification of Robotic Systemshttps://repo.valu3s.eu/use-cases/uc11-automated-robot-inspection-cell-for-quality-control-of-automotive-body-in-white/workflow/mbf-workflowhttps://repo.valu3s.eu/@@site-logo/logo_valu3s_green_transparent.png
MBF Workflow
Model-Based Formal Specification and Verification of Robotic Systems
The workflow starts with user requirement specifications and functional descriptions. Then, the state-based models are created as well as defining formal specifications of requirements. Creating models becomes easy with the use of a model pattern library. The formal specification of requirements also contains the pre-specified regulations for robotic systems. The user just selects the related regulations. Next, the state-based models are verified based on the formal specifications by utilizing model checking. If the models are verified based on the specifications, the next verification stage is runtime verification. Otherwise, the models are revised by the user. At the next verification stage, specifications, state-based models, and codes are used to generate a monitor needed for runtime verification. Next, runtime verification is implemented by running the monitor and the programs of the system concurrently. Collision/kinematics checkers supports the safety verification of the running programs of robotic systems. If the programs during execution are verified based on the specifications, the workflow ends. Otherwise, the user needs to revise the codes.