An approach to combining UML and TLA+ in software specification

Graphical software specifications offer intuitive, accessible overviews of complex systems, while formal notations provide precision, thoroughness, and formal verification of the model. The Unified Modeling Language (UML) is a widely-used graphical notation, while the Temporal Logic of Actions (TLA+) is a novel formal notation for specifying the valid states of a system. The approach proposed in this paper is to create a combined set of interrelated UML and TLA+ specifications. This study uses both UML and TLA+ to model a cruise control system, producing a variety of UML and TLA+ artifacts. Formal verification of the TLA+ specification provides greater confidence in the related UML artifacts, and the UML graphics help to elucidate the TLA+ specification. Several novel results emerge from this case study, including a combined modeling approach of the two notations, correspondences between UML use cases and TLA+ actions, and the use of TLA+ notation in UML statecharts.