عنوان پایان‌نامه

تحلیل جبری معماری خط تولید نرم افزار



    دانشجو در تاریخ ۲۶ بهمن ۱۳۹۲ ، به راهنمایی ، پایان نامه با عنوان "تحلیل جبری معماری خط تولید نرم افزار" را دفاع نموده است.


    محل دفاع
    کتابخانه مرکزی پردیس 2 فنی شماره ثبت: E 2442;کتابخانه مرکزی -تالار اطلاع رسانی شماره ثبت: 63076
    تاریخ دفاع
    ۲۶ بهمن ۱۳۹۲

    مهندسی خط محصول نرم‌افزار از طریق مدیریت تغییرپذیری و استفاده مجدد اصولی از دارایی‌های مشترک سیستم‌های نرم‌افزاری مشابه، روشی را برای تولید کارای یک خانواده از این سیستم‌ها پیشنهاد می‌دهد. معماری یک خط محصول نرم‌افزار، اشتراکات و تغییرپذیری بین محصولات مختلف را در سطح بالایی از انتزاع با تمرکز بر زیرسیستم‌ها و ارتباطات بین آن‌ها به تصویر می‌کشد. سیستم‌های بحرانی زیادی با استفاده از روش خط محصول نرم‌افزار تولید می‌شوند. از این رو، تضمین درستی معماری خطوط محصول نرم‌افزار برای کشف خطاها در مراحل اولیه فرآیند تولید سیستم‌های نرم‌افزاری و در نتیجه جلوگیری از انتشار آن‌ها در مراحل بعدی این فرآیند، حیاتی به نظر می‌رسد. ‎ ما یک زبان توصیف معماری صوری برای توصیف جنبه‌های ساختاری و رفتاری معماری خط محصول ارائه می‌دهیم به‌طور‌ی‌که از تغییرپذیری‌های سطح معماری به‌طور صریح پشتیبانی می‌کند. ‌این زبان از نمادگذاری‌های متنی و گرافیکی برای توصیف معماری بهره می‌گیرد و سعی می‌کند تا مدل معتبری از خط محصول را ارائه دهد. رفتار عناصر معماری با استفاده از عبارت‌های شبه جبری ترتیبی بیان می‌شود.‎ هم‌چنین ما با یک روش قاعده‌مند، چگونگی به دست آوردن معنای صوری رفتار کل معماری خط محصول را از رفتار عناصر آن و ارتباطات بین آن‌ها بیان می‌کنیم. توصیف صوری رفتار یک معماری خط محصول، به‌کارگیری شیوه‌های صوری هم‌چون وارسی‌ مدل و استدلال هم‌ارزی را برای درستی‌یابی و تغییر در توصیف انجام شده امکان‌پذیر خواهد کرد. برای استدلال هم‌ارزی، ما مفهوم شبیه‌سازی دوسویه خط محصول را معرفی می‌نمائیم. چارچوب پیشنهادی ما، نشان می‌دهد که یکپارچه‌سازی روش‌های صوری و شبه صوری، به ما قدرت تولید یک زبان توصیف معماری را می‌دهد که در حین سادگی برای استفاده، امکان مشخص کردن و درستی‌یابی پیچیدگی‌های معماری خط محصول را مهیا خواهد کرد.
    Abstract
    Software product line (SPL) engineering proposes efficient development of multiple related software systems (called products at once through systematic reuse of common parts and management of variability between the products in a SPL. A SPL architecture reifies the commonalities and variability between the various products at the highest level of abstraction by focusing on their subsystems and relationships. Many safety critical systems are developed as product lines. So correctness assurance of SPL architecture is crucial to detect design errors at the early stages of developments, and consequently prevent their propagations to the next steps. We provide a formal architecture description language to capture behavioral and structural aspects of product line architectures while variability relative to the software architecture of the product line are explicitly addressed. The language uses the textual and graphical notations to describe the architecture and tries to provide a valid model of SPL. The behavior of elements are specified by sequential semi-algebraic process terms. Also, we define how the overall behavior of an architecture is derived from the behavior of its elements and graphical description in a systematic way. The formal behavior description of a product line architecture enables application of formal techniques like model checking and equational reasoning to detect design errors and to manipulate its description . To apply the latter technique, we provide the notion of product line bisimilarity over process terms. Our framework demonstrate that integrating semi-formal and formal notations provides us powerful yet simple description language to specify and verify complexities adherent to the product line architectures.