An Approach To The Code Framework Generation And Analysis Of Interrupt-driven System

An interrupt-drived system is a real-time control system consisting of system tasks and interrupt handlers.Such systems required high safety and reliability.Any minor errors could cause casualties or consequences of heavy losses.The occurrence of an interrpt event is uncertain in the run-time of the interrupt drive systems.Some of the design errors in such systems can only be revealed by a certain sequence of interruptions.It has significant difficulties in revealing,locating and reproducing these errors.Model Checking as a formal method could better solve the problem of reproducing and locating errors in interrupt-driven systems.Formal models are used to modelling the behaviors of software systems.These formal models can be quickly analyzed and verified whether the interrupt drive system design contains design errors or not.To efficiently apply Model Checking method to interrupt-driven systems,two issues must be considered.First,how to efficiently extract formal models from interrupt-driven systems.Second,it is necessary to consider how to ensure the consistency between interrupt-drived systems and system models.Another way to improve the efficiency of development of interrupt-driven systems is to generate code(framework)for interrupt-driven systems from formal models.This paper attempts to address the above issues by proposing a code generation and analysis approach for interrupt-driven systems.The approach mainly includes the following works:1.A method architecture composed of the code-framework-generation technique for interrupt-driven systems,and the analysis method,which includes the characteristic attributes of the interrupt-driven system,the design of interrupt-driven system model,the design of the overall code framework generation and validation process architecture.2.A technique to transform formal models into the code framework of interrupt-driven systems.The elements of the model are transformed into code framework and annotations.Programers need only fulfill the details of interrupt/task-handlers.This technique can improve the efficiency of development,and ensure the structural consistency between models and system implementations.3.A technique to extract formal models from the existing source code of interrupt-driven systems.Based on the control-flow information and some commonly-used patterns,this technique can find interrupt-handlers from the source code,and get a partial model.4.Two analysis techniques to get the information about worst case execution time(WCET)and shared variable access information about interrupt/task handlers.These techniques can ensure the consistency between system models and source code.5.Implementation the prototype tools described in this paper.The feasibility of the proposed method is illustrated by an example.