形式化模型验证方法在UI中的应用

哈Ha！ 我向您呈现Hillel Wayne 撰写的文章“正式指定UI”的翻译。

来自作者

相对最近，我遇到了一篇有关软件开发中的工程方法的文章，其中vasil-sd谈论了有关所创建软件产品规范的形式验证。 合金用作工具箱。 注释中的主要主题之一是在某些现代Web项目的上下文中分析文章，因为它昂贵，耗时长，难以使用所有人都可以快速/廉价地进行使用的形式化方法。 自从作者提到Hillel Wayne博客（即此类示例所在）以来，我决定翻译他的一些文章，作为vasil-sd正文的补充

警告 ：

• 作者所说的一切都称为有限状态机，我将其称为状态机或状态机模型。
• 我从前面提到的有关工程开发方法的文章中学到了一些术语。 不过，对我而言，这个话题相对较新，因为两位作者（无论是国外的还是不是外国的）都不能理解-不要发誓。

正式的UI规范

良好的用户界面对于创建正确的软件至关重要。 而且，如果用户在使用该程序时遇到问题，他们可能会做错事。 我不想在用户界面上工作-我不认为自己高于此，但那不是“我的”。 视觉效果和界面引起了我的关注，能够应付所有这些问题的人引起了我的疯狂敬意。

我喜欢正式的方法。 我的朋友Kevin Lynagh最近发布了sketch.systems ¹ ，一种针对UI设计人员的新的正式规范工具。 好吧，让我们找出答案-我对形式方法的热爱可以克服我的恐惧吗？

问题

回到Edmodo，我正在为Snapshot应用程序创建用户界面。 这是我们第二次尝试赚钱的尝试：我们首先给所有老师免费的程序，然后要求捐款或类似的东西。 如您所见，Edmodo并没有太大的商业头脑。 ²

在快照中，教师可以在学生中进行“投票”或“小睡”。 此外，该程序汇总调查结果，并在以下部分中为教师提供一些实时报告：“摘要”报告，“按学生”和“按标准”。 另外，我们决定该程序应该有一个“答案”报告，可以从“学生”报告中打开该报告，并提供有关错误答案的信息。

我们设想用户可以通过按必要的按钮在报表之间移动，并且应该可以从其他报表访问所有报表（答案除外）。 在过渡情况下，“可用”一词的含义相当模糊：它可能意味着“您可以以某种方式转到报告”，或者可能意味着“单击即可直接转到所需的报告。”上述内容仅是用户的一部分整个应用程序的界面，除了报表中的导航外，还具有自己的导航系统。

当系统开始变得更加复杂时，我们需要小心。 这意味着编写规范。 那么我们如何指定呢？ 我看到老师可以在应用程序的特定屏幕上，并且可以采取措施移至另一个屏幕。 这使我想到了一个想法，我们可以将教师的行为视为有限状态机。

状态机

有限状态机（FSM）是抽象自动机理论中最简单的数学模型之一。 您具有一组有限的状态，一组状态之间的转换以及一组触发转换的事件（触发器）。 每个过渡都与事件相关，因此，如果事件发生，状态可能会更改。 ³在我们的模型中，事件将是“老师按下按钮”。以下是我们当前系统的状态机模型：


该模型显示了我们用户界面的两个问题。 首先，所有有限状态机都需要初始状态，但是我们没有初始状态。 老师访问“报告”页面时，他应该首先看到哪个报告？ 其次，当您单击已查看的报表按钮时，我们不会指出会发生什么。 这是模棱两可的，因为有几种行为：

1. 如果您在摘要报告中，则不会出现“摘要”按钮或不执行任何操作。
2. 如果您在摘要报告中，则“摘要”按钮将重置报告。

我们选择了第二个选项。 我们的初始状态是“摘要”报告。


该模型非常准确地传达了我们的用户界面-也很混乱。 这是有限状态机模型的一个显着局限性：状态之间的转换越多，感知它们的难度就越大。 在我们的案例中，几乎可以从每个报告切换到另一个报告。

