RSDS, a Subset of UML with Precise Semantics
Kevin Lano, David Clark, Kelly Androutsopoulos · L objet · 2003
In this paper we describe the semantic foundation of a subset, RSDS, of the UML notation. This subset is specifically intended to support reactive system specification, and has a formal semantics expressed in temporal logic. We define this semantics, and use the semantics to justify RSDS techniques for modular decomposition and verification of reactive systems, including a structure-preserving translation to SMV.