|
 
|
[JBG08] On the use of real-time Maude for architecture description and verification : a case study
Conférence Internationale avec comité de lecture : 1st International Academic Conference on Visions of Computer Science, London, UK, January 2008, pp.305-317, Series eWiC Series,
motcle:
Résumé:
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.
For further information, please visit this web site.
For further information, please visit this web site.
BibTeX
| @inproceedings { | |||
| JBG08, | |||
| title | = | "{On the use of real-time Maude for architecture description and verification : a case study}", | |
| author | = | " C. Jerad and K. Barkaoui and A. Grissa-Touzi ", | |
| booktitle | = | "{1st International Academic Conference on Visions of Computer Science, London, UK}", | |
| year | = | 2008, | |
| month | = | "January", | |
| series | = | "eWiC Series", | |
| pages | = | "305-317", | |
| } | |||
