We use a railway-related case study to illustrate the differences that can be encountered while modeling and verifying a system using an academic formal verification framework and an industrial model-based framework. The different roles and structures of the two approaches are illustrated. We analyze instances where the exclusive use of interactive simulation cannot replicate the formal verification activity, and we derive some future research directions.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Comparing Model Checking and Model-Based Simulation

  • Davide Basile,
  • Franco Mazzanti

摘要

We use a railway-related case study to illustrate the differences that can be encountered while modeling and verifying a system using an academic formal verification framework and an industrial model-based framework. The different roles and structures of the two approaches are illustrated. We analyze instances where the exclusive use of interactive simulation cannot replicate the formal verification activity, and we derive some future research directions.