The SPINJA Model Checker

被引：0

作者：

de Jonge, Marc

Ruys, Theo C.

机构：

来源：

MODEL CHECKING SOFTWARE | 2010年 / 6349卷

关键词：

D O I：

暂无

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

SPINJA is a model checker for PROMELA, implemented in Java. SPINJA is designed to behave similarly to SPIN, but to be more easily extendible and reusable. Despite the fact that SPINJA uses a layered object-oriented design and is written in Java, SPINJA's performance is reasonable: benchmark experiments have shown that, in exhaustive mode, SPINJA is about five times slower than the highly optimized SPIN. For bitstate verification runs the difference is only a factor of two.

引用

页码：124 / 128

页数：5