• Introduction

• Manual

• Tutorial

• Case Study

• Supplemental Material

Introduction to MoVe4BT

Workflow

First, users can create the BT structure and specify the detailed semantics of each node, including the manipulations of data, the data constraints, the execution time, etc. Then, task requirements can be specified as the verification properties, including the timed properties. After completing the modeling of the BT, the corresponding Timed CSP_bt model will be automatically generated. Based on the properties, a model checking-based verification process will be carried out. If the model does not satisfy the property, a counterexample will be generated to guide users to fix the errors in the BT.

Contacts

Please feel free to contact us if you have any questions about MoVe4BT.

• Peishan Huang (huang_ps@nudt.edu.cn)
• Weijiang Hong (hongweijiang17@nudt.edu.cn)
• Zhenbang Chen (zbchen@nudt.edu.cn)
• Ji Wang (wj@nudt.edu.cn)