引用本文: | 邓小妮,袁卫卫,曾熠,等.指挥控制的形式化描述与性质验证[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[点击复制] |
|
|
|
本文已被:浏览 6067次 下载 5345次 |
指挥控制的形式化描述与性质验证 |
邓小妮, 袁卫卫, 曾熠, 罗雪山 |
(国防科技大学 人文与管理学院,湖南 长沙 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 |
|
|
|
|
|