Towards Modeling And Verification Of Interrupt-driven Programs

Interrupt-driven programs(IDP),as a special form of software,has been undergoing a growth of applications in real-world industrial embedded systems across various domains.In order to improve the responsiveness of the target system and thus satisfy domain-specific real-time constraints,IDP prioritizes the execution of the most urgent requests.From the practical perspective,IDP is often implemented in safety-critical systems,therefore its correctness is of the top significance.Any software defects may trigger severe system failure and further lead to a huge loss on money and human lives.However,to guarantee the safety of IDP is challenging for the following three-fold reasons.First,IDP includes special operations besides common programming patterns,such as interrupt enabling,asynchronous deferral and communication with hardware via registers.These features make accurate program analyses hard.Second,as a class of concurrent software,IDP incurs a large number of interleaving because of the non-deterministic occurrences of interrupt signals.As a result,the state space of IDP suffers from an exponential growth as the number of interrupts increases.In that case,analysis of IDP can hardly be scalable for real-world complex applications.Lastly,analysis of IDP is dependent on the characteristics of the application domain.With respect to the diversity of domains,it is desirable to specify the domain knowledge in a unified and concise manner so that the domain knowledge can be better integrated with the analysis.To sum up,checking the safety of IDP remains a research challenge in practice.In this paper,we have proposed novel techniques to model and verify IDP.To this end,we first introduced iDola,a modeling language for IDP.iDola is capable of specifying basic control flow structures,and interrupt related operations as well,including posting an asynchronous deferral,enabling and disabling interrupt signals and access to registers.Based on iDola model,we have further defined the formal and operational semantics of IDP,which determines the behavior of IDP in different contexts.Moreover,with the formal model of IDP,we have proposed a verification framework of IDP based on program sequentialization.Specifically,we transformed a concurrent IDP into a sequential one via instrumenting three types of scheduling functions,which can simulate the preemption,asynchronous scheduling and register-based communication.In further,we have defined interrupt dependency graph and its automatic generation algorithm,which enables identifying dependencies between interrupt handlers so as to reduce the state space of IDP and accelerate verification.We have implemented the aforementioned techniques in a tool prototype called Tsmart-SiRi,and applied it in a real-world industrial embedded system — Multifunction Vehicle Bus Controller(MVBC).In this case study,Tsmart-SiRi managed to guarantee the analysis accuracy by avoiding false alarms.In terms of verification performance,Tsmart-SiRi achieved an optimization from 18.84 % to67.35 % through interrupt dependency graph.The verification helped uncover three types of previously unknown bugs,resulted from preemption and register-based communication with unexpected timing.All the bugs have been reproduced and confirmed in simulation runs.