...
  • 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>電子情報通信学会技術研究報告. ソフトウェアインタプライズモデリンゲ. Software Interprise Modeling >上流設計からモデル検査プロセスまでの一貫設計検証環境～UML記述からSPINモデル検査器用プロセス定義及び線形時相論理式への自動変換手法
【24h】

上流設計からモデル検査プロセスまでの一貫設計検証環境～UML記述からSPINモデル検査器用プロセス定義及び線形時相論理式への自動変換手法

机译：对于自旋模型检查器自动转换方法SPIN模型检查器和自动转换方法SPIN模型Testimulator到UML描述从上游设计验证环境到模型检测过程

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

摘要

SPINモデル検査器を実行するには，専用の仕様記述言語PROMELAで対象モデルを記述する．また，検査対象の仕様の記述には線形時相論理（LTL）式を用いる．本研究では，システム開発の上流設計段階で使われるUML 図を，PROMELAコード及びLTL式に自動変換する手法を提案する．UMLのステートマシン図と配置図を組みで利用し，ステートマシン図に，対象モデルの振る舞いや配置状況，要求仕様を記述し，PROMELAコードへの自動変換を実現する．一方，要求仕様として，UMLのシーケンス図を仕様パターンに準拠した記法に制限·展開することで，LTL式の自動生成を実現する．以上の機能を有する援用ツール群を試作し，ある通信プロトコルを対象とした上位設計に対する自動変換を実施し，評価を行った．
机译：要执行旋转模型检查器，请使用专用规范描述语言PROMELA描述目标模型。 另外，线性时间相位逻辑（LTL）用作要检查规范的描述。 在本研究中，我们提出了一种方法来自动转换在系统开发的上游设计阶段中使用的UML图。 UML的状态机图组合使用，状态机图描述了目标模型，排列状态和目标模型所需规范的行为，并实现了对PROMELA代码的自动转换。 另一方面，作为要求规范，通过根据规范模式限制和扩展规范模式中的UML的序列图来实现LTL表达的自动生成。 具有上述功能的测试工具组是原型的，并且执行了对某些通信协议的上部设计的自动转换，并进行评估。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号