可组合嵌入式软件建模与验证技术研究综述

可组合嵌入式软件以构件开发技术为基础，研究嵌入式构件的建模、组合性质、构件间组合机制以及组合验证等理论、方法和技术.从组合理论、建模与验证技术这3个方面对可组合嵌入式软件的研究现状进行调研分析.组合理论研究给出构件可组合性的乐观定义和悲观定义，从组合操作、组合规则两个方面定义构件间的组合机制.针对嵌入式构件的特点，着重调研了非功能特性和异构构件的建模与组合技术，分析了非功能特性约束、面向多特性的模型等方法.分析了基于契约的验证、基于不变量的验证、基于模型检查的验证等多种嵌入式软件组合验证技术.最后，探讨了需要进一步研究的问题.

Survey on Modeling and Verification Techniques of Composable Embedded Software

Based on CBSE (component-based software engineering), this research on composable embedded software investigates the theory, methods and technologies for modeling and verification of embedded components. The paper surveyes the state-of-the-art research and practices on composable embedded system from three perspectives: composite theory, modeling, and verification techniques. It introduces the optimistic and pessimistic definitions of component compatibility, and composition mechanisms including operations and rules. In modeling techniques, the paper particularly addresses the issues of composition of non-functional attributes and heterougeneous components, which are important to embedded components design and verification. It analyzes non-functional attribute constraints and multi-attributes oriented model. The paper also investigates three typical verification techniques of component composition including contract-based, invariants-based, and model checking techniques. It discusses future works in the end.