Integrating formal specifications in the development and testing of UIs by formal model–view–controller pattern

Ensuring software functionality, maintainability, and modularity is vital while developing UIs. For this reason, architectural patterns, like the Model–View–Controller (MVC), are usually employed. The MVC aims to separate the representation of information (model) from its presentation to the user (view). One can use a formal model to study the system and the UI, but such formal models are separately developed and analyzed, and the results of the analysis cannot be assured for the actual implementation. To address this problem, we introduced the formal MVC pattern (fMVC), allowing the integration of Asmeta specifications into the model of the MVC-designed software. This paper extends the fMVC pattern and the framework to better support Java Swing components and enhance error management, including automatic model state rollback on input failure. Moreover, we propose an extension enabling testers to generate and reuse Avalla scenarios for UI validation. We demonstrate the framework’s application, covering modeling, validation, and verification at the model level for the AMAN case study that inspired us during the definition of the fMVC pattern. Moreover, we show how the AMAN UI can be implemented and tested by our approach.