RESCUE: Reliable Embedded System design based on Co-verification in a Unified Environment

RESCUE：统一环境中基于协同验证的可靠嵌入式系统设计

• 批准号: 234310760
• 负责人: Professorin Dr.-Ing. Paula Herber
• 金额: --
• 依托单位: Embedded Systems Group
• 依托单位国家: 德国
• 项目类别: Research Grants
• 财政年份: 2013
• 资助国家: 德国
• 起止时间: 2012-12-31 至 2020-12-31
• 项目状态: 已结题
• 来源: https://gepris.dfg.de/gepris/projekt/234310760?language=en
• 关键词: RESCUE; Reliable; Embedded; System; design

Embedded systems are often employed in safety-critical applications, for example, in cars, airplanes or traffic control systems. This makes their correctness crucial to avoid high financial losses or even human injuries or deaths. However, the verification of embedded systems is a challenge, mainly because these systems are very complex, have to run on limited resources, and typically consist of deeply integrated hardware (HW) and software (SW) components. To overcome this problem, we propose a modular verification framework that supports the whole design flow of digital HW/SW system combining a variety of verification techniques, ranging from formal hardware verification over software verification to system verification. We target the system level design language SystemC, which has become the de facto standard in HW/SW co-design, but severely lacks support for automated and comprehensive verification. Its semantics is only informally defined, and verification techniques are ad-hoc and non-systematic. To achieve a formally well-founded verification flow, We start with a formal definition of an intermediate representation (IR) for SystemC (SysCIR). Then, we process the SysCIR by a set of modular engines. First, we develop innovative slicing and abstraction engines, which significantly reduce the semantic state space. Second, we provide a set of transformation engines that target a variety of verification tools. In particular, we combine hardware, software and system verification techniques in order to cope with the different models of computation inherently intertwined in embedded HW/SW systems. Another important contribution will be a technique to automatically select and combine our slicing, abstraction, and transformation engines.

嵌入式系统通常用于安全关键应用中，例如汽车、飞机或交通控制系统。这使得它们的正确性对于避免高额经济损失甚至人员伤亡至关重要。然而，嵌入式系统的验证是一个挑战，主要是因为这些系统非常复杂，必须在有限的资源上运行，并且通常由深度集成的硬件（HW）和软件（SW）组件组成。为了克服这个问题，我们提出了一个模块化的验证框架，支持整个设计流程的数字硬件/软件系统相结合的各种验证技术，从正式的硬件验证软件验证系统验证。我们的目标是系统级设计语言SystemC，它已成为硬件/软件协同设计中事实上的标准，但严重缺乏对自动化和全面验证的支持。它的语义只是非正式定义的，验证技术是临时的和非系统的。为了实现一个正式的有根据的验证流程，我们开始与SystemC（SysCIR）的中间表示（IR）的正式定义。然后，我们处理SysCIR的一组模块化引擎。首先，我们开发了创新的切片和抽象引擎，显着减少了语义状态空间。第二，我们提供了一组转换引擎，它们针对各种验证工具。特别是，我们结合联合收割机的硬件，软件和系统验证技术，以科普固有的交织在嵌入式硬件/软件系统的计算的不同模型。另一个重要的贡献将是一种自动选择和联合收割机组合我们的切片、抽象和转换引擎的技术。

项目成果

Bit-precise formal verification of discrete-time MATLAB/Simulink Models using SMT Solving

使用 SMT 求解对离散时间 MATLAB/Simulink 模型进行位精确形式验证

• DOI: 10.1109/emsoft.2013.6658586
• 发表时间: 2013
• 期刊: 2013 Proceedings of the International Conference on Embedded Software (EMSOFT)
• 作者: Paula Herber;Robert Reicherdt;Patrick Bittner
• 通讯作者: Patrick Bittner

The RESCUE Approach - Towards Compositional Hardware/Software Co-verification

RESCUE 方法 - 实现组合硬件/软件协同验证

• DOI: 10.1109/hpcc.2014.109
• 发表时间: 2014
• 期刊: 2014 IEEE Intl Conf on High Performance Computing and Communications, 2014 IEEE 6th Intl Symp on Cyberspace Safety and Security, 2014 IEEE 11th Intl Conf on Embedded Software and Syst (HPCC,CSS,ICESS)
• 作者: Paula Herber

Bit-Precise Formal Verification for SystemC Using Satisfiability Modulo Theories Solving

使用可满足性模理论求解的 SystemC 的位精确形式验证

• DOI: 10.1007/978-3-319-90023-0_5
• 发表时间: 2015
• 作者: Lydia Jaß;Paula Herber
• 通讯作者: Paula Herber