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 条

[41] Checking consistency of SDL plus MSC specifications
D'Souza, D
Mukund, M
MODEL CHECKING SOFTWARE, 2003, 2648 : 151 - 165
[42] An Approach for Checking Resource Feasibility of Workflow Specifications
Xiao Jing
Wei Xiong
Chen Shu
PROCEEDINGS OF THE FIRST INTERNATIONAL WORKSHOP ON EDUCATION TECHNOLOGY AND COMPUTER SCIENCE, VOL I, 2009, : 163 - 167
[43] Checking consistency of SDL+MSC specifications
D'Souza, Deepak
Mukund, Madhavan
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2003, 2648 : 151 - 165
[44] Checking Correctness of Code Generator Architecture Specifications
Hasabnis, Niranjan
Qiao, Rui
Sekar, R.
2015 IEEE/ACM INTERNATIONAL SYMPOSIUM ON CODE GENERATION AND OPTIMIZATION (CGO), 2015, : 167 - 178
[45] Model checking for object specifications in hidden algebra
Lucanu, D
Ciobanu, G
VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, PROCEEDINGS, 2004, 2937 : 97 - 109
[46] MemSAT: Checking Axiomatic Specifications of Memory Models
Torlak, Emina
Vaziri, Mandana
Dolby, Julian
PLDI '10: PROCEEDINGS OF THE 2010 ACM SIGPLAN CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION, 2010, : 341 - 350
[47] Model-checking TRIO specifications in SPIN
Morzenti, A
Pradella, M
San Pietro, P
Spoletini, P
FME 2003: FORMAL METHODS, PROCEEDINGS, 2003, 2805 : 542 - 561
[48] Efficient Black-Box Checking via Model Checking with Strengthened Specifications
Shijubo, Junya
Waga, Masaki
Suenaga, Kohei
RUNTIME VERIFICATION (RV 2021), 2021, 12974 : 100 - 120
[49] CirCUs: A satistiability solver geared towards bounded model checking
Jin, HS
Awedh, M
Somenzi, F
COMPUTER AIDED VERIFICATION, 2004, 3114 : 519 - 522
[50] Formal Consistency Checking over Specifications in Natural Languages
Yan, Rongjie
Cheng, Chih-Hong
Chai, Yesheng
2015 DESIGN, AUTOMATION & TEST IN EUROPE CONFERENCE & EXHIBITION (DATE), 2015, : 1677 - 1682

← 1 2 3 4 5 →