首页> 外文OA文献 >Approches formelles pour l'analyse de la performabilité des systèmes communicants mobiles (Applications aux réseaux de capteurs sans fil)
【2h】

Approches formelles pour l'analyse de la performabilité des systèmes communicants mobiles (Applications aux réseaux de capteurs sans fil)

机译:approhes formeles pour l'analysis delaperformabilitédessystèmesmocmunitiesmobiles(applicationsauxréseauxdecapteurs sans fil)

代理获取
本网站仅为用户提供外文OA文献查询和代理获取服务,本网站没有原文。下单后我们将采用程序或人工为您竭诚获取高质量的原文,但由于OA文献来源多样且变更频繁,仍可能出现获取不到、文献不完整或与标题不符等情况,如果获取不到我们将提供退款服务。请知悉。

摘要

Nous nous intéressons à l'analyse des exigences de performabilité des systèmes communicants mobiles par model checking. Nous modélisons ces systèmes à l'aide d'un formalisme de haut niveau issu du p-calcul, permettant de considérer des comportements stochastiques, temporels, déterministes, ou indéterministes. Cependant, dans le p-calcul, la primitive de communication de base des systèmes est la communication en point-à-point synchrone. Or, les systèmes mobiles, qui utilisent des réseaux sans fil, communiquent essentiellement par diffusion locale. C'est pourquoi, dans un premier temps, nous définissons la communication par diffusion dans le p-calcul, afin de mieux modéliser les systèmes que nous étudions. Nous proposons d'utiliser des versions probabilistes et stochastiques de l'algèbre que nous avons défini, pour permettre des études de performance. Nous en définissons une version temporelle permettant de considérer le temps dans les modèles. Mais l'absence d'outils d'analyse des propriétés sur des modèles spécifiés en une algèbre issue du p-calcul est un obstacle majeur à notre travail. La définition de règles de traduction en langage PRISM, nous permet de traduire nos modèles, en modèles de bas niveau supports du model checking, à savoir des chaînes de Markov à temps discret, à temps continu, des automates temporisés, ou des automates temporisés probabilistes. Nous avons choisi l'outil PRISM car, à notre connaissance, dans sa dernière version, il est le seul outil à supporter les formalismes de bas niveau que nous venons de citer, et ainsi il permet de réaliser des études de performabilité complètes. Cette façon de procéder nous permet de pallier à l'absence d'outils d'analyse pour nos modèles. Par la suite, nous appliquons ces concepts théoriques aux réseaux de capteurs sans fil mobiles.
机译:我们对通过模型检查来分析移动通信系统的性能需求感兴趣。我们使用p演算的高级形式主义对这些系统进行建模,从而使我们能够考虑随机,时间,确定性或不确定性行为。但是,在p演算中,系统的基本通信原语是同步点对点通信。但是,使用无线网络的移动系统主要通过本地广播进行通信。这就是为什么,首先,我们通过在p演算中的扩散来定义通信,以便更好地对我们正在研究的系统进行建模。我们建议使用已定义的概率形式和随机形式的代数,以进行性能研究。我们定义一个临时版本,允许考虑模型中的时间。但是,由于缺乏用于分析p微积分导致的代数中指定模型的属性的工具,这是我们工作的主要障碍。 PRISM语言中转换规则的定义使我们可以将模型转换为支持模型检查的低级模型,即离散时间,连续时间马尔可夫链,定时自动机或概率定时自动机。我们之所以选择PRISM工具,是因为据我们所知,它是最新版本中唯一支持我们刚刚提到的低级形式主义的工具,因此可以进行完整的性能研究。这种进行方式使我们能够补偿模型缺乏分析工具的情况。随后,我们将这些理论概念应用于移动无线传感器网络。

著录项

  • 作者

    ABO Robert; BARKAOUI Kamel;

  • 作者单位
  • 年度 2011
  • 总页数
  • 原文格式 PDF
  • 正文语种 French
  • 中图分类

相似文献

  • 外文文献
  • 专利

客服邮箱:kefu@zhangqiaokeyan.com

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

  • 服务号