Embedded Software Verification Using Symbolic Execution and Uninterpreted Functions

Symbolic simulation and uninterpreted functions have long been staple techniques for formal hardware verification. In recent years, we have adapted these techniques for the automatic, formal verification of low-level embedded software—specifically, checking the equivalence of different versions of assembly language programs. Our approach, though limited in scalability, has proven particularly promising for the intricate code optimizations and complex architectures typical of high-performance embedded software, such as for DSPs and VLIW processors. Indeed, one of our key findings was how easy it was to create or retarget our verification tools to different, even very complex, machines. The resulting tools automatically verified or found previously unknown bugs in several small sequences of industrial and published example code. This paper provides an introduction to these techniques and a review of our results.     

采用随机Petri网的嵌入式机载软件可靠性检测

针对嵌入式机载软件设计中存在的典型缺陷问题，结合嵌入式机载软件任务调度特性，提出采用随机Petri网对嵌入式机载软件设计进行仿真验证的可靠性检测方法，以提高嵌入式机载软件设计的可靠性。该方法采用随机Petri网对嵌入式机载软件系统行为建模，并给出典型缺陷的检测策略和判定准则，然后通过对Petri网模型进行仿真验证，检测系统是否存在此类设计缺陷；并给出了软件设计的运行流程的仿真验证算法，以支持对相应设计的可靠性检测。通过与其他可靠性检测方法的比较，表明了该方法的有效性。     

Design verification in model-based?��-controller development using an abstract component

Component-based software development is a promising approach for controlling the complexity and quality of software systems. Nevertheless, recent advances in quality control techniques do not seem to keep up with the growing complexity of embedded software; embedded systems often consist of dozens to hundreds of software/hardware components that exhibit complex interaction behavior. Unanticipated quality defects in a component can be a major source of system failure. To address this issue, this paper suggests a design verification approach integrated into the model-driven, component-based development methodology Marmot. The notion of abstract components—the basic building blocks of Marmot—helps to lift the level of abstraction, facilitates high-level reuse, and reduces verification complexity by localizing verification problems between abstract components before refinement and after refinement. This enables the identification of unanticipated design errors in the early stages of development. This work introduces the Marmot methodology, presents a design verification approach in Marmot, and demonstrates its application on the development of a μ-controller-based abstraction of a car mirror control system. An application on TinyOS shows that the approach helps to reuse models as well as their verification results in the development process.     

FPGA的验证平台及有效的SoC验证方法

设计了一种基于FPGA的验证平台及有效的SoC验证方法,介绍了此FPGA验证软硬件平台及软硬件协同验证架构,讨论和分析了利用FPGA软硬件协同系统验证SoC系统的过程和方法.利用此软硬件协同验证技术方法,验证了SoC系统、DSP指令、硬件IP等.实验证明,此FPGA验证平台能够验证SoC设计,提高了设计效率.     

Formal hardware verification methods: A survey

Growing advances in VLSI technology have led to an increased level of complexity in current hardware systems. Late detection of design errors typically results in higher costs due to the associated time delay as well as loss of production. Thus it is important that hardware designs be free of errors. Formal verification has become an increasingly important technique towards establishing the correctness of hardware designs. In this article we survey the research that has been done in this area, with an emphasis on more recent trends. We present a classification framework for the various methods, based on the forms of the specification, the implementation, and the proff method. This framework enables us to better highlight the relationships and interactions between seemingly different approaches.     

构件化嵌入式软件设计模型非功能性质验证的工具实现

嵌入式软件的非功能性质是系统高可靠性的重要构成部分.传统的嵌入式软件可靠性保障技术主要关注于系统开发后期,缺乏有效工具对系统设计的非功能性质进行分析与验证.对基于接口自动机模型的构件化嵌入式软件设计验证原型工具T-CBESD(Tool for Component-based Embedded Software Designs)进行了资源及能耗等非功能性质验证功能的扩展设计与实现,包括:资源接口自动机和能耗接口自动机模型的输入输出接口设计、UML顺序图模型的预处理、带非功能语义信息的组合系统状态空间数据结构的设计、非实时资源使用性质与实时相关能量消耗特征验证算法的实现,以及一个通信构件组合系统的实例应用分析.     

Managing the verification trajectory

