ورود به حساب

نام کاربری گذرواژه

گذرواژه را فراموش کردید؟ کلیک کنید

حساب کاربری ندارید؟ ساخت حساب

ساخت حساب کاربری

نام نام کاربری ایمیل شماره موبایل گذرواژه

برای ارتباط با ما می توانید از طریق شماره موبایل زیر از طریق تماس و پیامک با ما در ارتباط باشید


09117307688
09117179751

در صورت عدم پاسخ گویی از طریق پیامک با پشتیبان در ارتباط باشید

دسترسی نامحدود

برای کاربرانی که ثبت نام کرده اند

ضمانت بازگشت وجه

درصورت عدم همخوانی توضیحات با کتاب

پشتیبانی

از ساعت 7 صبح تا 10 شب

دانلود کتاب The Inverse Method: Parametric Verification of Real-time Unbedded Systems

دانلود کتاب روش معکوس: تأیید پارامتریک سیستم‌های بدون بستر بلادرنگ

The Inverse Method: Parametric Verification of Real-time Unbedded Systems

مشخصات کتاب

The Inverse Method: Parametric Verification of Real-time Unbedded Systems

ویرایش: 1 
نویسندگان:   
سری: FOCUS Series 
ISBN (شابک) : 1848214472, 9781848214477 
ناشر: Wiley-ISTE 
سال نشر: 2013 
تعداد صفحات: 161 
زبان: English 
فرمت فایل : PDF (درصورت درخواست کاربر به PDF، EPUB یا AZW3 تبدیل می شود) 
حجم فایل: 5 مگابایت

قیمت کتاب (تومان) : 45,000



ثبت امتیاز به این کتاب

میانگین امتیاز به این کتاب :
       تعداد امتیاز دهندگان : 17


در صورت تبدیل فایل کتاب The Inverse Method: Parametric Verification of Real-time Unbedded Systems به فرمت های PDF، EPUB، AZW3، MOBI و یا DJVU می توانید به پشتیبان اطلاع دهید تا فایل مورد نظر را تبدیل نمایند.

توجه داشته باشید کتاب روش معکوس: تأیید پارامتریک سیستم‌های بدون بستر بلادرنگ نسخه زبان اصلی می باشد و کتاب ترجمه شده به فارسی نمی باشد. وبسایت اینترنشنال لایبرری ارائه دهنده کتاب های زبان اصلی می باشد و هیچ گونه کتاب ترجمه شده یا نوشته شده به فارسی را ارائه نمی دهد.


توضیحاتی در مورد کتاب روش معکوس: تأیید پارامتریک سیستم‌های بدون بستر بلادرنگ



این کتاب تکنیک‌های تأیید پیشرفته را برای سیستم‌های جاسازی شده در زمان واقعی، بر اساس روش معکوس برای اتومات‌های زمان‌دار پارامتریک معرفی می‌کند. این فرمالیسم های رایج برای مشخصات و تأیید سیستم های همزمان زمان دار و به ویژه اتومات های زمان دار و همچنین چندین الحاقیه مانند اتومات های زمان دار مجهز به کرونومتر، اتومات های هیبریدی خطی و اتومات های هیبریدی افین را بررسی می کند.
روش معکوس معرفی شده است. و مزایای آن برای تضمین استحکام در سیستم های بلادرنگ نشان داده شده است. سپس، نشان داده می‌شود که چگونه یک تکرار روش معکوس می‌تواند با محاسبه نقشه‌برداری رفتاری سیستم، مسئله پارامترهای خوب را برای اتوماتای ​​زمان‌دار پارامتریک حل کند. پسوندهای مختلفی به ویژه برای سیستم‌های ترکیبی و برنامه‌های کاربردی برای مشکلات زمان‌بندی با استفاده از اتومات‌های زمان‌دار با کرونومتر پیشنهاد شده‌اند. نمونه‌های مختلف، هم از ادبیات و هم از صنعت، تکنیک‌ها را در سراسر کتاب نشان می‌دهند.
تأییدات پارامتریک مختلف، به‌ویژه انتزاع‌های مدار حافظه‌ای که توسط سازنده چیپ‌ست ST-Microelectronics فروخته می‌شود، و همچنین بررسی‌های بعدی انجام می‌شود. سیستم کنترل پرواز نسل بعدی فضاپیمای طراحی شده توسط ASTRIUM Space Transportation.

محتوا:

1. خودکار زمانبندی پارامتریک.
2. روش معکوس برای خودکارهای زمانبندی پارامتریک.
3. روش معکوس در عمل: کاربرد در مطالعات موردی.
4. کارتوگرافی رفتاری خودکارهای زماندار.
5. سنتز پارامتر برای اتوماتای ​​هیبریدی.
6. کاربرد در تحلیل استحکام مسائل زمانبندی.
7. نتیجه گیری و دیدگاه ها.

درباره نویسندگان

اتین آندره دانشیار آزمایشگاه اطلاعات پاریس نورد، دانشگاه پاریس 13 است. (Sorbonne Paris Cité) در فرانسه. علایق تحقیقاتی فعلی او بر تأیید سیستم‌های بلادرنگ متمرکز است.
رومن سولات در حال تکمیل دکترای خود در آزمایشگاه LSV در ENS-Cachan در فرانسه است که بر مدل‌سازی و تأیید سیستم‌های زمانی ترکیبی تمرکز دارد.


توضیحاتی درمورد کتاب به خارجی

