Behavioral Compatibility Without State Explosion: Design and Verification of a Component-based Elevator Control System

Paul C. Attie, David Lorenz, Aleksandra Portnova, Hana Chockler

نتاج البحث: فصل من :كتاب / تقرير / مؤتمرمنشور من مؤتمرمراجعة النظراء

ملخص

Most methods for designing component-based systems and verifying their compatibility address only the syntactic compatibility of components; no analysis of run-time behavior is made. Those methods that do address run-time behavior suffer from state-explosion: the exponential increase of the number of global states, and hence the complexity of the analysis, with the number of components. We present a method for designing component-based systems and verifying their behavioral compatibility and temporal behavior that is not susceptible to state explosion. Our method is mostly automatic, with little manual deduction required, and does not analyze a large system of connected components at once, but instead analyzes components two-at-a-time. This pair-wise approach enables the automatic verification of temporal behavior, using model-checking, in time polynomial in the number and size of all components. Our method checks that behavior of a pair of interacting components conforms to given properties, specified in temporal logic. Interaction of the components is captured in a product of their behavioral automata, which are provided as a part of each component's interface. We demonstrate the effectiveness of our method by applying it to the design and verification of a component-based elevator control algorithm.

اللغة الأصليةالإنجليزيّة
عنوان منشور المضيفProceedings of the 9th International Conference on Component-Based Software Engineering (CBSE '06)
مكان النشرVästerås, Sweden
ناشرSpringer Verlag
الصفحات33-49
عدد الصفحات17
مستوى الصوت4063
رقم المعيار الدولي للكتب (المطبوع)3540356282, 9783540356288
المعرِّفات الرقمية للأشياء
حالة النشرنُشِر - يونيو 2006
منشور خارجيًانعم
الحدث9th International Symposium on Component-Based Software Engineering, CBSE 2006 - Vasteras, السويد
المدة: ٢٩ يونيو ٢٠٠٦١ يوليو ٢٠٠٦

سلسلة المنشورات

الاسمLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
مستوى الصوت4063 LNCS
رقم المعيار الدولي للدوريات (المطبوع)0302-9743
رقم المعيار الدولي للدوريات (الإلكتروني)1611-3349

!!Conference

!!Conference9th International Symposium on Component-Based Software Engineering, CBSE 2006
الدولة/الإقليمالسويد
المدينةVasteras
المدة٢٩/٠٦/٠٦١/٠٧/٠٦

بصمة

أدرس بدقة موضوعات البحث “Behavioral Compatibility Without State Explosion: Design and Verification of a Component-based Elevator Control System'. فهما يشكلان معًا بصمة فريدة.

قم بذكر هذا