We observe that object-oriented (OO) formalisms and specification languages are popular and obviously useful, and, in particular, that they are increasingly used even for systems that change over time. At the same time, however, the system specification is not precise enough in these approaches. This thesis presents a formal approach to modelling OO dynamic systems using a logic-based framework. The UML which is an OO standard language, and the Statecharts formalism which is a leading approach to modelling dynamic systems, have been formalized in the framework. In addition, formal reasoning from the system-in-run perspective has been put forward, focusing on business goals. Business goals, an emerging issue within systems engineering, are reasoned with as a systematic way to check whether the goals are achieved or not in real business activities, and to cope with the situation where the goals are violated.