Implementing a modal logic over data and processes using XTL

被引：0

作者：

Bryans, J ^{[1
]}

Shankland, C ^{[1
]}

机构：

[1] Univ Stirling, Dept Comp Sci & Math, Stirling FK9 4LA, Scotland

来源：

FORMAL TECHNIQUES FOR NETWORKED AND DISTRIBUTED SYSTEMS | 2001年 / 69卷

关键词：

modal logic; symbolic LOTOS; CADP; XTL;

D O I：

暂无

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

The modal logic FULL is designed to capture strong bisimulation over early symbolic transition systems (STSs) for full LOTOS. It provides a compact way of expressing and verifying properties involving both data and transitions. In this paper we present a restricted prototype implementation of a model checker for LOTOS for queries written using the FULL logic. The model checker is developed within the CADP package using XTL.

引用

页码：201 / 216

页数：16

共 27 条

[1]

AJUBI I, 1989, FORMAL DESCRIPTION T, P89

[2]

AMYOT D, 2000, FEATURE INTERACTIONS, V6

[3]

[Anonymous], MODEL CHECKING

[4]

BROY M, 1996, LECT NOTES COMPUTER, V1169

[5]

BRYANS J, 2001, UNPUB REPORT DEV SYM

[6]

BRYANS J, 2001, AVOCS 01 WORKSH AUT

[7] SYMBOLIC MODEL CHECKING FOR SEQUENTIAL-CIRCUIT VERIFICATION [J].

BURCH, JR ;

CLARKE, EM ;

LONG, DE ;

MCMILLAN, KL ;

DILL, DL .

IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 1994, 13 (04) :401-424

[8]

CALDER M, 2001, IN PRESS COMPUTER J

[9]

CALDER M, 2001, TR200177 U GLASG

[10]

CALDER M, 2001, LNCS, V2021, P384

← 1 2 3 →