论文部分内容阅读
嵌入式系统在关系国计民生的众多行业中应用广泛。确保嵌入式系统正确可靠对经济发展、人身安全和社会稳定有着重要影响，是当今计算机和控制领域的重要研究课题。形式化方法是确保系统正确性和可靠性的重要手段。然而，形式化方法以数学理论为基础，对用户有较高要求，限制了形式化方法在工业界的应用。本文以PLC软件为研究对象，针对其固有特性和现实问题，分别从语言层、检查层和实现层三个方面研究了构件化建模方法。论文主要工作包括：1.语言层，开发了领域建模语言PLC-BIP。PLC-BIP以形式化语言BIP为基础，在领域知识表达和模型语义标注两方面分别进行了扩展。实现了PLC周期工作方式、定时器、函数调用和中断调度机制等特征的建模，方便用户建立系统级模型。给出了自顶向下的嵌入式系统一般分解原则和自底向上的构件与系统映射关系。定义IL指令的操作语义，并给出基于转换的方法为已有代码建立形式化模型。2.检查层，针对构件化建模过程中可能违反领域潜在约束的问题，提出一种基于领域语义的静态检查框架。给出了领域约束的形式化表达，将领域约束是否满足的问题转化为领域概念格上的约束求解问题。可在建模过程中自动检查模型相对于领域约束的满足情况，尽早发现建模错误。3.实现层，提出基于形式化模型自动生成PLC代码的方法。该方法综合考虑了实现平台的硬件特征以及时间和资源约束，确保生成代码可运行。实现了PLC代码自动生成算法并结合双门控制案例展示了自动生成PLC代码的步骤。4.实现了构件化建模工具原型系统。它提供图形化的模型编辑界面；提供PLC装置控制领域构件类型和操作算子；实现了模型语法检查和一致性检查；支持模型的语义标注以及领域约束的实时检查。给出了该方法在无锡灵山梵宫门仓控制系统上的典型应用。案例通过PLC-BIP语言提供的领域操作算子和构件类型，建立了系统模型，体现了建模方法的易用性。在建模过程中，工具自动检查模型是否满足领域约束。