On the Use of Real-Time Maude for Architecture Description and Verification: A Case Study

Real-Time Maude is an executable rewriting logic language particularly well suited for the specification of object-oriented open and distributed real time systems. In this paper we explore the possibility of using Real-Time Maude as a formal notation for software architecture description and verification of real time systems. The system model is composed of two kinds of descriptions: static and dynamic. The static description consists in identifying the different elements composing the architecture, while the dynamic description is the definition of the rules governing the system behaviour in terms of the possible actions allowed. The correspondence between software architecture concepts and the Real-Time Maude concepts are developed for this purpose. The step towards verifying system architecture is realized by applying Real-Time Maude simulation and analysis techniques to the described model and the properties that must be satisfied. An example is used to illustrate our proposal and to compare it with other architecture description languages.