作者：李勇; 李揭阳; 曹子宁体系结构分析设计语言构件式系统计算树逻辑z语言模型检测
摘要：构件式系统是一种采用构件组合技术实现的结构系统，即在采用单个构件封装简单的业务功能基础上，通过集成多个构件逐步构造新的组合构件来实现比较复杂的业务功能。在开发构件式系统软件的过程中，正确的子构件模型组合方式才有可能构建安全可靠的总构件模型。计算树逻辑（CTL）能较为准确地描述状态迁移的时序性质，而擅长形式规格说明的Z语言在数据约束方面具有强大作用。因此，基于CTL和Z语言对体系结构分析设计语言（AADL）进行功能拓展，即可建立更为安全可靠的组合模型。为此，在分析研究AADL的建模元素和建模流程的基础上，提出了计算树逻辑CTL和Z语言对AADL行为附件进行扩充的思路与方法。该方法可有效保证构建模型的合理性和有序性。基于CZ—AADL建模规范和飞行管理系统实例进行了验证实验。实验结果表明，CZ—AADL建模规范增强了AADL建模的灵活性和多样性。也为采用不同建模方式的多模块间的融合提供了可能。
注：因版权方要求，不能公开全文，如需全文，请咨询杂志社
