Analyzing Real-Time Event-Driven Programs

Embedded real-time systems are typically programmed in low-level languages which provide support for event-driven task processing and real-time interrupts. We show that the model checking problem for real-time event-driven Boolean programs for safety properties is undecidable. In contrast, the model checking problem is decidable for languages such as Giotto which statically limit the creation of tasks. This gives a technical reason (static analyzability) to prefer higher-level programming models for real-time programming, in addition to the usual readability and maintainability arguments.

• Type: Conference
• Year: 2009
• Where: FORMATS
• Authors: Pierre Ganty, Rupak Majumdar
• Keywords: Event-driven Task Processing, Formal Methods, FORMATS 2009, Model Checking Problem, Real-time