信号时序逻辑（STL）规范对非正式文本要求的系统验证。
STLInspector的Python项目详细描述
信号时序逻辑（stl）规范的系统验证 反对非正式的文本要求。
目标 STLInspector是 识别在形式化过程中发生的典型故障 通过修改候选规范的需求。 STLInspector计算 一系列代表性的信号，使需求工程师能够 为了根据所有变异的变体验证候选规范， 从而实现全变异覆盖。通过目视检查 通过基于web的gui，工程师可以获得对 形式化的正确性-即使她不熟悉 史崔。STLInspector 使形式化规范的评估可被广泛使用 因此有助于利用 规范和计算机辅助验证。
安装
STLInspector取决于 关于Python 2，ANTLR v4，定理证明者 Z3使用python绑定和 python包Flask和 Flask-Assets。 另外，gui依赖于 Bootstrap， jQuery，jQuery UI， Chart.js，和 handlebars。
使用包管理器安装或下载python 2>；=2.7.9 来自http://www.python.org/downloads。这也提供了python 包装经理皮普。 STLInspector是 作为python package提供，可以是 使用PIP安装：
pip install STLInspector
注意，所需的javascript框架不是本地安装的， 但通过网络连接加载。这是有限制的 你只能在互联网上使用图形用户界面。由于 出于安全原因，禁止对gui进行网络访问，并且gui 仅通过本地主机可用。
教程
这是一个演示如何使用 STLInspector。它显示 程序的标准工作流程和示例需求。为了一个 更深入的理解考虑阅读 documentation。
通过执行stlinspector .启动服务器。
打开浏览器并转到http://localhost:5000。
按new requirements project按钮，输入标题 tutorial requirements project并按add按钮。这个 项目概述打开。
在text requirements块中，按edit按钮 输入：
The velocity should be higher than 5km/h from second 1 to second 3.
在current stl candidate块中，按edit按钮 输入：
F[1,3] velocity > 5
在visual inspection results下，将name替换为test user 然后按new visual inspection。
显示了文本需求和测试信号。评估 对测试信号的文本要求并按yes或no 按钮。执行此操作，直到不再显示测试信号。然后按 返回项目概述。
要查看评估结果，请按show results按钮。 因为在我们的例子中stl候选是错误的，一些 评估结果应与STL候选结果不同。
将stl候选更改为：
G[1,3] velocity > 5
重新对新的stl候选者进行目视检查。
不应获取stl的冲突计算结果 现在是候选人。
按“保存”按钮，项目将保存到 tutorial_requirements_project.stlinspector当前 目录。恭喜，你验证了STL候选人 文本要求！
文档
更多信息请参见 documentation 详细介绍了基于web的gui的使用、解析器和变异 操作员。gui提供了文档的html版本。
贡献
我们非常感谢为 STLInspector。全部 对这个项目的贡献应该作为请求在github上发送。 STLInspector使用 语义版本控制卧床 packaging.python.org。 在请求拉取之前，请运行测试套件python setup.py test。
许可证
欢迎加入QQ群-->： 979659372
