- 【Updated on May 12, 2025】 Integration of CiNii Dissertations and CiNii Books into CiNii Research
- Trial version of CiNii Research Knowledge Graph Search feature is available on CiNii Labs
- 【Updated on June 30, 2025】Suspension and deletion of data provided by Nikkei BP
- Regarding the recording of “Research Data” and “Evidence Data”
A Method and Tool Support for Generating SOFL Formal Specifications from Programs
Bibliographic Information
- Other Title
-
- ソースコードからSOFL形式仕様への生成手法と支援ツールの提案
Search this article
Description
Software systems developed in practice often lack an appropriate specification defining their functionality. This is also true in legacy software systems and many realistic software projects. Moreover, software review detects bugs, but the result of review depends on the reviewer. To deal with this problem, we put forward an approach to automatically generating formal specifications from source code as a step of reverse engineering. This includes transformations at two levels. One is to transform source code into Condition Data Flow Diagrams (CDFD) used in the Structured Object-Oriented Formal Language (SOFL) specification language, which includes mainly dealing with sequence, selection, and repetition. The other is to support the formation of formal specifications for operations involved in the CDFD and SOFL specification. SOFL is a formal engineering method. It provides a formal language which integrates structured method and object oriented language. By providing a tool support for generating SOFL specifications, we could provide a useful support for the construction of specifications in SOFL and help detect bugs in the source code. The tool can also help visualize the relations between operations for confirmation.
Journal
-
- 法政大学大学院紀要. 情報科学研究科編
-
法政大学大学院紀要. 情報科学研究科編 14 1-6, 2019-03-31
法政大学大学院情報科学研究科
- Tweet
Details 詳細情報について
-
- CRID
- 1390009224824865536
-
- NII Article ID
- 120006714908
-
- NII Book ID
- AA12746425
-
- HANDLE
- 10114/00021932
-
- ISSN
- 24321192
-
- Text Lang
- ja
-
- Article Type
- departmental bulletin paper
-
- Data Source
-
- JaLC
- IRDB
- CiNii Articles
-
- Abstract License Flag
- Allowed