مشخصات کتاب

Towards Verified Systems

ویرایش:  
نویسندگان: Jonathan Bowen (Eds.)  
سری: Real-Time Safety Critical Systems 2 
ISBN (شابک) : 9780444899019 
ناشر: Elsevier Science Ltd 
سال نشر: 1994 
تعداد صفحات: 292 
زبان: English 
فرمت فایل : PDF (درصورت درخواست کاربر به PDF، EPUB یا AZW3 تبدیل می شود) 
حجم فایل: 5 مگابایت 

در صورت تبدیل فایل کتاب Towards Verified Systems به فرمت های PDF، EPUB، AZW3، MOBI و یا DJVU می توانید به پشتیبان اطلاع دهید تا فایل مورد نظر را تبدیل نمایند.

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

توضیحاتی در مورد کتاب به سمت سیستم های تأیید شده

با افزایش پیچیدگی سیستم‌های تعبیه‌شده با کنترل کامپیوتری، شیوه‌های صنعتی کنونی برای توسعه آن‌ها باعث نگرانی می‌شود، به‌ویژه برای کاربردهای حیاتی ایمنی که در آن جان انسان‌ها در خطر است. استفاده از نرم افزار در چنین سیستم هایی در دهه اخیر به شدت افزایش یافته است. روش‌های رسمی، مبتنی بر پایه‌های محکم، ابزاری را برای کمک به کاهش خطر ایجاد خطا در طول مشخصات و توسعه فراهم می‌کنند. در حال حاضر علاقه زیادی هم در محافل دانشگاهی و هم در محافل صنعتی در مورد مسائل مربوط به آن وجود دارد، اما این تکنیک ها هنوز نیاز به بررسی و انتشار بیشتر دارند تا استفاده گسترده از آنها به واقعیت تبدیل شود. این کتاب نتایج تحقیق در مورد تکنیک هایی را برای کمک به تأیید رسمی سیستم های سخت افزاری / نرم افزاری مختلط ارائه می دهد. جنبه‌های مشخصات سیستم و تأیید از نیازمندی‌ها تا سخت‌افزار زیربنایی، با توجه به مسائل بلادرنگ مورد بررسی قرار می‌گیرند. کار ارائه شده عمدتاً حول محور زبان برنامه نویسی Occam و پارادایم ریزپردازنده Transputer است. اثبات قضیه HOL، بر اساس منطق مرتبه بالاتر، عمدتاً در کاربرد براهین بررسی شده ماشینی استفاده شده است. این متن کار تحقیقاتی انجام شده بر روی پروژه مشارکتی DTI/SERC در UK Dictorate Engineering Dictorate Safemos را شرح می دهد. شرکای Inmos Ltd، Cambridge SRI، آزمایشگاه محاسبات دانشگاه آکسفورد و آزمایشگاه کامپیوتر دانشگاه کمبریج بودند که مشکلات تأیید رسمی سیستم های تعبیه شده را بررسی کردند. مهمترین نتایج پروژه در قالب مجموعه ای از فصول مرتبط به هم توسط اعضای پروژه و پرسنل مرتبط ارائه شده است. علاوه بر این، مروری بر دو سرمایه گذاری دیگر با اهداف مشابه به عنوان ضمیمه گنجانده شده است. مطالب موجود در این کتاب برای محققان علوم محاسباتی و متخصصان صنعتی پیشرفته در نظر گرفته شده است که علاقه‌مند به کاربرد روش‌های رسمی در سیستم‌های حیاتی ایمنی در تمام سطوح انتزاعی از نیازمندی‌ها تا سخت‌افزار هستند. علاوه بر این، مطالبی با ماهیت کلی‌تر ارائه شده است که ممکن است برای مدیران مسئول پروژه‌هایی که روش‌های رسمی را به کار می‌گیرند، به‌ویژه برای سیستم‌های ایمنی-بحرانی، و سایرینی که به استفاده از آنها فکر می‌کنند، علاقه‌مند باشد.

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

