دسترسی نامحدود
برای کاربرانی که ثبت نام کرده اند
دانلود کتاب The Inverse Method: Parametric Verification of Real-time Unbedded Systems
دانلود کتاب روش معکوس: تأیید پارامتریک سیستم‌های بدون بستر بلادرنگ
مشخصات کتاب
The Inverse Method: Parametric Verification of Real-time Unbedded Systems
ویرایش: 1
نویسندگان: Etienne André. Romain Soulat
سری: FOCUS Series
ISBN (شابک) : 1848214472, 9781848214477
ناشر: Wiley-ISTE
سال نشر: 2013
تعداد صفحات: 161
زبان: English
فرمت فایل : PDF (درصورت درخواست کاربر به PDF، EPUB یا AZW3 تبدیل می شود)
حجم فایل: 5 مگابایت
قیمت کتاب (تومان) : 42,000
در صورت تبدیل فایل کتاب 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