In this paper we take a closer look at the automated analysis of designs, in particular of verification by model checking. Model checking tools are increasingly being used for the verification of real-life systems in an industrial context. In addition to ongoing research aimed at curbing the complexity of dealing with the inherent state space explosion problem – which allows us to apply these techniques to ever larger systems – attention must now also be paid to the methodology of model checking, to decide how to use these techniques to their best advantage. Model checking “in the large” causes a substantial proliferation of interrelated models and model checking sessions that must be carefully managed in order to control the overall verification process. We show that in order to do this well both notational and tool support are required. We discuss the use of software configuration management techniques and tools to manage and control the verification trajectory. We present Xspin/Project, an extension to Xspin, which automatically controls and manages the validation trajectory when using the model checker Spin. Published online: 18 June 2002     

一种基于监测的嵌入式系统设计技术

提出一种嵌入式系统软硬件协同设计方法，它以数据流图为系统模型对嵌入式系统的功能和性能需求进行描述，并通过一种特定的实现结构，使得设计者可以借助快速样机平台和事件驱动式监测技术来精确测定目标系统对系统模型的实现状况，从而使得软硬件协同设计过程特别是系统优化和性能验证能在精确、可靠的测试数据基础上进行．同目前通常使用的以软硬件部件性能估算为基础的软硬件协同设计方法相比，这种以测试为基础的设计技术更能确保设计结果的合理．     

嵌入式系统虚拟开发环境的设计与实现

在嵌入式系统虚拟开发环境中为软件与硬件分别设计了ＥＳＤＬ语言和ＥＨＤＬ语言．ＥＳＤＬ是ＡＮＳＩＣ的超集,它为嵌入式编程增加了一些数据类型．ＥＨＤＬ是一种硬件描述语言．开发人员可以利用由嵌入式软件调度器和嵌入式硬件模拟器组成的协同验证环境调试嵌入式系统．利用这个虚拟的集成环境,软件开发人员可以在设计初期发现与硬件相关的错误,硬件开发人员可以获得系统功能的真实描述．硬件、软件的设计错误可以在系统制造之     

Codesign of embedded systems: status and trends

Ever increasing embedded system design complexity combined with a very tight time-to-market window has revolutionized the embedded-system design process. The concurrent design of hardware and software has displaced traditional sequential design. Further, hardware and software design now begins before the system architecture (or even the specification) is finalised. System architects, customers, and marketing departments develop requirement definitions and system specifications together. System architects define a system architecture consisting of cooperating system functions that form the basis of concurrent hardware and software design. Interface design requires the participation of both hardware and software developers. The next step integrates and tests hardware and software-this phase consists of many individual steps. Reusing components taken from previous designs or acquired from outside the design group is a main design goal to improve productivity and reduce design risk. It is argued that new methodologies and AD tools support an integrated hardware software codesign process     

基于安全风险的RTL级硬件木马验证研究

信息时代使得信息安全变得日益重要。攻击方为了获取想要的信息,除了使用软件方面的手段,如病毒、蠕虫、软件木马等,也使用硬件手段来威胁设备、系统和数据的安全,如在芯片中植入硬件木马等。如果将硬件木马植入信息处理的核心--处理器,那将风险更高、危害更大。然而,硬件木马位于信息系统底层核心的层面,难以被检测和发现出来。硬件木马是国内外学术界研究的热点课题,尤其是在设计阶段结合源代码的硬件木马检测问题,是新问题,也是有实际需要的问题。在上述背景下,围绕源代码中硬件木马的检测和验证展开了研究。基于硬件木马危害结果属性,在学术上提出基于安全风险的模型和验证规则,给出相应的描述形式,从理论上说明安全验证规则在减少验证盲目性、缩小可疑代码范围、提高评估效率的作用,实验表明,基于安全风险规则的验证,可以避免验证的盲目性和测试空间向量膨胀的问题,有效验证疑似硬件木马的存在和危害,对源代码安全评估是有一定效果的。     

AFDX-ES SoC验证平台的构建与实现

以SoC软硬件协同设计方法学及验证方法学为指导,系统介绍了以ARM9为核心的AFDX-ES SoC设计过程中,软硬件协同设计和验证平台的构建过程及具体实施。应用实践表明该平台具有良好的实用价值。     

Combining Software and Hardware Verification Techniques

Combining verification methods developed separately for software and hardware is motivated by the industry's need for a technology that would make formal verification of realistic software/hardware co-designs practical. We focus on techniques that have proved successful in each of the two domains: BDD-based symbolic model checking for hardware verification and partial order reduction for the verification of concurrent software programs. In this paper, we first suggest a modification of partial order reduction, allowing its combination with any BDD-based verification tool, and then describe a co-verification methodology developed using these techniques jointly. Our experimental results demonstrate the efficiency of this combined verification technique, and suggest that for moderate–size systems the method is ready for industrial application.     