该系统及其模型的进一步开发变得成问题。 因为，例如，如果考虑到教师随时可以退出系统，那么状态机的下一个模型将看起来像这样：


要添加注销功能，我们必须再添加四个边缘。 用这种方法进行的进一步规范开发很快就消失了。 我们需要某种方式来代表“一般”过渡。 为此，我们可以使用嵌套状态，这会使我们的形式主义复杂化，但可以简化规范。

Harel状态图

我们的大多数状态都具有所谓的超级状态的通用逻辑：我们的所有四个“报告”都具有用于注销系统的相同逻辑，而主要的三个具有相同的转换。 如果我们可以将它们归类为“父母身份”报告，那么剩下的工作就是确定向“退出”的过渡，并在子状态中分配此过渡。 逻辑类似于继承：子状态继承（或覆盖）父状态的转换。

具有嵌套状态的有限状态机称为分层状态机，有几种不同的方式对其进行形式化。 为UI编写状态机模型的最合适方法是Harel Statechart。 ⁴她^的规则如下：

1. 所有的父母状态都是抽象的。 每个父状态必须定义一个默认的子状态。
2. 子状态会自动继承所有父转换，但也可以覆盖它们。
3. 过渡可以指示任何状态。 如果切换到父状态，请转到其默认子状态。 如果子状态也是父状态，则递归确定该状态。

您可以在Graphviz中开发Harel状态图，并且每次在图形图的许多顶点，边缘和令人愉悦的地方都感到恐惧。 我们将使用Sketch.systems更好的用户界面：

Snapshot logout -> Login Page Reports summary -> Summary students -> Students standards -> Standards Summary* Students answer -> Answers Standards Answers close -> Students Login Page login -> Snapshot 

_来源

我建议遵循该图的链接，因为 她是互动的。 您可以单击过渡并查看状态如何变化。 这是《哈克尔状态图》的一大优势：它们不仅形式简明，而且富有动感。 您可以研究它们。

在研究图表时，我发现了一个错误：您可以直接从“答案”转到“标准”。 可以通过使“答案”成为“输入”而不是“报告”的直接后代来解决此问题：


_来源

理想情况下，很高兴在图表上清楚地看到此类问题，这暗示了模型验证的某种自动化。

检查一下

正式规范有两个优点。 其中之一是隐式的：形式化工作导致对系统的更好理解。 另一个是明确的：如果我们有正式的规范，我们可以检查其属性。 我们的用户界面是否有死锁？ 是否存在隐式或错误指定的过渡？

Sketch.systems可以检查Harel状态图的格式是否正确，但是不能检查模型的行为。 还有其他确定状态机状态的工具，特别是UML状态图，但是所有这些工具都针对代码级规范，而不是系统级规范。 他们的目标是最终从状态图生成C或Java代码。 但是它们太底层了，无法测试抽象属性，而我们也太高层了，不想生成代码。 如果要进行形式化测试，则需要使用通用规范语言描述模型。

幸运的是，对于这种情况，这很容易做到。 为此，我们将使用Alloy，因为它可以最准确地反映Harel状态图的结构。 ⁵我们可以使用签名扩展来表示嵌套状态：“标准”扩展“报告”表示每个“标准”也是“报告”，这相当于在相应的Harel图中声明这是子状态。 这简化了过渡的定义。 它们中的每一个都由一个谓词表示，该谓词花费时间（t），初始状态（开始）和最终状态（结束），并声明时间t的状态从开始到结束持续t.next。 尽管父状态是抽象的事实，我们仍然可以将它们用作开始并利用父转换。

 open util/ordering[Time] sig Time { state: one State } abstract sig State {} abstract sig Login extends State {} abstract sig Reports extends Login {} one sig Logout extends State {} one sig Students, Summary, Standards extends Reports {} one sig Answers extends Login {} pred transition[t: Time, start: State, end: State] { t.state in start t.next.state in end } pred logout[t: Time] { transition[t, Login, Logout] } pred login[t: Time] { transition[t, Logout, Summary] } pred students[t: Time] { transition[t, Reports, Students] } pred summary[t: Time] { transition[t, Reports, Summary] } pred standards[t: Time] { transition[t, Reports, Standards] } pred answers[t: Time] { transition[t, Students, Answers] } pred close_answers[t: Time] { transition[t, Answers, Students] } fact Trace { first.state = Summary all t: Time - last | logout[t] or login[t] or students[t] or summary[t] or standards[t] or answers[t] or close_answers[t] } 

