Verifying hardware components with JACK

被引：0

作者：

DeNicola, R

Fantechi, A

Gnesi, S

Larosa, S

Ristori, G

机构：

[1] UNIV PISA, DIP INGN INFORMAZ, PISA, ITALY

[2] CNR, IST ELABORAZ INFORMAZ, I-56100 PISA, ITALY

[3] UNIV PISA, DIPARTIMENTO INFORMAT, PISA, ITALY

来源：

CORRECT HARDWARE DESIGN AND VERIFICATION METHODS | 1995年 / 987卷

关键词：

D O I：

暂无

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

JACK (the acronym for Just Another Concurrency Kit) is a workbench integrating a set of verification tools for concurrent system specifications, supported by a graphical interface offering facilities to use these tools separately or in combination. The environment offers several functionalities to support the design, analysis and verification of systems specified using process algebras. In this paper we use JACK to formally specify the hardware components of a buffer system. Then we verify, by using the checking capabilities of JACK, the correctness of the specification with respect to some safety requirements, expressed in the action based temporal logic ACTL.

引用

页码：246 / 260

页数：15

共 19 条

[1]

Bouali A., 1994, Bulletin of the European Association for Theoretical Computer Science, P207

[2]

BOUALI A, 1992, LNCS, V663

[3] AUTOMATIC VERIFICATION OF FINITE-STATE CONCURRENT SYSTEMS USING TEMPORAL LOGIC SPECIFICATIONS [J].

CLARKE, EM ;

EMERSON, EA ;

SISTLA, AP .

ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1986, 8 (02) :244-263

[4]

CLEAVELAND R, 1990, LECT NOTES COMPUT SC, V407, P24

[5]

DANELUTTO M, 1995, UNPUB

[6]

DEFRANCESCO N, 1994, LNCS

[7] 3 LOGICS FOR BRANCHING BISIMULATION [J].

DENICOLA, R ;

VAADRAGER, F .

JOURNAL OF THE ACM, 1995, 42 (02) :458-487

[8]

DENICOLA R, 1990, LECT NOTES COMPUT SC, V469, P407

[9] AN ACTION-BASED FRAMEWORK FOR VERIFYING LOGICAL AND BEHAVIORAL PROPERTIES OF CONCURRENT SYSTEMS [J].

DENICOLA, R ;

FANTECHI, A ;

GNESI, S ;

RISTORI, G .

COMPUTER NETWORKS AND ISDN SYSTEMS, 1993, 25 (07) :761-778

[10]

DENICOLA R, 1991, 6 INT WORKSH SOFTW S, P54

← 1 2 →