Conference
Towards Robustness Analysis using PVS
| العنوان: | Towards Robustness Analysis using PVS |
|---|---|
| المؤلفون: | Clavel, R., Pierre, Laurence, Leveugle, Régis |
| المساهمون: | Techniques de l'Informatique et de la Microélectronique pour l'Architecture des systèmes intégrés (TIMA), Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS) |
| المصدر: | Proc. Conference on Interactive Theorem Proving (ITP'11), Nijmegen (NL), 22-25 August ; Conference on Interactive Theorem Proving (ITP'11) ; https://hal.science/hal-00625269 ; Conference on Interactive Theorem Proving (ITP'11), Aug 2011, Nijmegen, Netherlands. pp.71-86, ⟨10.1007/978-3-642-22863-6_8⟩ |
| بيانات النشر: | HAL CCSD Springer |
| سنة النشر: | 2011 |
| المجموعة: | Université Grenoble Alpes: HAL |
| مصطلحات موضوعية: | robustness, pvs, PACS 85.42, [SPI.NANO]Engineering Sciences [physics]/Micro and nanotechnologies/Microelectronics |
| جغرافية الموضوع: | Nijmegen, Netherlands |
| الوصف: | International audience ; This work targets the use of formal methods for enhancing dependability analysis of sequential circuits described at the Register Transfer (RT) level. We consider solutions oriented towards theorem-proving techniques as an alternative to classical fault-injection techniques, for analyzing the consequences of errors caused by transient faults. A preliminary study was conducted to evaluate the advantages of a highly automated tool like ACL2 in that context. However, this study showed that, in spite of its numerous advantages, the ACL2 logic is not always expressive enough to deal with the properties under consideration here. In this paper, we briefly explain the shortcomings of ACL2 relatively to our problem, and we investigate the application of PVS, thus enabling to improve our simple and multiple faults models and the associated verification methodology. |
| نوع الوثيقة: | conference object |
| اللغة: | English |
| Relation: | hal-00625269; https://hal.science/hal-00625269 |
| DOI: | 10.1007/978-3-642-22863-6_8 |
| الاتاحة: | https://hal.science/hal-00625269 https://doi.org/10.1007/978-3-642-22863-6_8 |
| رقم الانضمام: | edsbas.C6BCAAB4 |
| قاعدة البيانات: | BASE |
| DOI: | 10.1007/978-3-642-22863-6_8 |
|---|