This book introduces state-of-the-art verification techniques for real-time embedded systems, based on the inverse method for parametric timed automata. It reviews popular formalisms for the specification and verification of timed concurrent systems and, in particular, timed automata as well as several extensions such as timed automata equipped with stopwatches, linear hybrid automata and affine hybrid automata.
The inverse method is introduced, and its benefits for guaranteeing robustness in real-time systems are shown. Then, it is shown how an iteration of the inverse method can solve the good parameters problem for parametric timed automata by computing a behavioral cartography of the system. Different extensions are proposed particularly for hybrid systems and applications to scheduling problems using timed automata with stopwatches. Various examples, both from the literature and industry, illustrate the techniques throughout the book.
Various parametric verifications are performed, in particular of abstractions of a memory circuit sold by the chipset manufacturer ST-Microelectronics, as well as of the prospective flight control system of the next generation of spacecraft designed by ASTRIUM Space Transportation.

Contents:

1. Parametric Timed Automata.
2. The Inverse Method for Parametric Timed Automata.
3. The Inverse Method in Practice: Application to Case Studies.
4. Behavioral Cartography of Timed Automata.
5. Parameter Synthesis for Hybrid Automata.
6. Application to the Robustness Analysis of Scheduling Problems.
7. Conclusion and Perspectives.

About the Authors

Étienne André is Associate Professor in the Laboratoire d’Informatique de Paris Nord, in the University of Paris 13 (Sorbonne Paris Cité) in France. His current research interests focus on the verification of real-time systems.
Romain Soulat is currently completing his PhD at the LSV laboratory at ENS-Cachan in France, focusing on the modeling and verification of hybrid temporal systems.



فهرست مطالب

The Inverse Method......Page 2
Copyright......Page 3
Contents......Page 4
Preface......Page 8
Acknowledgments......Page 9
Introduction......Page 10
I.1.1. An example of asynchronous circuit......Page 11
I.2. The good parameters problem......Page 12
I.3.1. Content......Page 13
I.3.2. Organization of the book......Page 14
I.3.3. Acknowledgements......Page 15
1.1.1. Clocks......Page 16
1.1.3. Constraints......Page 17
1.3. Timed automata......Page 19
1.3.1. Syntax......Page 20
1.3.2. Semantics......Page 22
1.4. Parametric timed automata......Page 25
1.4.1. Syntax......Page 26
1.4.2. Semantics......Page 29
1.5.1. Representation of time......Page 34
1.5.2. Timed automata......Page 35
1.5.3. Time Petri nets......Page 36
1.5.4. Hybrid systems......Page 37
2 The Inverse Method for Parametric Timed Automata......Page 38
2.1.1. A motivating example......Page 39
2.1.2. The problem......Page 41
2.2.1. Principle......Page 42
2.2.3. Remarks on the algorithm......Page 43
2.2.4. Results......Page 47
2.3. Variants of the inverse method......Page 55
2.3.1. Algorithm with state inclusion in the fixpoint......Page 56
2.3.2. Algorithm with union of the constraints......Page 57
2.3.3. Algorithm with simple return......Page 59
2.3.4. Combination: inclusion in fixpoint and union......Page 60
2.3.6. Summary of the algorithms......Page 61
2.4.1. History of the inverse method......Page 64
2.4.3. Formal techniques of verification......Page 65
2.4.4. Problems related to the inverse problem......Page 66
2.4.5. Parameter synthesis for parametric timed automata......Page 68
3 The Inverse Method in Practice:Application to Case Studies......Page 70
3.1.2. Architecture and features......Page 71
3.2. Flip-flop......Page 72
3.3. SR-Latch......Page 73
3.3.1. Parameter synthesis......Page 74
3.4. AND?OR......Page 75
3.5.1. Description of the model......Page 77
3.6. Bounded Retransmission Protocol......Page 79
3.7. CSMA/CD protocol......Page 80
3.8.1. Description......Page 82
3.8.2. A short history......Page 86
3.8.3. Manually abstracted model......Page 87
3.8.4. Automatically generated model......Page 90
3.9.1. Description of the model......Page 92
3.9.2. Definition of a zone of good behavior......Page 93
3.10. Tools related to IMITATOR......Page 94
4 Behavioral Cartography of Timed Automata......Page 96
4.1. The behavioral cartography algorithm......Page 97
4.2.1. Acyclic parametric timed automata......Page 98
4.3. Case studies......Page 99
4.3.1. Implementation......Page 100
4.3.2. SR latch......Page 101
4.3.3. Flip-flop......Page 106
4.3.5. SPSMALL memory......Page 110
4.4. Related work......Page 116
5 Parameter Synthesis for Hybrid Automata......Page 118
5.1.1. Basic definitions......Page 120
5.1.2. Symbolic semantics of linear hybrid automata......Page 123
5.2.1. The inverse method for hybrid automata......Page 124
5.2.2. Behavioral cartography of hybrid automata......Page 126
5.2.3. Enhancement of the method for affine dynamics......Page 129
5.3. Implementation......Page 131
5.4. Discussion......Page 132
5.5. Related work......Page 133
6.1.1. Scheduling problems......Page 135
6.1.2. Timed automata augmented with stopwatches......Page 136
6.2.1. Modeling schedulability with timed automata......Page 137
6.2.3. Schedulability zone synthesis......Page 138
6.3.2. Schedulability zone synthesis......Page 140
6.3.3. Next generation spacecraft flight control system......Page 141
6.4. Discussion......Page 144
6.5. Related work......Page 145
7 Conclusion and Perspectives......Page 146
7.2. Preservation of temporal logics......Page 147
7.3. Application to other formalisms......Page 148
Bibliography......Page 149
Index......Page 160




نظرات کاربران

تمامی حقوق معنوی و مادی وبسایت متعلق به اینترنشنال لایبرری می باشد
نماد اعتماد الکترونیکی