Dependable Software Engineering. Theories, Tools, and Applications - 4th International Symposium, SETTA 2018, Beijing, China, September 4-6, 2018, Proceedings

Dependable Software Engineering. Theories, Tools, and Applications - 4th International Symposium, SETTA 2018, Beijing, China, September 4-6, 2018, Proceedings
复制标题

可靠的软件工程。

DOI：
10.1007/978-3-319-99933-3_6
复制
发表时间：
2018
期刊：
--
影响因子：
--
通讯作者：
Adelsberger S
Adelsberger S
中科院分区：
--
文献类型：
--
作者：
Adelsberger S

文献摘要

相似文献

虽然在验证软件方面取得了重大成就，但相对于图形用户界面（GUI）应用程序的普遍性和社会重要性，验证GUI应用程序的工作还不发达。在本文中，我们提出了一个库的开发验证，状态依赖的GUI应用程序的依赖类型的编程语言Agda。该库使用Agda的表达类型系统来确保GUI、其控制器和底层模型都是一致的，从而显著减少了GUI相关错误的范围。我们提供了一种方法来指定和证明GUI应用程序的用户交互和状态转换的正确性属性。关键是，GUI应用程序和正确性属性不限于有限状态机，并且可能涉及任意交互式程序的执行。此外，该库连接到一个标准的、命令式GUI框架，从而支持开发具有预期功能（如并发）的本机GUI应用程序。我们目前的应用程序，我们的图书馆建立GUI应用程序来管理医疗保健流程。我们考虑的正确性属性如下：（1）一个状态只能通过经过一个特定的中间状态才能达到，例如，一个特定的治疗只能在进行X射线之后才能达到。(2)一个人最终达到一个特定的状态，例如，一个人最终决定治疗。这些属性的规范是根据GUI应用程序模拟器定义的，该模拟器模拟用户执行的所有可能的交互序列。
Although there have been major achievements in verified software, work on verifying graphical user interfaces (GUI) applications is underdeveloped relative to their ubiquity and societal importance. In this paper, we present a library for the development of verified, state-dependent GUI applications in the dependently typed programming language Agda. The library uses Agda’s expressive type system to ensure that the GUI, its controller, and the underlying model are all consistent, significantly reducing the scope for GUI-related bugs. We provide a way to specify and prove correctness properties of GUI applications in terms of user interactions and state transitions. Critically, GUI applications and correctness properties are not restricted to finite state machines and may involve the execution of arbitrary interactive programs. Additionally, the library connects to a standard, imperative GUI framework, enabling the development of native GUI applications with expected features, such as concurrency. We present applications of our library to building GUI applications to manage healthcare processes. The correctness properties we consider are the following: (1) That a state can only be reached by passing through a particular intermediate state, for example, that a particular treatment can only be reached after having conducted an X-Ray. (2) That one eventually reaches a particular state, for example, that one eventually decides on a treatment. The specification of such properties is defined in terms of a GUI application simulator, which simulates all possible sequences of interactions carried out by the user.