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 条

[1] Model-Checking Circus State-Rich Specifications
Medeiros Oliveira, Marcel Vinicius
Sampaio, Augusto C. A.
Conserva Filho, Madiel S.
INTEGRATED FORMAL METHODS, IFM 2014, 2014, 8739 : 39 - 54
[2] Type checking parametrised programs and specifications in ASL+FPC
Aspinall, D
RECENT TRENDS IN ALGEBRAIC DEVELOPMENT TECHNIQUES, 2003, 2755 : 129 - 144
[3] Operational semantics for model checking circus
Woodcock, J
Cavalcanti, A
Freitas, L
FM 2005: FORMAL METHODS, PROCEEDINGS, 2005, 3582 : 237 - 252
[4] Consistency Checking for LSC Specifications
Guo, Hai-Feng
Zheng, Wen
Subramaniam, Mahadevan
THIRD INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING, PROCEEDINGS, 2009, : 119 - 126
[5] Automatic checking of instruction specifications
Fernandez, M
Ramsey, N
PROCEEDINGS OF THE 1997 INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING, 1997, : 326 - 336
[6] Model checking interactor specifications
Campos J.C.
Harrison M.D.
Automated Software Engineering, 2001, 8 (3-4) : 275 - 310
[7] Type checking for software system specifications in real-time process algebra
Liu, CW
Tan, XM
DCABES 2004, PROCEEDINGS, VOLS, 1 AND 2, 2004, : 1077 - 1083
[8] Model checking RAISE applicative specifications
Perna, Juan I.
George, Chris
FORMAL ASPECTS OF COMPUTING, 2013, 25 (03) : 365 - 388
[9] Checking temporal properties in SystemC specifications
Braun, A
Gerlach, J
Rosenstiel, W
SEVENTH IEEE INTERNATIONAL HIGH-LEVEL DESIGN VALIDATION AND TEST WORKSHOP, PROCEEDINGS, 2002, : 23 - 27
[10] Checking MSC specifications for timing inconsistency
Li, XD
Tan, WK
Zheng, GL
JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY, 2002, 17 (01) : 47 - 55

← 1 2 3 4 5 →