A Formalization of UML Statecharts for Real-Time Software Modeling