Formalization of UML state machines using temporal logic

The main purpose of this paper is to approach the use of formal methods in computing. In more specific terms, we use a temporal logic to formalize the most fundamental aspects of the semantics of UML state machines. We pay special attention to the dynamic aspects of the different operations associated with states and transitions, as well as the behaviour of transitions related with composite states. This, to the best of our knowledge, has not been done heretofore using temporal logic.Our formalization is based on a temporal logic that combines points, intervals, and dates. Moreover this new temporal logic is built over an innovative and simple topological semantics, which simplifies the metatheory development.