Verified Software in Web-Based Virtual Environments
摘要
In verified software development, we use formal methods to verify the software correctness with respect to its formally specified properties. However, there are no formal means to verify the properties themselves against informal requirements. Instead, validation via animation of formal specifications is used. To improve the validation, an animatable formal specification or an executable prototype derived from it can be embedded into a 3D virtual environment, resembling the one where the system will be used. Utilization of virtual environments instead of real ones contributes to the environmental and economic sustainability by saving resources. This paper presents a hypothetical case study that demonstrates how an executable prototype can be developed using the B-Method formal method and subsequently embedded into a collaborative virtual environment for validation purposes. The prototype developed is a control program of a fictional cleaning robot. Its critical property is to avoid harming people and other living beings by its operation. The virtual environment is created using A-Frame, a software framework for web-based virtual reality.