Due to rapidly increasing system complexity, shortening time-to-market,
and growing demand for hard real-time systems, formal methods are becoming
indispensable in the synthesis of embedded systems, which must satisfy
stringent temporal, memory, and environment constraints.
There is a general lack of practical formal
methods that can synthesize complex embedded real-time software
(ERTS). In this work, a formal method based on Time
Free-Choice Petri Nets (TFCPN) is proposed for ERTS synthesis.
The synthesis method employs quasi-static data
scheduling for satisfying limited embedded memory requirements
and uses dynamic real-time scheduling for satisfying hard
real-time constraints. Software code is then generated from a set
of quasi-statically and dynamically scheduled TFCPNs. Finally,
an application example is given to illustrate the feasibility of
the proposed TFCPN-based formal method for ERTS synthesis.
