The Formal Specification and Property Verification ofthe Command and Control
Author:
Affiliation:
Fund Project:
摘要
|
图/表
|
访问统计
|
参考文献
|
相似文献
|
引证文献
|
资源附件
|
文章评论
摘要:
在分析了IDEF0基本模型及其军用模型的基础上,结合面向对象的分析方法,提出了一个通用的指挥控制对象的概念模型,并采用形式化描述语言LOTOS(Language of Temporal Ordering Specification) 和基于动作的时序逻辑ACTL(Action Based Temporal Logical) 对系统进行了形式化描述和性质验证。这为C4ISR系统的需求描述和验证提供了一种新的思路和方法。
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.
参考文献
相似文献
引证文献
引用本文
邓小妮,袁卫卫,曾熠,等.指挥控制的形式化描述与性质验证. The Formal Specification and Property Verification ofthe Command and Control[J].国防科技大学学报,2003,25(6):62-66.