Published September 1, 2008
| Version v1
Publication
Open
On the Use of Real-Time Maude for Architecture Description and Verification: A Case Study
- 1. Centre d'Etudes et De Recherche en Informatique et Communications
- 2. Conservatoire National des Arts et Métiers
Description
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.
Translated Descriptions
⚠️
This is an automatic machine translation with an accuracy of 90-95%
Translated Description (Arabic)
مود في الوقت الحقيقي هي لغة منطقية قابلة للتنفيذ لإعادة الكتابة مناسبة بشكل خاص لمواصفات أنظمة الوقت الحقيقي المفتوحة والموزعة والموجهة للكائنات. في هذه الورقة، نستكشف إمكانية استخدام مود في الوقت الحقيقي كتدوين رسمي لوصف بنية البرمجيات والتحقق من الأنظمة في الوقت الحقيقي. يتكون نموذج النظام من نوعين من الأوصاف: ثابت وديناميكي. يتكون الوصف الثابت من تحديد العناصر المختلفة التي تشكل البنية، في حين أن الوصف الديناميكي هو تعريف القواعد التي تحكم سلوك النظام من حيث الإجراءات المحتملة المسموح بها. يتم تطوير المراسلات بين مفاهيم بنية البرمجيات ومفاهيم مود في الوقت الحقيقي لهذا الغرض. يتم تحقيق الخطوة نحو التحقق من بنية النظام من خلال تطبيق تقنيات محاكاة وتحليل مود في الوقت الحقيقي على النموذج الموصوف والخصائص التي يجب استيفاؤها. يتم استخدام مثال لتوضيح اقتراحنا ومقارنته بلغات وصف الهندسة المعمارية الأخرى.Translated Description (French)
Maude temps réel est un langage logique de réécriture exécutable particulièrement bien adapté à la spécification de systèmes temps réel ouverts et distribués orientés objet. Dans cet article, nous explorons la possibilité d'utiliser Maude temps réel comme notation formelle pour la description de l'architecture logicielle et la vérification des systèmes temps réel. Le modèle du système est composé de deux types de descriptions : statique et dynamique. La description statique consiste à identifier les différents éléments composant l'architecture, tandis que la description dynamique est la définition des règles régissant le comportement du système en termes d'actions possibles autorisées. La correspondance entre les concepts d'architecture logicielle et les concepts Maude temps réel est développée à cet effet. L'étape vers la vérification de l'architecture du système est réalisée en appliquant des techniques de simulation et d'analyse Maude temps réel au modèle décrit et aux propriétés qui doivent être satisfaites. Un exemple est utilisé pour illustrer notre proposition et la comparer avec d'autres langages de description d'architecture.Translated Description (Spanish)
Real-Time Maude es un lenguaje lógico de reescritura ejecutable especialmente adecuado para la especificación de sistemas en tiempo real abiertos y distribuidos orientados a objetos. En este artículo exploramos la posibilidad de utilizar Real-Time Maude como notación formal para la descripción de la arquitectura de software y la verificación de sistemas en tiempo real. El modelo de sistema se compone de dos tipos de descripciones: estática y dinámica. La descripción estática consiste en identificar los diferentes elementos que componen la arquitectura, mientras que la descripción dinámica es la definición de las reglas que rigen el comportamiento del sistema en términos de las posibles acciones permitidas. La correspondencia entre los conceptos de arquitectura de software y los conceptos de Real-Time Maude se desarrollan para este propósito. El paso hacia la verificación de la arquitectura del sistema se realiza aplicando técnicas de simulación y análisis de Maude en tiempo real al modelo descrito y las propiedades que deben cumplirse. Se utiliza un ejemplo para ilustrar nuestra propuesta y compararla con otros lenguajes de descripción de arquitectura.Files
305_Jerad.pdf.pdf
Files
(353.2 kB)
| Name | Size | Download all |
|---|---|---|
|
md5:fb1bcb456cb2bbe81d847679d3270811
|
353.2 kB | Preview Download |
Additional details
Additional titles
- Translated title (Arabic)
- حول استخدام مود في الوقت الحقيقي لوصف الهندسة المعمارية والتحقق منها: دراسة حالة
- Translated title (French)
- Sur l'utilisation de la maude en temps réel pour la description et la vérification de l'architecture : une étude de cas
- Translated title (Spanish)
- Sobre el uso de Maude en tiempo real para la descripción y verificación de la arquitectura: un estudio de caso
Identifiers
- Other
- https://openalex.org/W123498104
- DOI
- 10.14236/ewic/vocs2008.26
References
- https://openalex.org/W1482234031
- https://openalex.org/W1575698838
- https://openalex.org/W1584502955
- https://openalex.org/W1595206261
- https://openalex.org/W1687508979
- https://openalex.org/W1976195354
- https://openalex.org/W1979754763
- https://openalex.org/W2091567516
- https://openalex.org/W2098979034
- https://openalex.org/W2110553552
- https://openalex.org/W2127595607
- https://openalex.org/W2162366870
- https://openalex.org/W2526279767
- https://openalex.org/W2554044770
- https://openalex.org/W2762588455