| 指挥控制的形式化描述与性质验证 |
| |
| 引用本文： | 邓小妮,袁卫卫,曾熠,罗雪山.指挥控制的形式化描述与性质验证[J].国防科技大学学报,2003,25(6):62-66. |
| |
| 作者姓名： | 邓小妮 袁卫卫 曾熠 罗雪山 |
| |
| 作者单位： | 国防科技大学人文与管理学院,湖南,长沙,410073 |
| |
| 基金项目： | 国家部委预研基金资助项目 |
| |
| 摘 要： | 在分析了IDEF0基本模型及其军用模型的基础上,结合面向对象的分析方法,提出了一个通用的指挥控制对象的概念模型,并采用形式化描述语言LOTOS(LanguageofTemporalOrderingSpecification)和基于动作的时序逻辑ACTL(ActionBasedTemporalLogical)对系统进行了形式化描述和性质验证。这为C4ISR系统的需求描述和验证提供了一种新的思路和方法。
|
| 关 键 词： | 指挥控制 C4ISR 形式化描述 验证 LOTOS |
| 文章编号： | 1001-2486(2003)06-0062-05 |
| 收稿时间： | 2003/4/23 0:00:00 |
| 修稿时间： | 2003年4月23日 |
The Formal Specification and Property Verification of the Command and Control |
| |
| DENG Xiaoni,YUAN Weiwei,ZENG Yi and LUO Xueshan.The Formal Specification and Property Verification of the Command and Control[J].Journal of National University of Defense Technology,2003,25(6):62-66. |
| |
| Authors: | DENG Xiaoni YUAN Weiwei ZENG Yi and LUO Xueshan |
| |
| Institution: | College of Humanities and Management, National Univ. of Defense Technology, Changsha 410073, China;College of Humanities and Management, National Univ. of Defense Technology, Changsha 410073, China;College of Humanities and Management, National Univ. of Defense Technology, Changsha 410073, China;College of Humanities and Management, National Univ. of Defense Technology, Changsha 410073, China |
| |
| Abstract: | A conceptual model of the command and control object (C~2O) is described using the formal language LOTOS(Language of Temporal Ordering Specification), and the main properties of C~2O and C~2O-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 C~4ISR formal specification verification LOTOS |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
| 点击此处可从《国防科技大学学报》浏览原始摘要信息 |
| 点击此处可从《国防科技大学学报》下载免费的PDF全文 |
|
