عنوان پایان‌نامه
درستی یای با استفاده از اسرشنها در سطح تی ال ام
- رشته تحصیلی
- مهندسی کامپیوتر-معماری کامپیوتر
- مقطع تحصیلی
- کارشناسی ارشد
- محل دفاع
- کتابخانه مرکزی -تالار اطلاع رسانی شماره ثبت: 45455;کتابخانه مرکزی پردیس 2 فنی شماره ثبت: E 1758
- تاریخ دفاع
- ۱۷ شهریور ۱۳۸۹
- دانشجو
- امیرعلی غفرانی
- استاد راهنما
- زین العابدین نوابی شیرازی, سعید صفری
- چکیده
- با افزایش اندازه و پیچیدگی سیستم های دیجیتال و به منظور کاهش زمان و هزینه های تولید اینگونه سیستم ها، سطح انتزاع توصیف از سطح انتقال ثبات به سطح تراکنش تغییر کرد. هر چند با بالا رفتن سطح انتزاع کنترل پیچیدگی راحت تر و سرعت شبیه سازی نیز بیشتر شده است، با این وجود تعریف روش های درستی سنجی مناسب برای این سطح انتزاعی هنوز در ابتدای راه قرار دارند. در این پایان نامه تلاش شده است تا روشی برای درستی سنجی صوری مدار های توصیف شده در سطح تراکنش و بر مبنای کتابخانه TLM-2.0 که استاندارد فعلی توصیف چنین سیستم هایی می باشد ارائه شود. برای این امر ابتدا روش های توصیف صوری موجود ارائه و با یکدیگر مقایسه می شوند. سپس با انتخاب خودکاره زمان دار به عنوان مدلی مناسب برای توصیف مدل های سطح تراکنش، نحوه تبدیل این مدار ها به این مدل تبیین می شود. در گام بعد نحوه بیان ویژگی ها بر روی این مدل بیان می شود و سپس از ابزار درستی سنج ارائه شده برای این مدل صوری برای آزمودن برقراری این ویژگی ها استفاده می شود. نتایج زمانی این درستی سنجی با روشی مبتنی بر توصیف مدار ها با استفاده از مدل شبکه های پتری مقایسه می شود که حاکی از برتری نتایج این روش نسبت به روش مبتنی بر شبکه های پتری در مثال مقایسه شده است. در ادامه مفهوم صلاحیت سنجی عملیات درستی سنجی صوری تعریف می گردد و صلاحیت ویژگی های اعمال شده برای درستی سنجی آزموده می شود. هدف از صلاحیت سنجی پاسخ به این سؤال است که آیا محیط درستی سنجی که در اینجا متشکل از ویژگی های تعریف شده می باشد، قادر به تشخیص خطا های ممکن مدار می باشند یا خیر. بدین منظور یک مدل خطا بر روی این مدل صوری در نظر گرفته می شود و توانایی ویژگی های توصیف شده در کشف این خطا ها سنجیده می شود. تحلیل نتایج این مرحله می تواند به توصیف ویژگی های تعریف نشده کمک کند
- Abstract
- The ever-increasing complexity of digital systems forced the designers to move to a higher abstraction level, system level design. Designing in this level results in reduced cost and time of design and implementation, and helps the designer to cope with the complexity of recent systems. Although this abstraction led to easier handling of the design complexity and higher simulation speed, verification methods needed to verify correctness of the design are still immature for this level of abstraction. In this thesis, a mechanism is introduced to formally verify the properties on the system level designs implemented by transaction level modeling (TLM). Here, the models are defined using TLM2.0 library. For formal verification, it is needed to first choose a formal model in which the design should be described. Among various alternatives, Timed Automata (TA) was selected due to its advanced verifier tool, existence of time concept in the model, support of complex data structures, and other facilities. Then, translation of a TLM design into a TA model is described. The next step is to define properties of the design in the property specification description language of TA. These properties are verified on the formal model of the design, using the UPPAAL tool which is an existing verifier for TA. Comparison of the timing results of this method with a similar one based on petri-net formal method shows improvements in the considered cases. Moreover, the concept of formal verification qualification is introduced which can check the quality of the properties defined to verify the design. The purpose of the qualification is to answer the question "Have I defined enough properties to verify the design?" or "How good is the verification environment?" For this reason a fault model is introduced on TA formal model and the ability of defined properties to detect these faults on the actual design is examined. The analysis of the fault detection result is used as a hint to define missing properties. Keywords: Transaction Level Modeling, Verification Methods, Design Errors, Property Definition, Verification Qualification, Timed Automata, UPPAAL
