Verification Method of Safety Properties of Embedded Assembly Program by Combining SMT-Based Bounded Model Checking and Reduction of Interrupt Handler Executions

Embedded software has properties dependent on hardware (direct operation of address spaces, memory mapped I/O, interruption, etc.). Therefore, demands about the established method of formal verifications corresponding to those properties are increasing from the point of view of shorter development and high reliability. Our study aims at enabling a formal verification with Satisfiability Modulo Theories-Based Bounded Model Checking (SMT-Based BMC) of safety for embedded assembly codes. Our proposed method generates models of assembly codes in detail with the fixed-sized bit-vectors theory. The models generated by our method include interrupts, and the size of the models is reduced using Interrupt Handler Execution Reduction (IHER) technique. In this paper, we have developed the verification method of safety properties of embedded assembly program by combining SMT-Based Bounded Model Checking and Reduction of Interrupt Handler Executions. Moreover, we show the evaluation of our method by experiments using prototype model checker.

Design and Implementation of Digital Photo Frame Based on STM32F103VET6

This paper used STM32F103VET6 as the core processor, SD card to store the image file. In addition, the host controller read, write, operate and decode the image data stored in the SD card with the SPI communication mode. Then it will send the processed data to the indication controller. And finally display the photos with TFT-LCD. The function keys send interruption requests to the processor by external interrupting. With different interrupt handler, the processor can show and switch images in the digital photo frame in different ways so as to realize the various functions of the digital photo frame.

Study for Interrupt Controller S3C2410X of Embedded System

Interrupt handling in out-of-order execution processors requires complex hardware schemes to maintain the sequential state. By managing the interaction with external systems through effective use of interrupts can dramatically improve system efficiency and the use of processing resources. The actual process of determining a good handling method can be complicated, challenging and fun. Numerous actions are occurring simultaneously at a single point and these actions have to be handled fast and efficiently. The paper will provide a practical guide to designing an interrupt handler and discuss the various trade-offs between the different methods. The interrupt handling process of S3C2410X is described, normally, S3C2410X interrupt controller requests interrupt from kernel interrupt FIQ or IRQ of S3C2410X after the interrupt arbitration. The experiment purpose and experiment equipment is detailed listed. Finally, the author explored into the experiment principle and experiment procedure.