A Formal Verification Environment for Railway Signaling System Design

A fundamental problem in the design and development of embedded control systems is the verification of safety requirements. Formal methods, offering a mathematical way to specify and analyze the behavior of a system, together with the related support tools can successfully be applied in the formal proof that a system is safe. However, the complexity of real systems is such that automated tools often fail to formally validate such systems.This paper outlines an experience on formal specification and verification carried out in a pilot project aiming at the validation of a railway computer based interlocking system. Both the specification and the verification phases were carried out in the JACK (Just Another Concurrency Kit) integrated environment. The formal specification of the system was done by means of process algebra terms. The formal verification of the safety requirements was done first by giving a logical specification of such safety requirements, and then by means of model checking algorithms. Abstraction techniques were defined to make the problem of safety requirements validation tractable by the JACK environment.     

超大规模集成电路可调试性设计综述

随着硬件复杂度的不断提高和并行软件调试的需求不断增长,可调试性设计已经成为集成电路设计中的重要内容.一方面,仅靠传统的硅前验证已经无法保证现代超大规模复杂集成电路设计验证的质量,因此作为硅后验证重要支撑技术的可调试性设计日渐成为大规模集成电路设计领域的研究热点.另一方面,并行程序的调试非常困难,很多细微的bug无法直接用传统的单步、断点等方法进行调试,如果没有专门的硬件支持,需要耗费极大的人力和物力.全面分析了现有的可调试性设计,在此基础上归纳总结了可调试性设计技术的主要研究方向并介绍了各个方向的研究进展,深入探讨了可调试性结构设计研究中的热点问题及其产生根源,给出了可调试性结构设计领域的发展趋势.     

Efficient verification of railway infrastructure designs against standard regulations

In designing safety-critical infrastructures s.a. railway systems, engineers often have to deal with complex and large-scale designs. Formal methods can play an important role in helping automate various tasks. For railway designs formal methods have mainly been used to verify the safety of so-called interlockings through model checking, which deals with state change and rather complex properties, usually incurring considerable computational burden (e.g., the state-space explosion problem). In contrast, we focus on static infrastructure models, and are interested in checking requirements coming from design guidelines and regulations, as usually given by railway authorities or safety certification bodies. Our goal is to automate the tedious manual work that railway engineers do when ensuring compliance with regulations, through using software that is fast enough to do verification on-the-fly, thus being able to be included in the railway design tools, much like a compiler in an IDE. In consequence, this paper describes the integration into the railway design process of formal methods for automatically extracting railway models from the CAD railway designs and for describing relevant technical regulations and expert knowledge as properties to be checked on the models. We employ a variant of Datalog and use the standardized “railway markup language” railML as basis and exchange format for the formalization. We developed a prototype tool and integrated it in industrial railway CAD software, developed under the name RailCOMPLETE^®. This on-the-fly verification tool is a help for the engineer while doing the designs, and is not a replacement to other more heavy-weight software like for doing interlocking verification or capacity analysis. Our tool, through the export into railML, can be easily integrated with these other tools. We apply our tool chain in a Norwegian railway project, the upgrade of the Arna railway station.     

Introductory Paper

In today’s competitive market designing of digital systems (hardware as well as software) faces tremendous challenges. In fact, notwithstanding an ever decreasing project budget, time to market and product lifetime, designers are faced with an ever increasing system complexity and customer expected quality. The above situation calls for better and better formal verification techniques at all steps of the design flow. This special issue is devoted to publishing revised versions of contributions first presented at the 12th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME) held 21–24 October 2003 in L’Aquila, Italy. Authors of well regarded papers from CHARME’03 were invited to submit to this special issue. All papers included here have been suitably extended and have undergone an independent round of reviewing.     

Object-based hardware/software component interconnection model for interface design in system-on-a-chip circuits

The design of system-on-a-chip (SoC) circuits requires the integration of complex hardware/software components that are customized to efficiently execute a specific application. Nowadays, these components include many different embedded processors executing concurrent software tasks. In this paper, we present an object-based component interconnection model to represent both hardware and software components within a system architecture in a very high level of abstraction. This model is used in a design flow for automatic generation of hardware/software interfaces for SoC circuits. Design tools for automatic generation of embedded operating systems, hardware interfaces and associated device drivers are presented and evaluated using the results obtained with a VDSL application.