본문 바로가기
  • Home

Requirements Specification and Static Code Verification of Simulation Models based on Discrete Event System Formalism

  • Journal of Software Forensics
  • Abbr : JSF
  • 2025, 21(2), pp.113~122
  • DOI : 10.29056/jsav.2025.06.12
  • Publisher : Korea Software Assessment and Valuation Society
  • Research Area : Engineering > Computer Science
  • Received : June 3, 2025
  • Accepted : June 20, 2025
  • Published : June 30, 2025

Changbeom Choi ORD ID 1 Seungho Yang ORD ID 1 Sooyoung Jang ORD ID 1

1국립한밭대학교

Accredited

ABSTRACT

This paper proposes a requirements specification and a static code verification based on the LLVM/Clang framework for simulation models based on the Discrete Event System (DES) formalism. In the modeling and simulation of complex systems, precise interaction between the model code and the simulation engine's API is essential for the early detection and resolution of code errors. This research defines requirement specifications like MUST-CALL, NEVER-CALL, and MUST-FOLLOW to support developers in strictly adhering to simulation model development guidelines. The proposed tool utilizes LLVM/Clang’s static analysis to parse C++ code and systematically check for violations of the defined requirement specifications before execution. A key contribution of this research is performing static code verification that reflects the specific characteristics of modeling based on the DES formalism. This approach aims to reduce runtime errors and improve model maintainability, ultimately contributing to the development of efficient and reliable models.

Journal Copyright Policy

No CCL information provided

Citation status

* References for papers published after 2025 are currently being built.

This paper was written with support from the National Research Foundation of Korea.