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

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

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.