面向机器人软件模型保障案例的形式化证据生成方法

研究提出一种基于模型的方法，将形式化验证嵌入保障案例（AC）工作流，以系统化生成证据。该方法利用具有形式语义的领域建模语言RoboChart，通过预定义模板将自然语言需求自动转换为形式化断言，并编排多种验证工具结合模型检验与定理证明，验证结果自动集成为证据。案例研究展示了该方法的有效性，论文为预印本，已被Software and Systems Modeling（SoSyM）接收。