An Improved Conversion Technique from EPNAT Models to VDM++ Specifications for Simulation of Abstract Software Behavior
Sho Matsumoto, Ryoichi Ishigami, Tetsuro Katayama, Tomohiko Takagi · Proceedings of International Conference on Artificial Life and Robotics · 2024
Formal software models based on EPNAT (Extended Place/transition Net with Attributed Tokens) can be converted to VDM++ specifications that enable simulation of abstract software behavior before implementation processes.However, the conversion technique has two problems, that is, (1) extracting all properties to be checked from the VDM++ specifications requires time and effort, and (2) the structure of the VDM++ specifications has less readability and maintainability.In this study, we improve the conversion technique by (1) adding features to extract an abstract current state of software, and (2) dividing into classes that correspond to subnets of EPNAT models.This paper shows a new conversion rule, a new structure of VDM++ specifications, a simple example, and the discussion about their effectiveness.