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
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.