• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>International journal of agent-oriented software engineering >Formally Specifying And Verifying Mobile Agents - Model Checking Mobility: The Mobioz Approach
【24h】

Formally Specifying And Verifying Mobile Agents - Model Checking Mobility: The Mobioz Approach

机译：正式指定和验证移动代理-模型检查移动性：Mobioz方法

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

摘要

The notion of the mobile agent has been around for over a decade in order to capture the new form of computation in communication networks. A mobile agent is a computing entity which can move around different hosts on the network, carrying its state and procedures. Mobile bject-Z (MobiOZ), which is designed to provide a practical means to the specifiers who are working on mobile agent applications, is an extended notation of Object-Z, with mobile and communication primitives for specifying and verifying mobile agent applications. In this paper, we will give an overview of the MobiOZ notation and present its semantic foundation, then demonstrate how the specifications in MobiOZ can be simulated and verified by SPIN, a model checker, by translating MobiOZ specifications into PROcess MEta LAnguage (PROMELA), a process-based formal specification language of SPIN.
机译：为了捕捉通信网络中新的计算形式，移动代理的概念已经存在了十多年。移动代理是一个计算实体，可以承载网络的不同主机并携带其状态和过程。 Mobile bject-Z（MobiOZ）旨在为正在处理移动代理程序应用程序的规范者提供一种实用的手段，它是Object-Z的扩展表示，具有用于指定和验证移动代理程序应用程序的移动和通信原语。在本文中，我们将概述MobiOZ符号并介绍其语义基础，然后演示如何通过模型检查器SPIN将MobiOZ规范转换为PROcess MEta语言（PROMELA）来模拟和验证MobiOZ中的规范，一种基于流程的SPIN正式规范语言。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号