iDola: Bridge Modeling to Verification and Implementation of Interrupt-Driven Systems

In real-time embedded applications, interrupt-driven systems are widely adopted due to strict timing requirements. However, development of interrupt-driven systems is time-consuming and error-prone. To conveniently ensure a trustworthy system design and implementation is a challenging problem, especially in complex applications. In this paper, we present a novel domain-specific language called iDola to model interrupt-driven systems declaratively and concisely. A major strength of iDola is the feasibility to capture complex interrupt handling mechanism in real-time operating systems and target platforms, such as delayed service and buffered processing. We also propose the formal operational semantics and code generation algorithm of iDola, so that iDola models can be transformed to timed automata for verification and loaded to generate platform-specific codes. We apply iDola on the modeling of an industrial interrupt-driven system, multifunction vehicle bus controller which runs in an embedded environment with eCos operating system. Based on iDola, the system is modeled with a dispatcher which embodies advanced interrupt handling in eCos, including buffered interrupt service routine and deferred service routine. Through transformation, the system design is verified and design bugs are detected. Code generation is also executed using the proposed algorithm. Generated codes display comparatively equal performance in the real system. We believe iDola can facilitate building a trustworthy interrupt-driven system.