指挥控制的形式化描述与性质验证
DOI:
作者:
作者单位:

作者简介:

通讯作者:

中图分类号:

基金项目:

国家部委预研基金资助项目


The Formal Specification and Property Verification ofthe Command and Control
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

    在分析了IDEF0基本模型及其军用模型的基础上,结合面向对象的分析方法,提出了一个通用的指挥控制对象的概念模型,并采用形式化描述语言LOTOS(Language of Temporal Ordering Specification) 和基于动作的时序逻辑ACTL(Action Based Temporal Logical) 对系统进行了形式化描述和性质验证。这为C4ISR系统的需求描述和验证提供了一种新的思路和方法。

    Abstract:

    A conceptual model of the command and control object (C2O) is described using the formal language LOTOS(Language of Temporal Ordering Specification), and the main properties of C2O and C2O-based systems are defined using ACTL(Action Based Temporal Logical). Then a model-based-verification approach is provided aiming at the above key properties verification. The practical example shows that the new approach is viable.

    参考文献
    相似文献
    引证文献
引用本文

邓小妮,袁卫卫,曾熠,等.指挥控制的形式化描述与性质验证. The Formal Specification and Property Verification ofthe Command and Control[J].国防科技大学学报,2003,25(6):62-66.

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2003-04-23
  • 最后修改日期:
  • 录用日期:
  • 在线发布日期: 2013-06-14
  • 出版日期:
文章二维码