Software systems are becoming complex and dynamic with the passage of time and to provide better fault tolerance and resource management they need to have the ability of self-adaptation. Software agents are expected to work autonomously and deal with unfamiliar situations astutely. Achieving cent percent test case coverage for these agents has always been a problem due to the limited resources. Also a high degree of dependability is expected from autonomous software agents. Multi-agent systems deployed in dynamic and unpredictable environment needs to have the ability of self-adaptation, making them adaptable to the failures. These systems have emerged as a useful technique to model real-time systems and these real-time multi-agent systems by their nature have temporal constraints. Though real-time multi-agent systems have been formally modelled in the past but self-adaptive real-time multi-agent systems are yet to be addressed. State of the art encourage the use of MAPE-K feedback loop for the provision of self-adaptation in any system. Hence there is a dire need of formal vocabulary that can be used for the conceptual design of any real-time multi-agent system with self-adaptation. In this work we proposed a framework SMARTS (Self-adaptive Multi-Agent Real-Time Systems) for the formal modelling of selfadaptive real-time multi-agent systems. Our framework integrates reflection perspective and unification with distribution perspective into the SIMBA (SIstema Multiagente Basado en ARTIS) agent architecture. For a precise semantic description of the constructs of our framework, we used Timed Communicating Object-Z (TCOZ) language. The core functionality of the system is depicted using managed system and self-adaptive unit. The self-adaptive functionality is provided by using a predefined interfaces based on Monitor, Analyze, Plan and Execute phases of the MAPE-K feedback loop. The managed system comprises the ARTIS agents, which are designed to work in hard real-time environment. In SMARTS the non-terminating behavior of the ARTIS agent is represented using active class concept of TCOZ. For communication between active processes, channel communication mechanism of TCOZ is utilized. We elaborate the application of the SMARTS framework using a trivial case-study of Traffic Management System for real-time congestion control. We ensure the correctness of the system by formally specifying and verifying the actions of the communicating real-time agents in Timed-Arc Petri-Nets as they are visually more expressive than Linear Temporal Logic (LTL) and Computational Tree Logic (CTL). The traffic models are verified using Timed Computational Tree Logic (TCTL) via translations into timed automata. The TAPAAL model checker is used for the formal verification. The simulation results show the computation trees of the traffic models, trace of the satisfied properties, count of the transitions triggered and places visited during the verification process. This formal verification of real-time self-adaptive multi-agent systems will enhance the confidence and expressibility to address the correctness of such systems.