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

嵌入式系统通常用于安全关键应用，例如汽车、飞机或交通控制系统。这使得它们的正确性对于避免严重的经济损失甚至人员伤亡至关重要。然而，嵌入式系统的验证是一个挑战，主要是因为这些系统非常复杂，必须在有限的资源上运行，并且通常由深度集成的硬件(HW)和软件(SW)组件组成。为了克服这一问题，我们提出了一种支持数字软硬件系统整个设计流程的模块化验证框架，该框架结合了从正式硬件验证到软件验证再到系统验证的各种验证技术。我们的目标是系统级设计语言SystemC，它已经成为软硬件协同设计的事实标准，但严重缺乏对自动化和全面验证的支持。它的语义只是非正式定义的，验证技术是临时的和非系统的。为了实现形式上基于良好的验证流程，我们从SystemC的中间表示(IR)的正式定义(SysCIR)开始。然后，我们通过一组模块化引擎来处理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.