Model-Driven Architecture (MDA) presents a set of layered models to separate design concerns from platform concerns. The model executability for each model element is still challenging although MDA is currently able to cope with most syntactic and transformation definition issues. Moreover, the importance of rigorous specification and verification of the system is increasing, as the embedded software is more widely used for systems closely related to our life. Thus, this paper suggests behavior modeling views characterizing Platform-Independent Model (PIM) and Platform-Specific Model (PSM) behaviors and formal and verifiable models for them. In this, the PIM behavior is given from the view of the functionality of the software in Statecharts, whereas the PSM behavior is modeled from the view of a timed and resource-constrained behavior in TRoS, an extension of Statecharts in respect of time and resource constraints. Moreover, we provide an efficient way where PIM in Statecharts is transformed into PSM in TRoS. Using our approach, PIM and PSM behavior are captured in formal semantics for rigorous analysis in terms of system behavior, and the PSM behavior in TRoS is effectively and consistently obtained from the PIM behavior in Statecharts. We present a case study, in which safety-critical software for a railway control system is developed to show the feasibility of our approach.