Description style of model-based formal specification considering executability and readability

Yasumasa Nakatsugawa, Taro Kurita, Keijiro Araki

Research output: Contribution to journalArticle

Abstract

In this paper, we propose description style of model-based formal specification considering an executability for verification and a readability. We use model-based formal specification language VDM++. In a software development, a role of specification and that of design are often distinguished. If this boundary is ambiguous, designers can not understand a scope of specification and design. In an executable specification, there are mechanisms of execution and description of specifications. If this boundary is ambiguous, it is hard to understand a specification. First, we focus on the internal data structure as a boundary between specification and design. We propose techniques of hiding types that are outside the scope of specification. We compare the differences in a readability by use of hiding techniques. Next, in a executable specification, we examine a readability and an executability from the description style provided by the language specification of VDM++. Finally, we present the part of experimental results of ongoing project.

Original languageEnglish
Pages (from-to)130-135
Number of pages6
JournalComputer Software
Volume27
Issue number2
Publication statusPublished - May 2010

Fingerprint

Specifications
Specification languages
Formal specification
Data structures
Software engineering

All Science Journal Classification (ASJC) codes

  • Software

Cite this

Description style of model-based formal specification considering executability and readability. / Nakatsugawa, Yasumasa; Kurita, Taro; Araki, Keijiro.

In: Computer Software, Vol. 27, No. 2, 05.2010, p. 130-135.

Research output: Contribution to journalArticle

Nakatsugawa, Y, Kurita, T & Araki, K 2010, 'Description style of model-based formal specification considering executability and readability', Computer Software, vol. 27, no. 2, pp. 130-135.
Nakatsugawa, Yasumasa ; Kurita, Taro ; Araki, Keijiro. / Description style of model-based formal specification considering executability and readability. In: Computer Software. 2010 ; Vol. 27, No. 2. pp. 130-135.
@article{1be8124cabde4413bba4aa2cda4f3cc6,
title = "Description style of model-based formal specification considering executability and readability",
abstract = "In this paper, we propose description style of model-based formal specification considering an executability for verification and a readability. We use model-based formal specification language VDM++. In a software development, a role of specification and that of design are often distinguished. If this boundary is ambiguous, designers can not understand a scope of specification and design. In an executable specification, there are mechanisms of execution and description of specifications. If this boundary is ambiguous, it is hard to understand a specification. First, we focus on the internal data structure as a boundary between specification and design. We propose techniques of hiding types that are outside the scope of specification. We compare the differences in a readability by use of hiding techniques. Next, in a executable specification, we examine a readability and an executability from the description style provided by the language specification of VDM++. Finally, we present the part of experimental results of ongoing project.",
author = "Yasumasa Nakatsugawa and Taro Kurita and Keijiro Araki",
year = "2010",
month = "5",
language = "English",
volume = "27",
pages = "130--135",
journal = "Computer Software",
issn = "0289-6540",
publisher = "Japan Society for Software Science and Technology",
number = "2",

}

TY - JOUR

T1 - Description style of model-based formal specification considering executability and readability

AU - Nakatsugawa, Yasumasa

AU - Kurita, Taro

AU - Araki, Keijiro

PY - 2010/5

Y1 - 2010/5

N2 - In this paper, we propose description style of model-based formal specification considering an executability for verification and a readability. We use model-based formal specification language VDM++. In a software development, a role of specification and that of design are often distinguished. If this boundary is ambiguous, designers can not understand a scope of specification and design. In an executable specification, there are mechanisms of execution and description of specifications. If this boundary is ambiguous, it is hard to understand a specification. First, we focus on the internal data structure as a boundary between specification and design. We propose techniques of hiding types that are outside the scope of specification. We compare the differences in a readability by use of hiding techniques. Next, in a executable specification, we examine a readability and an executability from the description style provided by the language specification of VDM++. Finally, we present the part of experimental results of ongoing project.

AB - In this paper, we propose description style of model-based formal specification considering an executability for verification and a readability. We use model-based formal specification language VDM++. In a software development, a role of specification and that of design are often distinguished. If this boundary is ambiguous, designers can not understand a scope of specification and design. In an executable specification, there are mechanisms of execution and description of specifications. If this boundary is ambiguous, it is hard to understand a specification. First, we focus on the internal data structure as a boundary between specification and design. We propose techniques of hiding types that are outside the scope of specification. We compare the differences in a readability by use of hiding techniques. Next, in a executable specification, we examine a readability and an executability from the description style provided by the language specification of VDM++. Finally, we present the part of experimental results of ongoing project.

UR - http://www.scopus.com/inward/record.url?scp=77956425988&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=77956425988&partnerID=8YFLogxK

M3 - Article

VL - 27

SP - 130

EP - 135

JO - Computer Software

JF - Computer Software

SN - 0289-6540

IS - 2

ER -