【免费】SOFL形式化规范中流程输入输出自动可视化的设计与实现资源-CSDN文库

毕业设计

需积分: 0 17 浏览量 2023-04-09 10:11:28 上传评论收藏 286KB PDF 举报

资源推荐

资源详情

资源评论

David C. Wyld et al. (Eds) : NeCoM, SEAS, SP, CMCA - 2018

pp. 33–48, 2018. © CS & IT-CSCP 2018 DOI : 10.5121/csit.2018.80903

UTOMATED

ISUALIZATION

NPUT

UTPUT

ROCESSES IN

SOFL

ORMAL

PECIFICATIONS

Yu Chen

and Shaoying Liu

Graduate School of Computer and Information Sciences, Hosei University,

Japan

Faculty of Computer and Information Sciences, Hosei University, Japan

BSTRACT

While formal specification is regarded as an effective means to capture accurate requirements

and design, validation of the specifications remains a challenge. Specification animation has

been proposed to tackle the challenge, but lacking an effective representation of the input/output

data in the animation can considerably limit the understanding of the animation by clients. In

this paper, we put forward a tool supported technique for visualization of the input/output data

of processes in SOFL formal specifications. After discussing the motives of our work, we

describe how data of each kind of data type available in the SOFL language can be visualized to

facilitate the representation and understanding of input/output data. We also present a

supporting tool for the technique and a case study to demonstrate the usability and effectiveness

of our proposed technique. Finally, we conclude the paper and point out the future research

directions.

EYWORDS

Visualization, SOFL, Formal specification, Data type, Formal methods

NTRODUCTION

Formal specification has proved to be effective to help capture accurate requirements and design

in software development if used properly together with practical engineering approaches [1].

While this can considerably contribute to the communication between the developers in a

software project, it may not effectively facilitate the communication between the developer and

the client due to the fact that mathematical expressions in the formal specification can be difficult

for the client to understand in general. Therefore, a potential risk that the formal specification

may not correctly and completely define what the client really wants will eventually affect the

reliability of the software.

To tackle this problem, formal specification animation has been proposed [2]. The common

characteristic of the existing animation techniques is to use test data (also called animation data)

to dynamically demonstrate the input-output relation for operations defined in the specification.

Compared to the reading and understanding technique, animation is proved to be more effective

in validating formal specifications against the client’s requirements [3][4]. However, our

experience and study suggest that the effect of specification animation is rather limited due to the

fact that input and output data with complex structures can be difficult to comprehend during

34 Computer Science & Information Technology (CS & IT)

animation. Without resolving this limitation, specification animation would be difficult to be

transferred to industry for realistic software developments.

In this paper, the researchers put forward a tool supported visualization of input and output data

of operations in formal specifications. The proposed visualization technique can be widely

applicable to model-based formal notations, such as VDM-SL, Z, and Event-B, SOFL has been

chosen, standing for Structured Object-Oriented Formal Language, as the formal notation in our

discussions, partly because SOFL has been used in various joint software projects with industry

and partly because SOFL offers a comprehensible way to use formal specifications in practical

software development.

Our major contributions in this paper are twofold. One is the design of a visualized representation

of each type of data provided in the SOFL language. Such a visualization aims to facilitate the

expression of the data in a graphical user interface (GUI). The other is the implementation of a

software tool supporting the visualization and animation of a single operation called process in

SOFL.

The remainder of this paper is organized as follows. Section II briefly introduce the background

and related work. Section III discusses the design of visualized representation of various data

types. Section IV briefly explain how the visualized representation can be utilized in a single

process animation. Section V presents the tool researchers have built to support the proposed

technique. Section VI gives a small case study to demonstrate its usability. Finally, in Section

VII, we conclude the paper and put forward some future research directions.

ACKGROUND

AND

ELATED

ESEARCH

In SOFL, a process performs an action, task, or operation that takes input and produces output.

Figure 1 shows a simple form of a process. The process is composed of five parts: name, input

port, output port, pre-condition and post-condition. The name of the process always puts in the

center of the box. The input port in the left part of the box receives the input data flows and the

output port in the right part of the box used to connect output date flows. The pre-condition in the

upper part of the box is a condition which the inputs are required to meet, and the post-condition

in the lower part of the box is a condition which the outputs are required to satisfy [1].

Figure 1. A simple process

Briefly, the process transforms the input data flows to the output data flows. The animation of the

process will show the procedure of how the input data flows could transform to output data flows.

But in the visualization process, input and output data flows are often composed of a number of

complex data types which is difficult for user to understand. Therefore, the effect of animation is

quite limited. Without solving this problem, the animation of a process in SOFL formal

specifications will be difficult to put into use in industry.

Computer Science & Information Technology (CS & IT) 35

ELATED

ORK

Formal specification animation attracts a few developers since it provides an effective way to

