嵌入式系统构件模型的领域语义检查方法研究

Component-based modeling is a popular method to design and develop embedded systems. To ensure the correctness of the model, it is vital to check whether the connections among components are correct. With the increased scale of embedded systems, the amounts of connections and interactions increase. It becomes harder to check whether the connections are correct. Conventional semantic checking is based on type systems. Although type systems can check the mismatch of data types on the connected ports, it is hard to check whether the more sophisticated domain constraints are satisfied. Type systems are insufficient for the correctness-critical requests on components of embedded systems. In this project, we study on the methods to uniformly solve various domain-specific semantic errors, like forbidden connections, unit errors, mismatch of domain-specific semantics, transposition errors. We propose an ontology-based domain constraints specification language, which can uniformly and rigorously describe various domain constraints. We propose the automatic annotation method of domain-specific semantics, to build effectively the mappings between a component and its domain-specific semantics. We propose the consistency checking method for components, based on domain-specific semantics, which is self-adaptive to the modification of domain constraints. The proposed methods will be implemented into several embedded system modeling tools. The case studies in the application domains like the train control systems will also be done, to verify the generality and usability of the proposed methods.

构件化建模技术被广泛应用于嵌入式系统的设计和开发。为确保嵌入式系统构件化建模的正确性，检查构件之间连接是否正确至关重要。随着构件模型的不断增大，构件之间的连接交互增多，正确性检查越来越困难。常规的语义检查基于类型系统实现，能够判定数据类型是否匹配，却难以检测更为丰富的领域语义约束，不能满足嵌入式系统构件模型对正确性的严格要求。本项目研究能够一致解决构件模型连接许可、单位、含义、错位等多种错误的领域语义检查方法。提出基于本体的领域约束描述语言，一致严格的描述各种领域约束；提出领域语义自动标注方法，建立构件与领域语义的有效映射；提出基于领域语义的构件模型一致性检查方法，能够自适应领域约束的变动。研究成果将针对如列车控制等应用领域，在多种嵌入式系统建模语言工具中进行实例验证，以检验本研究方法的通用性和有效性。

本项目围绕面向领域特定语义的嵌入式系统构件模型语义检查方法开展研究，以便在静态检查阶段，统一检查与领域语义相关的连接许可、单位错误、含义混淆、连接错位等问题，保证构件模型的正确性。在领域约束描述语言方面，针对静态规则描述，提出了结构化自然语言语言SNL，具有表达能力强、易用、形式化等特征，并研究了基于SNL的规则库一致性和完备性检查算法。在面向构件模型的领域语义标注和推理方面，建立了一套基于概念格的领域语义类型系统，基于约束求解器和描述逻辑推理进行语义类型兼容性检查和领域规则检查。在面向嵌入式系统的构件模型语义检查方面，针对在基于可调度性规则的嵌入式系统体系结构分析、基于领域规则的嵌入式系统中断程序建模和正确性检查以及领域规则在同步异步融合建模和模型检查方面开展了研究工作。实现了领域知识建模工具和构件模型通用语义检查工具，并集成到Ptolemy II和Tsmart可信建模验证工具集中，扩展了两类工具的语义类型检查、连接关系检查、包含关系检查等检查能力。