Specifying and verifying a railroad crossing with cafeOBJ
Specifying and verifying a railroad crossing with cafeOBJ
复制标题
使用 CafeOBJ 指定和验证铁路道口
DOI：
10.1109/ipdps.2001.925137
复制
发表时间：
2001
期刊：
影响因子：
--
通讯作者：
K. Futatsugi
中科院分区：
文献类型：
--
作者：
K. Ogata;K. Futatsugi
CafeOBJ 是一种基于多种逻辑基础的广谱规范语言。 CafeOBJ 可用于指定系统的动态和静态方面，包括面向对象和反应式系统，并在 CafeOBJ 系统的帮助下验证其属性。在本文中，我们展示了 CafeOBJ 也可以用于描述实时系统并验证其属性。具体来说，我们通过引入所谓的时钟变量来演化UNITY计算模型，以便对实时系统进行建模，在CafeOBJ中描述铁路道口系统的规范，并借助CafeOBJ系统验证该系统具有基于该规范的安全属性。
CafeOBJ is a wide spectrum specification language based on multiple logical foundations. CafeOBJ can be used to specify dynamic as well as static aspects of systems including object-oriented and reactive systems and verify their properties with the help of the CafeOBJ system. In this paper, we show that CafeOBJ can be also used to describe real-time systems and verify their properties. Concretely, we evolve UNITY computational models by introducing so-called clock variables so as to model real-time systems, describe a specification of a railroad crossing system in CafeOBJ and verify that the system has a safety property based on the specification with the help of the CafeOBJ system.