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/1
Y1 - 2010/5/1
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
AN - SCOPUS:77956425988
VL - 27
SP - 130
EP - 135
JO - Computer Software
JF - Computer Software
SN - 0289-6540
IS - 2
ER -