| 引用本文: | 邓小妮,袁卫卫,曾熠,等.指挥控制的形式化描述与性质验证.[J].国防科技大学学报,2003,25(6):62-66.[点击复制] |
| DENG Xiaoni,YUAN Weiwei,ZENG Yi,et al.The Formal Specification and Property Verification of the Command and Control[J].Journal of National University of Defense Technology,2003,25(6):62-66[点击复制] |
|
| |
|
|
| 本文已被：浏览 6510次 下载 5902次 |
| 指挥控制的形式化描述与性质验证 |
| 邓小妮, 袁卫卫, 曾熠, 罗雪山 |
|
(国防科技大学 人文与管理学院，湖南 长沙 410073)
|
| 摘要: |
| 在分析了IDEF0基本模型及其军用模型的基础上，结合面向对象的分析方法，提出了一个通用的指挥控制对象的概念模型，并采用形式化描述语言LOTOS(Language of Temporal Ordering Specification) 和基于动作的时序逻辑ACTL(Action Based Temporal Logical) 对系统进行了形式化描述和性质验证。这为C4ISR系统的需求描述和验证提供了一种新的思路和方法。 |
| 关键词: 指挥控制 C4ISR 形式化描述 验证 LOTOS |
| DOI： |
| 投稿日期：2003-04-23 |
| 基金项目:国家部委预研基金资助项目 |
|
| The Formal Specification and Property Verification of the Command and Control |
| DENG Xiaoni, YUAN Weiwei, ZENG Yi, LUO Xueshan |
|
(College of Humanities and Management, National Univ. of Defense Technology, Changsha 410073, China)
|
| 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. |
| Keywords: command and control C4ISR formal specification verification LOTOS |
|
|
|
|
|
