最终项目“代码生成”在VerfiySpecApp-BSC中

申请规格的正式验证 每个程序的开发都从其规范开始。 在开始实施之前，必须确认规范的正确性。 蜂窝应用的规格显示出非常特殊的特征：从一个屏幕转移到另一个屏幕。 我们使用规格的特殊性来验证其正确性。 我们完成了什么？ 我们构建了一个工具，可以用图形方式定义蜂窝应用程序的规范，这意味着：将规范表示为图形：节点是与相应参数值关联的屏幕，边缘是促使过渡的事件。 我们的工具会获取用户想要检查的需求列表。 然后，它使用形式验证的机制来验证规格。 验证将导致确认消息或测试失败的路径。 为什么不平凡？ 这是尝试提出一种尚未编写相应代码时检查规格的方法的首次尝试。 突破; 没有人考虑过确认蜂窝应用规范正确性 我们做出的决定都不是微不足道的。 我们构建的程序图包括用户定义的所有条件，并且对于每个条件都有一组参数，我们必须检查行为的正确性。 该项目有哪些困难？ 我们的工具可以显示许多屏幕，我们支持用户可