As the complexity of embedded computer-controlled systems increases, the present industrial practice for their development gives cause for concern, especially for safety-critical applications where human lives are at stake. The use of software in such systems has increased enormously in the last decade. Formal methods, based on firm foundations, provide one means to help with reducing the risk of inducing errors during specification and development. There is currently much interest in both academic and industrial circles concerning the issues involved, but the techniques still need further investigation and promulgation to make their widespread use a reality. This book presents results of research into techniques to aid the formal verification of mixed hardware/software systems. Aspects of system specification and verification from requirements down to the underlying hardware are addressed, with particular regard to real-time issues. The work presented is largely based around the Occam programming language and Transputer microprocessor paradigm. The HOL theorem prover, based on higher order logic, has mainly been used in the application of machine-checked proofs. This text describes research work undertaken on the collaborative UK DTI/SERC-funded Information Engineering Dictorate Safemos project. The partners were Inmos Ltd, Cambridge SRI, the Oxford University Computing Laboratory and the University of Cambridge Computer Laboratory, who investigated the problems of formally verifying embedded systems. The most important results of the project are presented in the form of a series of interrelated chapters by project members and associated personnel. In addition, overviews of two other ventures with similar objectives are included as appendices. The material in this book is intended for computing science researchers and advanced industrial practitioners interested in the application of formal methods to real-time safety-critical systems at all levels of abstraction from requirements to hardware. In addition, material of a more general nature is presented, which may be of interest to managers in charge of projects applying formal methods, especially for safety-critical-systems, and others who are considering their use

فهرست مطالب

Content: 
Real-Time Saeety Critical Systems
Page ii

Front Matter
Page iii

Copyright page
Page iv

List of Figures
Page xiii

List of Tables
Page xv

Dedication
Page xvi

Foreword
Pages xvii-xviii
C.A.R. Hoare

Preface
Pages xix-xxi
J.P. Bowen

Contact Addresses
Pages xxiii-xxvi

CHAPTER 1 - Safety-Critical Systems and Formal Methods
Pages 3-33
J.P. Bowen, V. Stavridou

CHAPTER 2 - Overview of the Project
Pages 35-46
J.P. Bowen, M.J.C. Gordon, J.A. Camilleri, P.K. Pandya et al.

CHAPTER 3 - The HOL Logic and System
Pages 49-70
M.J.C. Gordon, A.M. Pitts

CHAPTER 4 - Timed Transition Systems
Pages 71-90
R.W.S. Hale, R.M. Cardell-Oliver, J.M.J. Herbert

CHAPTER 5 - State Transition Assertions: A Case Study
Pages 93-113
M.J.C. Gordon

CHAPTER 6 - A Real-time Programming Language
Pages 115-130
R.W.S. Hale, He Jifeng

CHAPTER 7 - Program Compilation
Pages 131-146
R.W.S. Hale

CHAPTER 8 - A Framework for Microprocessor Design
Pages 149-165
J.M.J. Herbert

CHAPTER 9 - Designing a Processor
Pages 167-192
D.E. Shepherd

CHAPTER 10 - Hardware Compilation
Pages 193-207
J.P. Bowen, He Jifeng, I. Page

CHAPTER 11 - Transfer into Industrial Design
Pages 211-221
D.E. Shepherd, J.P. Bowen

Appendix A - System Verification and the CLI Stack
Pages 225-248
W.D. Young

Appendix B - The ProCoS Project: Provably Correct Systems
Pages 249-265
H. Langmaack, A.P. Ravn

Acknowledgements
Page 267

Bibliography
Pages 269-296

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

کتاب های تصادفی

دانلود کتاب Gastroenterología

دانلود کتاب Helicopter Crew Chief

دانلود کتاب The Playboy Interview II

دانلود کتاب С бојних поља / S bojnih polja

دانلود کتاب Туризмдегі кəсіпкерлік іс-əрекет негіздері. Оқу құралы