首页> 外文期刊>Computer Languages, Systems & Structures >Frame conditions in the automatic validation and verification of UML/OCL models: A symbolic formulation of modifies only statements
【24h】

Frame conditions in the automatic validation and verification of UML/OCL models: A symbolic formulation of modifies only statements

机译:UML / OCL模型的自动验证和验证中的框架条件:仅修改语句的符号表示

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

摘要

Validation and verification of UML/OCL models is a crucial task in the design of complex software/hardware systems. The behavior in those models is expressed in terms of operations with pre- and postconditions. These, however, are often not precise enough to describe what may or may not be modified in a transition between two system states. This frame problem is commonly addressed by providing additional constraints in terms of so-called frame conditions and has already been considered in different research areas in the last decades—except for UML/OCL where corresponding approaches have been investigated only recently. Among these, the so-calledmodifies onlystatements constitute a very promising concept which is complementary to all other approaches. More precisely, instead of allowing arbitrary modifications in principle and prohibiting certain undesired behavior, the statements explicitly describe what is allowed to change. However, this approach to frame conditions has not been considered so far in any of the numerous approaches for the automatic validation and verification of the behavior in UML/OCL models that have been proposed in the last years. Most of these approaches rely on a symbolic formulation of all possible system states and transitions between them. Therefore, in this paper we explain howmodifies onlystatements can be integrated into an existing symbolic formulation. Based on this, we evaluate the applicability of the presented concept and compare it to previous implementations of frame conditions.
机译:在复杂的软件/硬件系统设计中,UML / OCL模型的验证和验证是至关重要的任务。这些模型中的行为表示为具有前置条件和后置条件的运算。然而,这些通常不够精确,无法描述在两个系统状态之间的转换中可能会或可能不会修改的内容。通常通过在所谓的框架条件方面提供其他约束来解决该框架问题,并且在最近的几十年中,不同的研究领域已经对此框架问题进行了研究,但UML / OCL除外,后者仅在最近才研究了相应的方法。在这些之中,所谓的仅修改陈述构成了非常有前途的概念,它是对所有其他方法的补充。更准确地说,这些声明不是在原则上允许任意修改并禁止某些不希望有的行为,而是明确描述了允许更改的内容。但是,到目前为止,在最近几年提出的用于UML / OCL模型中行为的自动验证和验证的众多方法中,至今尚未考虑到这种针对框架条件的方法。这些方法中的大多数都依赖于所有可能系统状态及其之间转换的符号表示。因此,在本文中,我们解释了仅修饰语如何可以集成到现有的符号表达中。基于此,我们评估了提出的概念的适用性,并将其与帧条件的先前实现进行了比较。

著录项

相似文献

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

客服邮箱:kefu@zhangqiaokeyan.com

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

  • 服务号