现在我们可以检查模型的属性。 例如，是否可以不通过“学生”报告而获得“答案”报告？

 check {all t: Time | t.state = Answers implies t.prev.state = Students} for 7 // valid 

当有人注销并再次登录时，我们还可以模拟一个示例：

 run {some disj t1, t2: Time | logout[t1] and login[t2]} for 7 

合金提供了相当广泛的规格。 通过验证某些特性（例如图皮奥科夫），可能会遇到困难。 但是，我不是第一个了解Alloy与状态图的配合情况的人。 南希·戴（Nancy Day）教授最近宣布了一种称为DASH的Alloy变体，该变体为Harel图添加了一流的Harel图语义。 你可以在这里阅读。

价值

所有这些都有价值吗？ 什么使交互式状态图比英语注释更好？ 绝对，当您扩展时，图更有价值。 我记得在Snapshot项目中，大约有几十个嵌套在多个大型层次结构中的教师屏幕。 没有正式的规范，我们将无法测试我们的工作。 据我所记得，我们犯了一些错误：

• 我们忘记将“结束响应报告”视为一个事件，而“响应”成为死胡同
• 创建新调查需要一堆我们确实不需要的县级路线。
• 创建调查后，我们尚未确定用户界面的行为，因此我们将教师返回到调查创建屏幕，他认为在错误期间未创建调查并重新创建了调查。
• 很难进入多个屏幕，因此没有人去看过它们。

我认为拥有正式的规范会有所帮助。 编写我上面所做的示例需要大约五分钟的时间，而整个应用程序的规范将花费不到两个小时的时间。 如果即使在设计阶段，这也帮助我们找到了所列错误中的至少一个，我们将在以后节省很多时间。

结论

我们讨论了用户与UI交互的正式规范。 我对形式方法的热爱可以克服对UI的恐惧吗？ 天哪 如果单击了Sketch.systems的链接，则可能会看到可以将Javascript原型附加到状态图。 这太神奇了！

尽管有我的恐惧，我认为正式方法还是有潜力的。 人们通常认为它们是NASA专门使用的纯学术内容。 该博客的主题是形式方法是日常工作的强大工具。 我主要考虑它们在后端和并行系统中的应用，因为我喜欢它。 但是它们的使用不仅限于我的偏好。 形式化方法对于用户界面尤为重要。 我认为到目前为止，Harel的状态图并不是最好的表示法，但这是一个很好的第一步。

顺便说一下，我建议您使用正式方法 。 告诉你的老板！

---

1. 警告，我是Alpha测试批准人之一。 我的大部分反馈像是“您应该使其更加复杂！”。 是的，我是一般的Alpha测试人员。 ^[返回]
2. 2017年，他们赚了100万，亏损了2000万。 ^[返回]
3. 有限状态机与确定性有限状态机有很多共同点，确定性有限状态机是计算机科学的重要组成部分。 应用领域的主要区别：确定性有限状态机的使用通过“它可以识别的一组常规语言”来证明，有限状态机的使用通过“规范一致性”来证明^[返回]
4. 主要竞争对手是UML状态图，它基本上代表了Harer状态图，并补充了其代码规范。 它更具表现力，但难以分析。 ^[返回]
5. 如果您不熟悉Alloy，我在这里和这里都写了几篇文章。