RSDS, a Subset of UML with Precise Semantics
Dans cet article nous décrivons les bases sémantiques d'un sous-ensemble, RSDS, de la notation UML. Ce sous-ensemble est spécifiquement étudié pour cibler la spécification des systèmes réactifs et a une sémantique formelle exprimée en logique temporelle. Nous définissons cette sémantique et nous l'utilisons pour justifier la technique de décomposition modulaire de RSDS, la vérification de systèmes réactifs aussi bien que la traduction vers SMV.
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.
K.LANO, D.CLARK, K.ANDROUTSOPOULOS
UML, RSDS, sémantique formelle, systèmes réactifs, SMV.
UML, RSDS, Formal semantics, Reactive systems, SMV.
Anglais
|
