BmotionWeb: A tool for rapid creation of formal prototypes

Abstract

The application of formal methods to the development of reliable interactive systems usually involves a multidisciplinary team with different roles and expertises (e.g. formal engineers, user interface designers and domain experts). While formal engineers provide the necessary expertise in formal methods, other roles may not be well versed in formal methods, such as user interface engineers or domain experts; consequently barriers may arise while working in a multidisciplinary team. For instance, communication problems and challenges in the rigorous use of formal method tools. Tools like BMotion Studio may reduce these barriers by creating visualizations of formal specifications, however, lacks features needed for the analysis of interactive systems. In this paper, we present a novel graphical environment that continues the ideas of BMotion Studio called BMotionWeb to provide support for the rapid creation of formal prototypes. A formal prototype links a mockup of a graphical user interface or device to an animated formal specification with the aim of providing lightweight formal validation of interactive systems. In order to demonstrate the application of BMotionWeb, we provide two case studies: a formal prototype of a simple phonebook software and a cruise control device.