The context of this work is related to embedded hard real-time systems development, more specifically, in the software generation phase. Embedded software has become much harder to design caused by the diversity of requirements and high complexity. 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. However, the dispatcher and timer interrupt handler overheads are often neglect in software synthesis research. This paper provides a formal approach for system?s modeling, and such model is adopted for synthesizing a timely and predictable scheduled code taking into account dispatcher and interrupt handler overheads.