Declarative GUIs: Simple, Consistent, and Verified
Declarative GUIs: Simple, Consistent, and Verified
复制标题
声明式 GUI：简单、一致且经过验证
DOI：
--
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Eric Walkingshaw
中科院分区：
文献类型：
--
作者：
Stephan Adelsberger;A. Setzer;Eric Walkingshaw
图形用户界面（GUI）在现实世界的软件中无处不在，并且是难以通过软件测试捕获的错误的臭名昭着来源。模型检查已经被用来证明某些类型的错误的存在，但模型检查工作在GUI应用程序的抽象模型上，这可能与其实现不一致。我们提出了一个库开发直接验证，状态依赖的GUI应用程序的依赖类型的编程语言Agda。在库中，GUI控制器的类型取决于GUI本身的规范，静态地强制它们之间的一致性。可以根据用户交互和状态转换定义和证明任意属性。我们的库连接到一个定制的Haskell后端，用于声明性的基于向量的GUI元素。与构建在现有命令式GUI框架上的早期版本的库相比，更具声明性的后端支持更简单的定义和证明。作为我们的图书馆的安全关键域的实际应用，我们提出了一个案例研究与维也纳医科大学合作开发。该案例研究实现了一个用于处方抗凝剂的医疗保健过程，手动遵循该过程时极易出错。我们的实现从数据感知业务流程的抽象描述中生成GUI，使我们的方法易于重用和适应其他安全关键流程。我们证明了可执行GUI应用程序的医学相关安全属性，例如给定某些输入，必须或不能达到某些状态。
Graphical user interfaces (GUIs) are ubiquitous in real-world software and a notorious source of bugs that are difficult to catch through software testing. Model checking has been used to prove the absence of certain kinds of bugs, but model checking works on an abstract model of the GUI application, which might be inconsistent with its implementation. We present a library for developing directly verified, state-dependent GUI applications in the dependently typed programming language Agda. In the library, the type of a GUI's controller depends on a specification of the GUI itself, statically enforcing consistency between them. Arbitrary properties can be defined and proved in terms of user interactions and state transitions. Our library connects to a custom-built Haskell back-end for declarative vector-based GUI elements. Compared to an earlier version of our library built on an existing imperative GUI framework, the more declarative back-end supports simpler definitions and proofs. As a practical application of our library to a safety-critical domain, we present a case study developed in cooperation with the Medical University of Vienna. The case study implements a healthcare process for prescribing anticoagulants, which is highly error-prone when followed manually. Our implementation generates GUIs from an abstract description of a data-aware business process, making our approach easy to reuse and adapt to other safety-critical processes. We prove medically relevant safety properties about the executable GUI application, such as that given certain inputs, certain states must or must not be reached.
影响因子：
3.3
作者：
J. Whittle;J. Hutchinson;M. Rouncefield
通讯作者：
J. Whittle;J. Hutchinson;M. Rouncefield
基于特征的工作流组合的形式化验证
DOI：
10.1109/edcc.2018.00039
发表时间：
2018
期刊：
--
影响因子：
--
作者：
Adelsberger S
通讯作者：
Adelsberger S
CoSMeDis：具有正式验证的保密保证的分布式社交媒体平台
DOI：
10.1109/sp.2017.24
发表时间：
2017
期刊：
--
影响因子：
--
作者：
Bauereiss T
通讯作者：
Bauereiss T