Embedded hard real-time software synthesis considering dispatcher overheads

Due to the increasing complexity and diversity of requirements, embedded software has become much harder to design. For instance, since several applications demand safety properties, the correctness and timeliness verification is an issue to be concerned. Usually, complex embedded real-time systems rely on specialized operating system kernels. However, operating systems may introduce significant overheads in execution time as well as in memory requirement. Software synthesis might be an alternative approach to operating systems usage, since it can generate tailored code for satisfying functional, performance, and resource constraints, and automatically generate runtime support (scheduling, resource management, communication, etc) customized for each particular specification. An often neglected situation in software synthesis research is the dispatcher and timer interrupt handler overheads. This paper provides a formal approach, based on time Petri nets, for synthesizing a timely and predictable scheduled code considering dispatcher overheads.