K-based definition of Real Time Distributed Systems: from a meta-model to maude modules

Besides the increasing complexity, real time behavior and dynamic evolution are other critical challenges imposed by the RT-DS (Real Time Distributed Systems) design. Component Based Software Engineering, as well as Model Driven Engineering may offer well-suited software development methodologies to tackle these challenges. This paper proposes and explains, through a realistic application, a hybrid approach, based on the main artifacts of MDA techniques and formal methods, for specifying and thereafter analyzing RT-DS. First, we provide DySAM*, as an extension with time dependent features of DySAM (Dynamic Software Architecture Meta-model) proposed in a previous work. Then, we integrate DySAM* in K-Maude tool in order to define the operational semantics of DS that deal with temporal features. This has the advantage to make possible both, system execution and temporal properties verification, in transparent manner.