【摘要】 形式化系统验证是保证系统设计正确性的一种重要手段.如何针对复杂机电系统物理与软件相融合的特征,对系统设计的动态特征进行验证,是系统验证研究领域亟待解决的问题.针对这一问题,对系统工程标准建模语言SysML进行扩展,提出了一套形式化系统模型验证方法.首先,以计算树逻辑和基于流的功能表示为形式化基础,形成基于SysML的系统功能建模方法;然后,以混合自动机为基础,建立基于SysML的系统行为建模方法;最后,针对物理与软件子系统的不同动态特征,借助NuSMV模型校验器,以层次化方式实现系统模型的自动验证.以移动机器人系统为例,展示了复杂机电系统设计模型的自动验证过程.更多还原

【Abstract】 Formal system verification is an important method to guarantee the correctness of system design. Because of the physical-software synergetic characteristics of complex mechatronic systems, how to verify the system design from the dynamic perspective is a challenging issue in this research area. To this end, we proposed a formal system model verification method by extending SysML, which is the standard modeling language for systems engineering. Specifically, first, we combined the computational tree logic(CTL) and flow-based functional representation as the formal basis and proposed a system functional modeling method in SysML; then, we proposed a system behavioral modeling method in SysML based on hybrid automata(HA); finally, specific to the different dynamics of physical and software subsystems, we conducted the system design model verification in a layered manner by leveraging the model checker NuSMV. We used the mobile robot system as a case study to illustrate the system verification process.更多还原