首页> 外文期刊>Programming and Computer Software >Comparison of specification decomposition methods in Event-B
【24h】

Comparison of specification decomposition methods in Event-B

机译:Event-B中规范分解方法的比较

获取原文
获取原文并翻译 | 示例

摘要

Decomposition is an important phase in the design of medium and large-scale systems. Various architectures of software systems and decomposition methods are studied in numerous publications. Presently, formal specifications of software systems are mainly used for experimental purposes; for this reason, their size and complexity are relatively low. As a result, in the development of a nontrivial specification, different approaches to the decomposition should be compared and the most suitable approach should be chosen. In this paper, the experience gained in the deductive verification of the formal specification of the mandatory entity-role model of access and information flows control in Linux (MROSL DP-model) using the formal Event-B method and stepwise refinement technique is analyzed. Two approaches to the refinementbased decomposition of specifications are compared and the sources and features of the complexity of the architecture of the model are investigated.
机译:分解是中型和大型系统设计的重要阶段。在许多出版物中研究了软件系统的各种体系结构和分解方法。当前,软件系统的正式规范主要用于实验目的。因此,它们的大小和复杂性相对较低。结果,在制定非同寻常的规范时,应比较不同的分解方法,并选择最合适的方法。本文分析了使用形式化Event-B方法和逐步改进技术对Linux中访问和信息流控制的强制实体角色模型(MROSL DP模型)的形式规范进行演绎验证的经验。比较了两种基于细化的规格分解方法,并研究了模型体系结构复杂性的来源和特征。

著录项

  • 来源
    《Programming and Computer Software》 |2016年第4期|198-205|共8页
  • 作者单位

    Educ Informat Secur Community, Moscow, Russia;

    Russian Acad Sci, Inst Syst Programming, Ul Solzhenitsyna 25, Moscow 109004, Russia|Moscow MV Lomonosov State Univ, GSP-1, Moscow 119991, Russia|Natl Res Univ, Higher Sch Econ, 1 Nd Kozhukhovsky Proezd 1-7, Moscow 101000, Russia;

    Russian Acad Sci, Inst Syst Programming, Ul Solzhenitsyna 25, Moscow 109004, Russia|Moscow MV Lomonosov State Univ, GSP-1, Moscow 119991, Russia|Natl Res Univ, Higher Sch Econ, 1 Nd Kozhukhovsky Proezd 1-7, Moscow 101000, Russia;

    Russian Acad Sci, Inst Syst Programming, Ul Solzhenitsyna 25, Moscow 109004, Russia|Moscow Inst Phys & Technol, Inst Skii Per 9, Dolgoprudnyi 141700, Moscow Oblast, Russia;

    Russian Acad Sci, Inst Syst Programming, Ul Solzhenitsyna 25, Moscow 109004, Russia;

  • 收录信息
  • 原文格式 PDF
  • 正文语种 eng
  • 中图分类
  • 关键词

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱:kefu@zhangqiaokeyan.com

京公网安备:11010802029741号 ICP备案号:京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有
  • 客服微信

  • 服务号