...
  • 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Science of Computer Programming >A discrete-time UML semantics for concurrency and communication in safety-critical applications
【24h】

A discrete-time UML semantics for concurrency and communication in safety-critical applications

机译：用于安全关键型应用程序中并发和通信的离散时间UML语义

获取原文
获取原文并翻译 | 示例
           
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

We define a subset krtUML of UML which is rich enough to express such modelling entities of UML, used in real-time applications, as active objects, dynamic object creation and destruction, dynamically changing communication topologies, combinations of synchronous and asynchronous communication, and shared memory usage through object attributes. We define a formal interleaving semantics for this kernel language by associating with each model M ∈ krtUML a symbolic transition system STS(M). We briefly outline how to compile models of industrial systems making use of generalisation hierarchies, weak and strong aggregation, and hierarchical state-machines into krtUML. The main aim of the paper is to provide an executable semantics for krtUML suitable for the formal verification of temporal model properties with existing model-checking tools.
机译：我们定义UML的子集krtUML，该子集足够丰富，可以表示实时应用中使用的UML建模实体，如活动对象，动态对象的创建和销毁，动态更改的通信拓扑，同步和异步通信的组合以及共享通过对象属性的内存使用情况。通过与每个模型M∈krtUML关联一个符号转换系统STS（M），我们为此内核语言定义了一种形式上的交织语义。我们简要概述了如何使用通用层次结构，弱聚合和强聚合以及层次状态机将工业系统模型编译为krtUML。本文的主要目的是为krtUML提供一种可执行的语义，适用于使用现有的模型检查工具对时态模型属性进行形式验证。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号