UCLA

With the increasing power of computers and advances in constraint solving technologies, formal and semi-formal verification have received great attentions on many applications. Formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property. These verification techniques have wide range of applications in real life. This dissertation describes the applications of formal and semi-formal verification in four parts. The first part of the dissertation focuses on software testing. For software testing, symbolic/concolic testing reasons about data symbolically but enumerates program paths. The existing concolic technique enumerates paths sequentially, leading to poor branch coverage in limited time. We improve concolic testing by bounded model checking. During concolic testing, we identify program regions that can be encoded by BMC on the fly so that program paths within these regions are checked simultaneously. We have implemented the new algorithm on top of KLEE and called the new tool Llsplat. We have compared Llsplat with KLEE using 10 programs from the Windows NT Drivers Simplified and 88 programs from the GNU Coreutils benchmark sets. With 3600 second testing time for each program, Llsplat provides on average 13% relative branch coverage improvement on all 10 programs in the Windows drivers set, and on average 16% relative branch coverage improvement on 80 out of 88 programs in the GNU Coreutils set.

The second part of the dissertation implements symbolic/concolic testing methods onto an embedded platform. With the more extensive use and of higher demand of the embedded systems, reliability of the embedded software becomes a critical issue. Thus it is important to design a test harness that can test embedded software on the real platform or hardware in the loop framework comprehensively and systematically. We present our design prototype Codecomb. Codecomb implements symbolic/concolic execution that is able to achieve high branch coverage to generated test cases. It mainly exploits client/server architecture to achieve the isolation of testing tools and program under test such that complex computing job is performed in the server side. Experimental results show that Codecomb can detect program deficiency automatically on the embedded platform, and precisely locate errors such as buffer overflow, memory leak in a running program.

The third part of the dissertation applies formal and semi-methods to high-level synthesis (HLS) for VLSI. Verifying functional equivalence of high-level synthesis with formal methods ensures the correctness of the transformation flow. Current verification work widely uses static analysis such as model checking, while a pure dynamic execution flow is missing. In this part, we propose a functional verification flow for HLS utilizing symbolic execution on both C and Verilog directly. Specifically, on behavior C level we collect program traces via symbolic

execution. As for Verilog level, we first generate a circuit satisfiability modulo theory (SMT) representation. Then we propose a light-weight pure symbolic execution framework to collect Verilog’s on-the-fly time invariant version-based traces. To alleviate the scalability issue, we develop an operation abstraction method using SMT solvers to match potential C and Verilog traces. Extensive experiments on circuits from numerical computing and Chstone benchmark verify the validity and effectiveness of the flow.

The last part of the dissertation investigates the applications on Energy Internet. Energy Router based system is a crucial part in the energy transmission and management under the circumstance of Energy Internet for green cities. During its design process, a sound formal verification and a performance monitoring scheme are needed to check its reliability and meaningful quantitative properties. In this chapter, we provide formal verification solutions for ER based system by proposing a continuous-time Markov chain model describing the architecture of ER based system. To verify real world function of the ER based system, we choose electricity trading to propose a Markov decision process model running on an ER subsystem to describe the trading behaviour. To monitor the system performance, we project the energy scheduling process in ER based system, and then implemented this scheduling process on top of cloud computing experiment tool. Finally, we perform extensive experiment evaluations to investigate the system reliability properties, quantitative properties, and scheduling behaviours. The experiment verifies the effectiveness of the proposed models and the monitoring scheme.