The GROOVE Simulator: A Tool for State Space Generation
The GROOVE Simulator: A Tool for State Space Generation
复制标题
GROOVE 模拟器：状态空间生成工具
DOI：
--
复制
发表时间：
2003
期刊：
影响因子：
--
通讯作者：
A. Rensink
中科院分区：
文献类型：
--
作者：
A. Rensink
这里描述的工具是称为Groove(基于图形的面向对象验证)的工具集的第一部分，用于面向对象系统的软件模型检查。Groove与其他模型检测方法的不同之处在于，它是基于图形转换的。它使用图形来表示状态快照；转换产生于图形生成规则的应用。这就产生了所谓的图转换系统(GTSRSquo)作为计算模型。
The tool described here is the first part of a tool set called GROOVE (GRaph-based Object-Oriented VErification) for software model checking of object-oriented systems. The special feature of GROOVE, which sets it apart from other model checking approaches, is that it is based on graph transformations. It uses graphs to represent state snapshots; transitions arise from the application of graph production rules. This yields so-called Graph Transition Systems (GTSrsquos) as computational models.