help people especially for simple users to understand the features defined by formal

specifications. It helps people to verify whether the specification is consistent with their intended

requirements. In this section, we introduce some related work on formal specification animation.

The most common idea of animation is, transforming the specification into one kind of program

language. Several animation tools are built based on the specification transformation. PiZA [5] is

an animator for Z formal specification. It translates Z specifications into Prolog to generate output

variables.

Tim Miller and Paul Strooper introduced a framework for animating model-based specification

by using testgraphs [6]. The framework provides a testgraph editor for users to edit testgraphs,

and then derive sequences for animation by traversing the testgraph. Gargantini and Riccobene

proposed an automatic driven approach to animating formal specifications in Parnas’ SCR tabular

notation [7]. An important feature of this work is the adoption of a model checker to help find

counter-examples that contain a state not satisfying the property to be established by animation.

Liu and Wang introduced an animation tool called SOFL Animator for SOFL specification

animation [8]. It provides syntactic level analysis and semantic level analysis of a specification.

When performing animation, the tool will automatically translate the SOFL specification into

Java program segments, and then use some test case to execute the program.

Li and Liu proposed a novel animation approach called Automatic Functional Scenarios-based

Animation. This approach uses data as connection among independent operations involved in a

specific behavior to “execute” specifications, and does not translate them to program. Researchers

explain how to generate necessary data for animation by modifying an automatic operation

function scenario-based test case generation method, and present a case study of applying this

animation approach to SOFL specification [9].

ESIGN

ATA

YPES

Data types are essential for specifications because they provide a notation for defining data

structures used in specifications [1]. It is crucially important to show a variety of data types with

proper kinds of visual interface to make the user understand the input and output accurately.

Different data types usually represent data with different structure, quantity, and meaning. For the

user, the operators defined on the data types are not interesting, the research team therefore decide

to ignore them and focus on the structures and values of the data of various types. Researchers

design a visual expression for each of the data types in SOFL to facilitate the user in

understanding the structure and meaning for each data type accurately and rapidly. Below the

definition of each data type will be presented and then its best manifestations will be explored.

4.1 Numeric, Character and Boolean Types

Numeric, Character and Boolean types are basic data types in SOFL. Numeric types contain nat0,

nat, int and real representing natural numbers including zero, natural numbers without zero,

integers and real numbers, respectively. The character type is the atomic unit for constructing

identifiers, operators and delimiters for separating different parts in a specification and contains

all characters of the SOFL character set. The boolean type contains only two values: true and

false.

剩余15页未读，继续阅读

评论收藏

内容反馈

AE86Jag

粉丝: 43
资源: 18

SOFL形式化规范中流程输入输出自动可视化的设计与实现

基于SOFL规范的语义分析

crm-sofl

软件工程,PPT教学课件

基于分层Petri网的面向服务需求求精 (2006年)

《软件工程》教学课件

YOLOV5口罩检测数据集+代码+模型 2000张标注好的数据+教学视频.zip

第十五届蓝桥杯大赛软件赛省赛-PythonB组题目

（免费）Chrome浏览器插件axure-chrome-extension

axure谷歌浏览器插件

免费插件-AI插件-illustrator插件集合-尺寸标注-智能填充-颜色自动处理-自动批处理-Windows安装包.zip

第十五届蓝桥杯大赛软件赛省赛-PythonA组题目

火狐Firefox浏览器的插件Video DownloadHelper 8.0 的合作应用VdhCoAppSetup2.0.19

最新版YS9082HC主控开卡工具 YS9082HC-MPToolV8.00.00.18.826-HCS1A25E2023062

安卓期末大作业（AndroidStudio开发），垃圾分类助手app，分为前台后台，代码有注释，均能正常运行

恩山新版中兴Telnet工具体验版-20230830.rar

SwitchHosts

第十五届蓝桥杯大赛软件赛省赛-C/C++ 研究生组

第十五届蓝桥杯大赛软件赛省赛-C++A组题目

Microsoft Equation Editor 3.0公式编辑器 安装包

Linux Centos7 升级最新版OpenSSH-9.6p1 有脚本（支持离线）

DirectX修复工具V4.3加强版（升级一键自动）

第十五届蓝桥杯大赛软件赛省赛C++B组题目

AI漫画推文神器豹剪：豹剪安装包

Java第十五届蓝桥杯大赛软件JavaB组真题

社交平台上经济类话题的文章热度信息，数据是真实的，但不是真实日期

Unet眼底血管图像分割数据集+代码+模型+系统界面+教学视频.zip

微信小程序源码大全（130个）

火狐Firefox浏览器的插件Video DownloadHelper 8.0 的合作应用VdhCoAppSetup2.0.11

Origin绘制相关性热图插件(Correlation Plot)

最新资源

Microsoft Equation Editor 3.0公式编辑器安装包