GeneSyst：一个推理B事件规范行为方面的工具。适用于安全属性。
GeneSyst: a Tool to Reason about Behavioral Aspects of B Event Specifications. Application to Security Properties.
摘要：
在本文中，我们提出了一种方法和工具，以建立符号标记的B规格转换系统。这个名为GeneSyst的工具可以考虑细化级别，并可以可视化抽象状态在具体层次状态中的分解。由此产生的符号转换系统代表了初始B事件系统的所有行为。因此，它可以用来推理它们。我们说明了使用GeneSyst检查电子钱包模型的安全属性。
英文摘要：
In this paper, we present a method and a tool to build symbolic labelled transition systems from B specifications. The tool, called GeneSyst, can take into account refinement levels and can visualize the decomposition of abstract states in concrete hierarchical states. The resulting symbolic transition system represents all the behaviors of the initial B event system. So, it can be used to reason about them. We illustrate the use of GeneSyst to check security properties on a model of electronic purse.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
