为何满足于 FRET 而不重构？重调 FRETISH 需求
软件工程
2022-02-14 v1
摘要
软件系统的形式化验证依赖于将其应遵循的需求形式化，这可能具有挑战性。在从自然语言形式化需求时，我们存在导致许多需求间信息重复的依赖关系，这意味着对一个需求的更改会在多处引发更新。我们提议将代码重构技术适配于 NASA 的形式化需求获取工具（FRET），即我们的首选工具。重构是在不改变软件外部行为的前提下重新组织软件以改善其内部结构的过程；它也可应用于需求，通过减少重复使其更易于管理。FRET 自动将需求（以其输入语言 Fretish 编写）翻译为时序逻辑，这使我们能够形式化验证重构保留了需求的底层含义。在本文中，我们提出四种针对 Fretish 需求的重构并解释其效用。我们描述了其中一种重构在民用飞机发动机软件控制器需求上的应用，以将依赖关系从重复中解耦，并分析了这如何改变需求数量与重复次数。我们使用 Spot（一种用于检查时序逻辑规范等价性的工具）评估了我们的方法。
引用
@article{arxiv.2202.05816,
title = {Why just FRET when you can Refactor? Retuning FRETISH Requirements},
author = {Matt Luckcuck and Marie Farrell and Oisín Sheridan},
journal= {arXiv preprint arXiv:2202.05816},
year = {2022}
}