首页    期刊浏览 2024年12月05日 星期四
登录注册

文章基本信息

  • 标题:Verifying ODP Computational Behavioral Specification by using B-Method
  • 本地全文:下载
  • 作者:Mr. Jalal Laassiri ; Saïd El Hajji ; Mr. Mohamed Bouhdadi
  • 期刊名称:International Journal of Computer Science and Security (IJCSS)
  • 电子版ISSN:1985-1553
  • 出版年度:2010
  • 卷号:4
  • 期号:1
  • 页码:31-39
  • 出版社:Computer Science Journals
  • 摘要:The Reference Model for Open Distributed Processing (RM-ODP) defines a framework for the development of Open Distributed Processing (ODP) systems in terms of five viewpoints. Each viewpoint language defines concepts and rules for specifying ODP systems from the corresponding viewpoint. However the ODP viewpoint languages are abstract and do not show how these should be represented and specified. We treat in this paper the need of formal notation and specification for behavior al concepts in the Computational language. Using the Unified Modeling Language (UML)/OCL (Object Constraints Language) we define a formal semantics for a fragment of ODP behavior concepts defined in the RM-ODP foundations part and in the Computational language. We mainly focus on time, action, behavior constraints (sequentiality, non determinism and concurrency constraints), and policies (permission, obligation, prohibition). We also give a mapping of the considered concepts to Event-B. This will permit the verification of such specifications. Finally we explore the benefits provided by the new extension mechanisms of B-Method for verifying the ODP computational specifications.
  • 关键词:RM-ODP; Computational Language; UML/OCL; Behavior Semantics; computational specifications; B-Method
国家哲学社会科学文献中心版权所有