| 指挥控制的形式化描述与性质验证 |
| |
| 作者姓名： | 邓小妮 袁卫卫 曾熠 罗雪山 |
| |
| 作者单位： | 国防科技大学人文与管理学院,湖南,长沙,410073;国防科技大学人文与管理学院,湖南,长沙,410073;国防科技大学人文与管理学院,湖南,长沙,410073;国防科技大学人文与管理学院,湖南,长沙,410073 |
| |
| 基金项目： | 国家部委预研基金资助项目 |
| |
| 摘 要： | 在分析了IDEF0基本模型及其军用模型的基础上,结合面向对象的分析方法,提出了一个通用的指挥控制对象的概念模型,并采用形式化描述语言LOTOS(LanguageofTemporalOrderingSpecification)和基于动作的时序逻辑ACTL(ActionBasedTemporalLogical)对系统进行了形式化描述和性质验证。这为C4ISR系统的需求描述和验证提供了一种新的思路和方法。
|
| 关 键 词： | 指挥控制 C4ISR 形式化描述 验证 LOTOS |
| 文章编号： | 1001-2486(2003)06-0062-05 |
| 收稿时间： | 2003-04-23 |
| 修稿时间： | 2003-04-23 |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
| 点击此处可从《国防科技大学学报》浏览原始摘要信息 |
|
点击此处可从《国防科技大学学报》下载免费的PDF全文 |
|
