Model Checking Memory-Related Properties of Hardware/Software Co-designs
Model Checking Memory-Related Properties of Hardware/Software Co-designs
复制标题
模型检查硬件/软件协同设计的内存相关属性
DOI：
10.1007/978-3-642-38853-8_9
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
S. Glesner
中科院分区：
文献类型：
--
作者：
Marcel Pockrandt;Paula Herber;V. Klös;S. Glesner
记忆安全在并发硬件/软件系统中起着至关重要的作用，并且必须在任何情况下保证。尽管存在一些可以完全验证的方法可以应对硬件和软件及其相互作用，但它们都不支持指针或内存。为了克服这个问题，我们提出了一种新颖的方法，用于模型检查SystemC/TLM设计的数字HW/SW系统的内存相关属性。主要想法是使用Uppaal定时自动机对SystemC内存模型的清洁子集进行正式化。然后，我们将这个形式的内存模型嵌入了我们先前提出的从SystemC/TLM到Uppaal定时自动机的自动转换。因此，我们可以完全自动验证广泛实用应用的与内存相关的属性。我们通过验证一种工业设计的记忆安全来展示我们的方法的适用性，该工业设计可以充分利用指针和引用。
Memory safety plays a crucial role in concurrent hardware/software systems and must be guaranteed under all circumstances. Although there exist some approaches for complete verification that can cope with both hardware and software and their interplay, none of them supports pointers or memory. To overcome this problem, we present a novel approach for model checking memory-related properties of digital HW/SW systems designed in SystemC/TLM. The main idea is to formalize a clean subset of the SystemC memory model using Uppaal timed automata. Then, we embed this formal memory model into our previously proposed automatic transformation from SystemC/TLM to Uppaal timed automata. With that, we can fully automatically verify memory-related properties of a wide range of practical applications. We show the applicability of our approach by verifying memory safety of an industrial design that makes ample use of pointers and call-by-reference.