Formal synthesis and code generation of real-time embedded software using time-extended quasi-static scheduling

The rapid escalation in complexity of real-time embedded systems design has made embedded software an integral system part such that formal software synthesis has become an indispensable design automation technique. The current work takes one more step forward in this research direction by proposing a formal synthesis method for complex real-time embedded software. Compared to previous work, our method not only synthesizes embedded software with complex interrelated branching choices for execution within a user-given memory bound, but also tries to guarantee the satisfaction of all user-given local and global time constraints. Our proposed method called time-extended quasi-static scheduling (TEQSS) synthesizes real-time embedded software code from a set of time complex-choice Petri nets. The two most important issues in real-time embedded software, namely memory and time constraints are both elegantly and efficiently handled by TEQSS. We show the feasibility of our method through a master-slave role switch application which is a part of the Bluetooth wireless communication protocol.