返回
A formal specification animation method for operation validation
DOI:10.1016/j.jss.2021.110948.png)
摘要
En 中文
Formal specification can benefit software quality by precisely defining the behaviors of operations to prevent primary mistakes in the early phase of software projects, but a remaining challenge is how such a specification can be checked comprehensibly to show whether it satisfies the user's perception of requirements. In this paper, we describe a new technique for animating operation specifications as a means to address this problem. The technique offers new ways to do (1) automatic animation data generation for both input and output of an operation based on pre-and post-conditions, (2) visualized demonstration of the relationships between input and the corresponding output, (3) comprehensible animation of data items, and (4) illustrative animation of logical expressions and the operators used in them. We discuss these issues and present a prototype tool that supports the automation of the proposed technique. We also report an industrial application as a trial experiment to validate the technique. Finally, we conclude the paper and point out future research directions. (C) 2021 Elsevier Inc. All rights reserved.
Keyword:
Formal specification
Specification animation
Verification and validation
AI总结
对已上传原文的论文进行重点信息的提取,主要内容包括:简要概述、研究摘要、背景介绍、关键亮点、图文解析、展望与总结。
期刊
IF:
4.1
论文数:
5.4K
被引数:
8.4K
机构
引用论文
Protocol for the evaluation of cost-effectiveness and health equity impact of a school-based tobacco prevention programme in a cluster randomised controlled trial (the TOPAS study)
BMJ Open
IF0

