论文标题
用TLA+指定和模型检查单页应用程序的工作流程
Specifying and Model Checking Workflows of Single Page Applications with TLA+
论文作者
论文摘要
单页应用程序（SPA）与基于超文本的Web应用程序不同，因为它们的工作流程不是由显式链接来定义的，而是通过其小部件状态的更改隐含的。因此，工作流程可能很难跟踪。我们提出了一种用TLA+指定和模型检查SPA的方法。我们的方法使记录和跟踪水疗中心的工作流程并找到潜在的设计缺陷变得更加容易。
Single Page Applications (SPAs) are different than hypertext-based web applications in that their workflow is not defined by explicit links, but rather implicitly by changes of their widgets' states. The workflow may hence be hard to track. We present an approach to specifying and model checking SPAs with TLA+. Our approach makes it easier to document and to track the workflow of SPAs and to find potential design flaws.
