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 条
  • [11] Checking formal specifications under simulation
    Canfield, W
    Emerson, EA
    Saha, A
    INTERNATIONAL CONFERENCE ON COMPUTER DESIGN - VLSI IN COMPUTERS AND PROCESSORS, PROCEEDINGS, 1997, : 455 - 460
  • [12] Static consistency checking for distributed specifications
    Nentwich, C
    Emmerich, W
    Finkelstein, A
    16TH ANNUAL INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING (ASE 2001), PROCEEDINGS, 2001, : 115 - 124
  • [13] Model checking linear logic specifications
    Bozzano, M
    DelZanno, G
    Martelli, M
    THEORY AND PRACTICE OF LOGIC PROGRAMMING, 2004, 4 : 573 - 619
  • [14] Local Module Checking for CTL Specifications
    Basu, Samik d
    Roop, Partha S.
    Sinha, Roopak
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2007, 176 (02) : 125 - 141
  • [15] Model Checking Specifications of Smart Cards
    Greimel, Karin
    Sessler, Norman
    Klotz, Thomas
    39TH ANNUAL CONFERENCE OF THE IEEE INDUSTRIAL ELECTRONICS SOCIETY (IECON 2013), 2013, : 7736 - 7741
  • [16] COMPRESSED MEDICAL AIR - SPECIFICATIONS AND CHECKING
    EDOUARD, B
    RAMOND, B
    BROSSARD, D
    CARTRON, MF
    RICORDEL, I
    CARLIER, A
    MEDECINE ET ARMEES, 1989, 17 (02): : 121 - 127
  • [17] Model checking large software specifications
    Chan, W
    Anderson, RJ
    Beame, P
    Burns, S
    Modugno, F
    Notkin, D
    Reese, JD
    IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1998, 24 (07) : 498 - 520
  • [18] Model checking TLA+ specifications
    Yu, Y
    Manolios, P
    Lamport, L
    CORRECT HARDWARE DESIGN AND VERIFICATION METHODS, 1999, 1703 : 54 - 66
  • [19] Support for Model Checking Z Specifications
    Siregar, Maria Ulfah
    PROCEEDINGS OF 2016 IEEE 17TH INTERNATIONAL CONFERENCE ON INFORMATION REUSE AND INTEGRATION (IEEE IRI), 2016, : 241 - 248
  • [20] Model checking RAISE applicative specifications
    Perna, Juan Ignacio
    George, Chris
    SEFM 2007: FIFTH IEEE INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND FORMAL METHODS, PROCEEDINGS, 2007, : 257 - +
12345