LES DERNIÈRES INFORMATIONS
Verification of Multi Decisional Reactive Agent using SMV Model Checker
Titre | Verification of Multi Decisional Reactive Agent using SMV Model Checker |
Publication Type | Conference Paper |
Year of Publication | 2013 |
Authors | Haqiq, A, Bounabat, B |
Conference Name | 2013 8TH INTERNATIONAL DESIGN AND TEST SYMPOSIUM (IDT) |
Publisher | IEEE |
ISBN Number | 978-1-4799-3525-3 |
Abstract | On account of the evolution of technology, more complicated software arrives with the need to be verified to prevent the errors occurrence in a system which could generate fatal accidents and economic loss. These errors must be detected in an early stage during the development process to reduce redesign costs and faults. To ensure the correctness of software systems, formal verification provides an alternative approach to verify that an implementation of the expected system fulfills its specification. This paper focuses on the verification of reactive system behaviors specified by the Multi Decisional Reactive Agent (MDRA) and modeled using MDRA Profile. The objective in this paper is to use the Model Checking technique for MDRA Profile verification through the Model Checker SMV (Symbolic Model Verifier) to automatically verify the system properties expressed in temporal logic. The SMV mainly focusing on reactive systems provides a modular hierarchical descriptions and definition of reusable components. Besides, the expression of system properties is more described through both Computational Tree Logic (CTL) and Linear Temporal Logic (LTL).
|
Contactez-nous
ENSIAS
Avenue Mohammed Ben Abdallah Regragui, Madinat Al Irfane, BP 713, Agdal Rabat, Maroc
Télécopie : (+212) 5 37 68 60 78
Secrétariat de direction : 06 61 48 10 97
Secrétariat général : 06 61 34 09 27
Service des affaires financières : 06 61 44 76 79
Service des affaires estudiantines : 06 62 77 10 17 / n.mhirich@um5s.net.ma
Résidences : 06 61 82 89 77
Contacts
Compteur de visiteurs:628,639
Education - This is a contributing Drupal Theme
Design by
WeebPal.