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.

Extensible Markup Language (XML) EA_UC11_MBF.xml — Extensible Markup Language (XML), 470 KB
Contents

There are currently no items in this folder.