Construction of VDM++ Specifications from Extended Screen Transition Diagrams for Validation of Microservice-based Web Applications

Construction of VDM++ Specifications from Extended Screen Transition Diagrams for Validation of Microservice-based Web Applications

연구 분야: Software Development

학회: 2024 IEEE 29th Pacific Rim International Symposium on Dependable Computing (PRDC)

This paper shows a technique to construct VDM++ specifications from ESTDs (Extended Screen Transition Diagrams) for validation of Web applications that are based on MVC model and microservices architectures. The notation of ESTDs is further extended so as to support microservices architectures, and then a basic structure of VDM++ specifications is discussed by using a simplified example. The behavior of microservices is described in VDM++, which will be useful to find services in which errors occur and their root causes.