Formal specification and proof of Gridjack

摘要：

Good computational model design has always been a key factor in determining whether it will be a successful system. A new approach was proposed to formally specifying and proving the Gridjack computational model design which uses architectural description language WRIGHT together with the process algebra CSP. Formal specification in WRIGHT provides a convenient way to modeling the complex overall structure by describing the interfaces and computations of the component combination. Furthermore, the model was easily proved in terms of laws of the CSP operators by defining the hidden actions of component processes with model-checking tool FDR. This approach can also be applied to formalization of other computational models, which is helpful to rapidly check the model features and revise the design.

关键词： CSP Gridjack computational model WRIGHT formal specification

作者: Li Mao Deyu Qi

作者单位: Research Institute of Computer System, South China University of Technology, Guangzhou, China Deptme Research Institute of Computer System, South China University of Technology, Guangzhou, China

会议类型: 国际会议

会议名称: 2012 Fifth International Symposium on Computational Intelligence and Design 第五届计算智能与设计国际会议 ISCID 2012

会议地点: 杭州

会议语种:英文

页码: 110-114

在线出版日期: 2012-10-28（万方平台首次上网日期，不代表论文的发表时间）