一种利用NuSMV验证具有无界多个客户端的服务之方案
计算机科学中的逻辑
2018-12-04 v1
摘要
我们研究客户端-服务器系统的模型检测，其中服务器提供若干类型的服务，这些服务在任何时刻可能依赖于当时活跃的特定类型客户端的数量。由于存在无界多个客户端，此类系统的状态空间是无限的，使得规约与验证十分困难。该问题可通过使用一种具有单子一阶(MFO)句子并辅以标准时序模态词封闭的规约语言来规避。MFO句子给出一个界，该界反过来可用于界定输入客户端-服务器系统的状态空间，从而使验证问题可判定。该方案使用NuSMV工具实现。
引用
@article{arxiv.1812.00183,
title = {A Scheme to Verify Services with Unboundedly many Clients using NuSMV},
author = {S Sheerazuddin and S Anand and R S Anish Badhri},
journal= {arXiv preprint arXiv:1812.00183},
year = {2018}
}