GeneSyst：一个用于推理B事件规范行为方面的工具——在安全属性中的应用
计算机科学中的逻辑
2010-04-12 v1 密码学与安全
摘要
在本文中，我们提出了一种从B规范构建符号化标记迁移系统的方法和工具。该工具名为GeneSyst，能够考虑精化层次，并可视化抽象状态在具体层次状态中的分解。生成的符号化迁移系统代表了初始B事件系统的所有行为。因此，它可以用于对这些行为进行推理。我们通过在一个电子钱包模型上检查安全属性，展示了GeneSyst的应用。
引用
@article{arxiv.1004.1472,
title = {GeneSyst: a Tool to Reason about Behavioral Aspects of B Event Specifications. Application to Security Properties.},
author = {Didier Bert and Marie-Laure Potet and Nicolas Stouls},
journal= {arXiv preprint arXiv:1004.1472},
year = {2010}
}