Scholarlink

<p>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 <i>formal</i> MVC pattern (<i>f</i>MVC), allowing the integration of <Emphasis FontCategory="NonProportional">Asmeta</Emphasis> specifications into the model of the MVC-designed software. This paper extends the <i>f</i>MVC 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 <Emphasis FontCategory="NonProportional">Avalla</Emphasis> 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 <i>f</i>MVC pattern. Moreover, we show how the AMAN UI can be implemented and tested by our approach.</p>

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

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

  • 期刊论文

  • 出版模式：

    开放获取

  • 发表日期：

    2025年5月12日

查看全文
  • Andrea Bombarda,
  • Silvia Bonfanti,
  • Angelo Gargantini

摘要

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.