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 条

[31] Checking amalgamability conditions for CASL architectural specifications
Klin, B
Hoffman, P
Tarlecki, A
Schröder, L
Mossakowski, T
MATHEMATICAL FOUNDATIONS OF COMPUTER SCIENCE 2001, 2001, 2136 : 451 - 463
[32] Model checking class specifications for web applications
Choi, EH
Watanabe, H
12TH ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE, PROCEEDINGS, 2005, : 67 - 75
[33] Partitioned model checking from software specifications
Feng, Xiushan
Hu, Alan J.
Yang, Jin
ASP-DAC 2005: PROCEEDINGS OF THE ASIA AND SOUTH PACIFIC DESIGN AUTOMATION CONFERENCE, VOLS 1 AND 2, 2005, : 583 - 587
[34] Model checking early requirements specifications in Tropos
Fuxman, A
Pistore, M
Mylopoulos, J
Traverso, P
FIFTH IEEE INTERNATIONAL SYMPOSIUM ON REQUIREMENTS ENGINEERING, PROCEEDINGS, 2001, : 174 - 181
[35] Refining Task Specifications Using Model Checking
Yeolekar, Anand
Metta, Ravindra
Venkatesh, R.
Chakraborty, Samarjit
2018 IEEE 24TH INTERNATIONAL CONFERENCE ON EMBEDDED AND REAL-TIME COMPUTING SYSTEMS AND APPLICATIONS (RTCSA), 2018, : 185 - 191
[36] A model checking approach for verifying COWS specifications
Fantechi, Alessandro
Gnesi, Stefania
Lapadula, Alessandro
Mazzanti, Franco
Pugliese, Rosario
Tiezzi, Francesco
FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING, PROCEEDINGS, 2008, 4961 : 230 - +
[37] Model checking Z specifications using SAL
Smith, G
Wildman, L
ZB 2005: FORMAL SPECIFICATION AND DEVELOPMENT IN Z AND B, PROCEEDINGS, 2005, 3455 : 85 - 103
[38] Model Checking Systems Against Epistemic Specifications
Lomuscio, Alessio R.
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2014, (146):
[39] MemSAT: Checking Axiomatic Specifications of Memory Models
Torlak, Emina
Vaziri, Mandana
Dolby, Julian
ACM SIGPLAN NOTICES, 2010, 45 (06) : 341 - 350
[40] Developing and checking prescriptive specifications for safety improvement
Yih, S
Tian, J
MICROPROCESSORS AND MICROSYSTEMS, 1998, 21 (10) : 587 - 594

← 1 2 3 4 5 →