A methodological approach to the formal specification of real-time systems by transformation of UML-RT design models

By following a methodological approach, introduced in a previous work, a correct system specification in terms of CSP+T process algebra is systematically obtained from the UML-RT model of a real-time software system. Among other contributions, this article aims at integrating collaboration diagrams into our approach to facilitate the specification of capsules in UML-RT design models. Thus, an improved systematic transformation procedure for deriving a correct and complete formal system specification of real-time systems is established here. Temporal requirements integration in the design and system specification stages of a real-time system is also addressed, so that the approach now opens up the possibility of carrying out scheduling and dependability analysis at the design phase of the system development life cycle for hard real-time systems. The article also discusses a practical application to present a systematic transformation from a UML-RT model of a well known manufacturing-industry paradigmatic case, the “Production Cell”.