Academic Journal
C.: Assume-Guarantee Verification for Interface Automata
| العنوان: | C.: Assume-Guarantee Verification for Interface Automata |
|---|---|
| المؤلفون: | Michael Emmi, Dimitra Giannakopoulou, Corina S. Păsăreanu |
| المساهمون: | The Pennsylvania State University CiteSeerX Archives |
| المصدر: | http://www.liafa.univ-paris-diderot.fr/~mje/papers/conf-fm-EmmiGP08.pdf. |
| بيانات النشر: | Springer |
| سنة النشر: | 2008 |
| المجموعة: | CiteSeerX |
| الوصف: | Interface automata provide a formalism capturing the high level interactions between software components. Checking compatibility, and other safety properties, in an automata-based system suffers from the scalability issues inherent in exhaustive techniques such as model checking. This work develops a theoretical framework and automated algorithms for modular verification of interface automata. We propose sound and complete assume-guarantee rules for interface automata, and learning-based algorithms to automate assumption generation. Our algorithms have been implemented in a practical model-checking tool and have been applied to a realistic NASA case study. 1 |
| نوع الوثيقة: | text |
| وصف الملف: | application/pdf |
| اللغة: | English |
| Relation: | http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.431.5320; http://www.liafa.univ-paris-diderot.fr/~mje/papers/conf-fm-EmmiGP08.pdf |
| الاتاحة: | http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.431.5320 http://www.liafa.univ-paris-diderot.fr/~mje/papers/conf-fm-EmmiGP08.pdf |
| Rights: | Metadata may be used without restrictions as long as the oai identifier remains attached to it. |
| رقم الانضمام: | edsbas.D61403CD |
| قاعدة البيانات: | BASE |
| الوصف غير متاح. |