Modeling and Verification of Real-Time Systems: Formalisms and Software Tools

ویرایش:  
 
سری:  
ISBN (شابک) : 9781848210134, 9780470611012 
ناشر: Wiley-ISTE 
سال نشر: 2008 
تعداد صفحات: 386 
زبان: English 
فرمت فایل : PDF (درصورت درخواست کاربر به PDF، EPUB یا AZW3 تبدیل می شود) 
حجم فایل: 4 مگابایت 

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

این عنوان به ارائه برخی از مهم ترین مفاهیم و تکنیک ها برای توصیف سیستم های بلادرنگ و تجزیه و تحلیل رفتار آنها به منظور قادر ساختن طراح برای دستیابی به تضمین های صحت زمانی اختصاص دارد.

موضوعات پرداخته شده شامل مدل‌های ریاضی سیستم‌های بلادرنگ و تکنیک‌های تأیید رسمی مرتبط مانند بررسی مدل، مدل‌سازی و تأیید احتمالی، زبان‌های برنامه‌نویسی و توصیف، و رویکردهای اعتبارسنجی مبتنی بر آزمایش است. با مشارکت نویسندگانی که در زمینه‌های مربوطه خود متخصص هستند، این امر به خواننده با آخرین هنر در راستی‌آزمایی رسمی سیستم‌های بلادرنگ و مروری بر ابزارهای نرم‌افزاری موجود ارائه می‌دهد. محتوا:
فصل 1 Time Petri Nets - روش‌های تحلیل و تأیید با TINA (صفحات 19-49): برنارد برتومیو، فلورنت پرز و فرانسوا ورنادات
فصل 2 اعتبار سنجی سیستم‌های راکتیو با استفاده از تأیید و آزمایش انطباق (صفحات 51-75): کامیل کنستان، تیری جرون، هروه مارچاند و ولاد روسو
فصل 3 مقدمه ای بر بررسی مدل (صفحات 77-110): استفان مرز
فصل 4 بررسی خودکار خودکارهای زمان بندی شده مدل (صفحات 111-140): پاتریشیا بویر و فرانسوا لاروسینی
فصل 5 مشخصات و تجزیه و تحلیل سیستم‌های ناهمزمان با استفاده از CADP (صفحات 141-169): Radu Mateescu
فصل 6 تأیید برنامه همزمان با Lustre/Lesar (صفحات 171-206): پاسکال ریموند
فصل 7 همزمان برنامه‌نویسی تابعی همزمان (Lucid Synchrone) صفحات 207–247): پل کاسپی، گرگوار هامون و مارک پوزه
فصل 8 تأیید سیستم‌های احتمالی زمان واقعی (صفحه‌های 249–288): مارتا کویتکووسکا، گتین نورمن، دیوید پارکر و جرمی اسپروستون
فصل 9 تأیید صحت روش‌ها و ابزارهای سیستم‌های احتمالی (صفحه‌های 289-318): سرژ حداد و پاتریس مورو
فصل 10 مدل‌سازی و تأیید سیستم‌های زمان واقعی با استفاده از مجموعه ابزار IF (صفحات 319-351): ماریوس بوزگا، سوزان گراف، لوران مونیر و Iulian Ober
فصل 11 معماری شرح زبان ها: مقدمه ای بر SAE AADL (صفحات 353-383): آنه ماری دپلانچ و سباستین فاکو

This title is devoted to presenting some of the most important concepts and techniques for describing real-time systems and analyzing their behavior in order to enable the designer to achieve guarantees of temporal correctness.

Topics addressed include mathematical models of real-time systems and associated formal verification techniques such as model checking, probabilistic modeling and verification, programming and description languages, and validation approaches based on testing. With contributions from authors who are experts in their respective fields, this will provide the reader with the state of the art in formal verification of real-time systems and an overview of available software tools.Content:
Chapter 1 Time Petri Nets – Analysis Methods and Verification with TINA (pages 19–49): Bernard Berthomieu, Florent Peres and Francois Vernadat
Chapter 2 Validation of Reactive Systems by Means of Verification and Conformance Testing (pages 51–75): Camille Constant, Thierry Jeron, Herve Marchand and Vlad Rusu
Chapter 3 An Introduction to Model Checking (pages 77–110): Stephan Merz
Chapter 4 Model Checking Timed Automata (pages 111–140): Patricia Bouyer and Francois Laroussinie
Chapter 5 Specification and Analysis of Asynchronous Systems using CADP (pages 141–169): Radu Mateescu
Chapter 6 Synchronous Program Verification with Lustre/Lesar (pages 171–206): Pascal Raymond
Chapter 7 Synchronous Functional Programming with Lucid Synchrone (pages 207–247): Paul Caspi, Gregoire Hamon and Marc Pouzet
Chapter 8 Verification of Real?Time Probabilistic Systems (pages 249–288): Marta Kwiatkowska, Gethin Norman, David Parker and Jeremy Sproston
Chapter 9 Verification of Probabilistic Systems Methods and Tools (pages 289–318): Serge Haddad and Patrice Moreaux
Chapter 10 Modeling and Verification of Real?Time Systems using the IF Toolset (pages 319–351): Marius Bozga, Susanne Graf, Laurent Mounier and Iulian Ober
Chapter 11 Architecture Description Languages: An Introduction to the SAE AADL (pages 353–383): Anne?Marie Deplanche and Sebastien Faucou