扩展SysML活动图的嵌入式系统设计安全性验证方法实证研究

在能源和交通等领域的复杂嵌入式系统设计中，确保安全性是至关重要的研究课题。本文针对这一挑战，提出了结合MARTE（Modelica for Automation and Robotics in Europe）语义信息的扩展SysML活动图模型。SysML是一种广泛应用于系统建模的标准化语言，而MARTE则专注于工业自动化和机器人系统的模型化，特别强调了非功能性属性，如安全性。 作者团队，由黄传林、黄志球、胡军、徐丙凤和曲长亮等专家组成，他们在软件工程、形式化验证和嵌入式软件建模等领域具有深厚背景。他们研究的核心是利用扩展SysML活动图来设计安全关键应用的嵌入式系统动态行为，并通过模型转换的方法进行系统设计安全性特征的正式分析和验证。 首先，他们构建了一个元模型，将SysML活动图与MARTE的非功能性质建模语义相结合，明确了两者间的语义映射规则，以便于理解模型之间的关系。然后，他们将时间自动机的概念引入，通过建立从时间自动机模型描述到UPPAAL（Unmanned Platform Performance Analysis Language）工具输入格式的语法转换方法，使得模型可以直接转化为工具支持的验证形式。 为了实现这个过程，他们设计了一个基于AMMA（Advanced Modeling and Multi-Agent Methodologies for Applications）平台的模型转换与验证框架。这个框架允许用户高效地将扩展SysML活动图转换为可执行的安全性验证模型，并在实际应用中，例如高铁控制系统设计，进行实例化的安全性验证。 通过这种方法，研究人员能够更系统地评估嵌入式系统的安全性，提高设计的可靠性和效率。整个研究不仅关注理论模型构建，还关注实际应用的落地，体现了理论与实践相结合的研究策略。这篇论文的成果对于嵌入式系统设计者和安全研究人员来说，提供了宝贵的方法论参考。