Published January 1, 2009
| Version v1
Publication
Open
Distributed CTL Model–Checking and counterexample search
- 1. Laboratoire d'Informatique de Paris-Nord
- 2. University of Sciences and Technology Houari Boumediene
- 3. Université Paris Cité
- 4. Université Sorbonne Paris Nord
- 5. Centre National de la Recherche Scientifique
Description
In this paper, we propose a distributed algorithm for CTL model-checking and a counterexample search whenever the CTL formula is not satisfied. The distributed approach is used in order to cope with the state space explosion problem. A cluster of workstations performs collaborative verification over a partitioned state space. Thus, every process involved in the distributed verification executes a labelling procedure on its own partial state space, and uses the parse tree of the CTL formula to evaluate sub-formulas and delay the synchronisations so as to minimise idle time. A counterexample search consists in a distributed construction of the tree-like corresponding to the failure executions. Some experiments have been carried out to evaluate the efficiency of this approach.
Translated Descriptions
⚠️
This is an automatic machine translation with an accuracy of 90-95%
Translated Description (Arabic)
في هذه الورقة، نقترح خوارزمية موزعة للتحقق من نموذج CTL والبحث عن مثال مضاد كلما لم يتم استيفاء صيغة CTL. يتم استخدام النهج الموزع من أجل التعامل مع مشكلة الانفجار الفضائي للدولة. تقوم مجموعة من محطات العمل بالتحقق التعاوني عبر مساحة حالة مقسمة. وبالتالي، فإن كل عملية تنطوي على التحقق الموزع تنفذ إجراء وضع العلامات على مساحة الحالة الجزئية الخاصة بها، وتستخدم شجرة التحليل لصيغة CTL لتقييم الصيغ الفرعية وتأخير المزامنة لتقليل وقت الخمول. يتكون البحث في المثال المضاد من بناء موزع للشجرة - مثل عمليات التنفيذ الفاشلة. وقد أجريت بعض التجارب لتقييم كفاءة هذا النهج.Translated Description (French)
Dans cet article, nous proposons un algorithme distribué pour la vérification du modèle CTL et une recherche de contre-exemple chaque fois que la formule CTL n'est pas satisfaite. L'approche distribuée est utilisée afin de faire face au problème d'explosion de l'espace d'état. Un cluster de postes de travail effectue une vérification collaborative sur un espace d'état partitionné. Ainsi, chaque processus impliqué dans la vérification distribuée exécute une procédure d'étiquetage sur son propre espace d'état partiel, et utilise l'arbre d'analyse de la formule CTL pour évaluer les sous-formules et retarder les synchronisations afin de minimiser le temps d'inactivité. Une recherche de contre-exemple consiste en une construction distribuée de l'arborescence correspondant aux exécutions de défaillance. Certaines expériences ont été menées pour évaluer l'efficacité de cette approche.Translated Description (Spanish)
En este artículo, proponemos un algoritmo distribuido para la verificación del modelo de CTL y una búsqueda de contraejemplo siempre que no se cumpla la fórmula de CTL. El enfoque distribuido se utiliza para hacer frente al problema de la explosión espacial estatal. Un clúster de estaciones de trabajo realiza la verificación colaborativa en un espacio de estados particionado. Por lo tanto, cada proceso involucrado en la verificación distribuida ejecuta un procedimiento de etiquetado en su propio espacio de estado parcial y utiliza el árbol de análisis de la fórmula CTL para evaluar las subfórmulas y retrasar las sincronizaciones para minimizar el tiempo de inactividad. Una búsqueda de contraejemplo consiste en una construcción distribuida del tipo árbol correspondiente a las ejecuciones de fallo. Se han llevado a cabo algunos experimentos para evaluar la eficiencia de este enfoque.Files
001_Boukala.pdf.pdf
Files
(140.4 kB)
| Name | Size | Download all |
|---|---|---|
|
md5:13d69fcf1729abd5110022a4cf329e9b
|
140.4 kB | Preview Download |
Additional details
Additional titles
- Translated title (Arabic)
- التحقق من نموذج CTL الموزع والبحث عن مثال مضاد
- Translated title (French)
- Modèle CTL distribué - Vérification et recherche de contre-exemple
- Translated title (Spanish)
- Modelo de CTL distribuido: verificación y búsqueda de contraejemplo
Identifiers
- Other
- https://openalex.org/W22348942
- DOI
- 10.14236/ewic/vecos2009.6
References
- https://openalex.org/W121054480
- https://openalex.org/W1501277483
- https://openalex.org/W1548575501
- https://openalex.org/W1559035930
- https://openalex.org/W1574520403
- https://openalex.org/W1600967790
- https://openalex.org/W1974155069
- https://openalex.org/W1999597477
- https://openalex.org/W2010327714
- https://openalex.org/W2030224590
- https://openalex.org/W2061438988
- https://openalex.org/W2081955678
- https://openalex.org/W2101577148
- https://openalex.org/W2117189826
- https://openalex.org/W2148821745
- https://openalex.org/W2151830023
- https://openalex.org/W2226980020
- https://openalex.org/W2278374431
- https://openalex.org/W4213162049
- https://openalex.org/W4246906001