指挥控制的形式化描述与性质验证

• 作者: 曾熠 罗雪山 袁卫卫 邓小妮
• 来源期刊: 国防科技大学学报
• 学科: 工学
• 关键词: 指挥控制 C4ISR 形式化描述 验证 LOTOS
• 年，卷（期）: 2003,（6）
• 所属期刊栏目: 电子工程·系统工程
• 页码范围: 62-66
• 页数: 5页
• 分类号: TP301.2
• 字数: 2923字
• 语种: 中文
• DOI: 10.3969/j.issn.1001-2486.2003.06.014

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	袁卫卫	国防科技大学人文与管理学院	10	153	6.0	10.0
2	罗雪山	国防科技大学人文与管理学院	123	1054	17.0	23.0
3	邓小妮	国防科技大学人文与管理学院	7	11	1.0	3.0
4	曾熠	国防科技大学人文与管理学院	8	105	6.0	8.0