Type Checking Circus Specifications

被引：0

作者：

Xavier, Manuela ^{[1
]}

Cavalcanti, Ana ^{[2
]}

Sampaio, Augusto ^{[1
]}

机构：

[1] Univ Fed Pernambuco, Ctr Informat, Recife, PE, Brazil

[2] Univ York, Dept Comp Sci, York, N Yorkshire, England

来源：

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE | 2008年 / 195卷 / 0C期

基金：

英国工程与自然科学研究理事会;

关键词：

Formal methods; concurrency; formal languages; type system; refinement tool;

D O I：

10.1016/j.entcs.2007.08.027

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

Circus is a formal language that combines Z, CSP and additional constructors of Morgan's refinement calculus. It is aimed at the development by refinement of state-rich reactive systems. In this work, we define the Circus type system and describe the design and implementation of a type checker. We developed the type checker based directly on the typing rules that formalise the type system of Circus. We believe that this contributed to the robust construction of the type checker. We also discuss the validation strategy of the type checker, including integrations with other Circus tools.

引用

页码：75 / 93

页数：19

共 50 条

[21] Equivalence checking of two statechart specifications
Park, MH
Bang, KS
Choi, JY
Kang, I
11TH IEEE INTERNATIONAL WORKSHOP ON RAPID SYSTEM PROTOTYPING, PROCEEDINGS, 2000, : 46 - 51
[22] Checking MSC specifications for timing inconsistency
Xuandong Li
Wenkai Tan
Guoliang Zheng
Journal of Computer Science and Technology, 2002, 17 : 47 - 55
[23] CONSISTENCY CHECKING OF AUTOMATA FUNCTIONAL SPECIFICATIONS
CHEBOTAREV, AN
MOROKHOVETS, MK
LOGIC PROGRAMMING AND AUTOMATED REASONING, 1993, 698 : 76 - 85
[24] CONTRACT CHECKING USING Z SPECIFICATIONS
Negreanu, Lorina
Mocanu, Irina
ANNALS OF DAAAM FOR 2009 & PROCEEDINGS OF THE 20TH INTERNATIONAL DAAAM SYMPOSIUM, 2009, 20 : 301 - 302
[25] CHET: A system for checking dynamic specifications
Reiss, SP
19TH INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING, PROCEEDINGS, 2004, : 302 - 305
[26] Checking JML specifications with B machines
Bouquet, F
Dadeau, F
Groslambert, J
ZB 2005: FORMAL SPECIFICATION AND DEVELOPMENT IN Z AND B, PROCEEDINGS, 2005, 3455 : 434 - 453
[27] Equivalence checking of circuits with parameterized specifications
Goldberg, E
THEORY AND APPLICATIONS OF SATISFIABILITY TESTING, PROCEEDINGS, 2005, 3569 : 107 - 121
[28] Checking JML specifications using an extensible software model checking framework
Edwin Robby
Matthew B. Rodríguez
John Dwyer
International Journal on Software Tools for Technology Transfer, 2006, 8 (3) : 280 - 299
[29] Checking strong specifications using an extensible software model checking framework
Robby
Rodríguez, E
Dwyer, MB
Hatcliff, J
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2004, 2988 : 404 - 420
[30] Efficient Realizability Checking by Modularization of LTL Specifications
Ito, Sohei
Osari, Kenji
Shimakawa, Masaya
Hagihara, Shigeki
Yonezaki, Naoki
COMPUTER JOURNAL, 2022, 65 (10): : 2801 - 2814

← 1 2 3 4 5 →