期刊文献+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息

一个集成形式化模型及其操作语义

An Integrated Formalized Model and Its Operational Semantics
下载PDF
导出
摘要 形式化方法在程序验证、模型检测的研究有着重要作用,集成形式化方法是形式化方法发展的一个方向.BCCS模型是集成B方法和进程代数CCS构建的一个混成模型,模型中给出了一个轻量级的描述语言,但缺少语义的支持.为了保证这个描述语言的完备性和一致性,本文则在传值CCS操作语义的基础上,结合B方法对抽象数据结构的定义、系统的限制以及功能处理,给出了BCCS的操作语义,进一步刻画BCCS模型. Formal methods play an important role in the study of program verification and model-checking. Integrated formal methods are a development direction of formal methods. The model of BCCS which integrates B language and CCS is a hybrid model and in this model, a light-weight description language is provided. In order to ensure completeness and consistency of this language, the operational semantics of BCCS is given on the basis of operational semantics of value-passing CCS and by combining the definition of abstract data structure, the systems restrictions and functional treatment using the B method so as to present a further description of the model of BCCS.
作者 匡春临 匡国防
机构地区 洛阳师范学院信息技术学院
出处 《洛阳师范学院学报》 2011年第2期72-75,共4页 Journal of Luoyang Normal University
关键词 形式化方法 BCCS模型 操作语义 formal method BCCS operational semantics
分类号 TP314 [自动化与计算机技术—计算机软件与理论]
  • 相关文献

参考文献8

  • 1匡春临,潘孝铭,蒋胜利.集成CCS和B语言的形式化方法[J].计算机工程与科学,2007,29(11):102-104. 被引量：2
  • 2Lamsweerde A V. Formal Specification : a Roadmap[ C]. the future of software engineering, A Finkelstein, ACM Press, 2000: 147 - 159.
  • 3Smith G, Derrick J. Specification, Refinement and Verification of Concurrent Systems - An Integration of Object - Z and CSP [ J ]. Formal Methods in System Design, 2001, 18 : 249 - 284.
  • 4Toetenal W J. model - oriented specification of communication agents [ D ]. Vilnius University, faculty of mathematics and infor- matics. 1992.
  • 5Bruns G. A Language for Value -passing CCS[ R]. Technical Report ECSLFCS -91 - 175, University of Edinburgh. 1991.
  • 6陆如钤.计算机语言的形式语义[M].北京:科学出版社,1992.
  • 7Abrial J R. The B- Book Assigning Programs to Meaning[ M].北京:电子工业出版社,2004.
  • 8Galloway A. Integrated Formal Methods with Richer Methodological Profiles for the Development of Multi - Perspective Systems [ D]. PhD thesis, University of Teesside, School of Computing and Mathematics, August, 1996.

二级参考文献9

  • 1HOARECAR．通信顺序进程[M]．周巢尘，译．北京：北京大学出版社，1990．
  • 2Butler M. csp2B: Apractical Approach to Combining CSP and B [J]. Formal Aspects of Computing, 2000, 12 (3): 182-198.
  • 3Schneider S, Treharne H. CSP Theorems for Communicating B Machines [R]. Technical Report CSD-TR-02-12, Department of Computer Science, Royal Holloway, University of London, 2003.
  • 4Butler M, Leuschel M. Combining CSP and B for Specification and Property Verification[A]. Proc of Formal Methods [C]. 2005. 221-236.
  • 5Smith G, Derrick J. Specification, Refinement and Verification of Concurrent Systems: An Integration of Object-Z and CSP[J]. Formal Methods in System Design, 2001, 18 (3):249-284.
  • 6Lano K. B语言与方法——实用形式化开发指南[M].鲍涌,刘建元,邹德林,等译.北京:高等教育出版社,1998.
  • 7Aceto L, Ingolfsdottir A, Larsen K G. Reactive Systems: Modelling, Specification and Verification[EB/OL]. http:// www. cs. auc. dk/_luea/SV/intro2ccs. pdf, 2007-01.
  • 8Taguchi K, Araki K. The State-Based CCS Semantics for Concurrent Z Specification[Z]. Proc of the 1st Int'l Conf on Formal Engineering Methods [ C ]. 1997. 283-292.
  • 9邹盛荣,郑国梁.B语言和方法与Z、VDM的比较[J].计算机科学,2002,29(10):136-138. 被引量：29

共引文献1

洛阳师范学院学报
2011年 第2期

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部