This paper addresses the difficulty that designers of embedded software systems face when doing formal verification. Existing theories and practices in verification are powerful, but when applying formal techniques, the use of detailed mathematical model descriptions in verification greatly increase the burden on system designers; construction of such models may be time consuming and error prone. We lay the groundwork for solving this problem by providing a mapping from actor models to mathematical models suitable for verification; the conversion is automatic with minimal human intervention. Meanwhile, the interactions between the verification model and its environment can guide us in designing how the implementation model interprets the raw data from sensors and to actuators, allowing us to reuse the verification model as the basis of its implementation model. Following these strategies, the productivity of designers and the correctness of designs can be maintained simultaneously.