一种基于契约的刺激-响应需求规约方法
软件工程
2017-04-18 v1
摘要
现有许多形式化方法以声明式形式捕获刺激-响应需求。但仍需将所得声明式语句翻译为命令式程序。本文描述了一种以带条件与断言的命令式程序例程形式来规约与验证刺激-响应需求的方法。随后程序证明器直接依据所述需求检查候选程序。文章通过将该方法应用于起落架系统（Landing Gear System）的 ASM 模型来说明该途径，该模型是用于评估规约与验证技术的广泛使用的现实示例。
引用
@article{arxiv.1704.04905,
title = {A contract-based method to specify stimulus-response requirements},
author = {Alexandr Naumchev and Manuel Mazzara and Bertrand Meyer and Jean-Michel Bruel and Florian Galinier and Sophie Ebersold},
journal= {arXiv preprint arXiv:1704.04905},
year = {2017}
}