Scholarlink

<p>Visual animation of formal specifications is useful for validation because it facilitates showing visually that the specifications satisfy the user’s perception of requirements. The technique is especially useful for domain experts who would not be expected to understand formal specifications. However, in most tools, the development of a visual animation is done by formal methods engineers and requires skills in various technologies (e.g. Flash, JavaScript, SVG). Our work contributes toward the tools that are dedicated to the B method, such as B-Motion Studio, VisB, etc. In this paper, we show how visual animation can be done using a domain-specific language (DSL), which is expected to be used by domain experts. The advantage is that the mapping between the DSL and the formal specification is written in B itself. The proposed approach is supported by Meeduse, a language workbench built on ProB, an animator and model-checker of the B method. This paper also explains the DSL tool where the mappings between the DSL and formal specification are generated in a semi-automated way.</p>

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

Visual animation of B specifications using executable DSLs

  • 期刊论文

  • 发表日期：

    2025年6月3日

查看全文
  • Asfand Yar,
  • Akram Idani,
  • Yves Ledru,
  • Simon Collart-Dutilleul

摘要

Visual animation of formal specifications is useful for validation because it facilitates showing visually that the specifications satisfy the user’s perception of requirements. The technique is especially useful for domain experts who would not be expected to understand formal specifications. However, in most tools, the development of a visual animation is done by formal methods engineers and requires skills in various technologies (e.g. Flash, JavaScript, SVG). Our work contributes toward the tools that are dedicated to the B method, such as B-Motion Studio, VisB, etc. In this paper, we show how visual animation can be done using a domain-specific language (DSL), which is expected to be used by domain experts. The advantage is that the mapping between the DSL and the formal specification is written in B itself. The proposed approach is supported by Meeduse, a language workbench built on ProB, an animator and model-checker of the B method. This paper also explains the DSL tool where the mappings between the DSL and formal specification are generated in a semi-automated way.