Synchronous Equivalence: Formal Methods for Embedded Systems

سیستم تعبیه شده به هر سیستمی که از الکترونیک استفاده می کند اما به عنوان یک کامپیوتر همه منظوره درک یا استفاده نمی شود، تعریف می شود. به طور سنتی، یک یا چند مدار الکترونیکی یا ریزپردازنده به معنای واقعی کلمه در سیستم تعبیه می‌شوند، یا نقش‌هایی را بر عهده می‌گیرند که قبلاً توسط دستگاه‌های مکانیکی انجام می‌شد، یا عملکردی ارائه می‌دهند که در غیر این صورت ممکن نیست.
هدف این کتاب بررسی چگونگی اعمال روش های رسمی در حوزه طراحی سیستم های جاسازی شده است. تاکید بر مشخصات، نمایش، اعتبارسنجی و کاوش طراحی چنین سیستم هایی از دیدگاه سطح بالا است. نویسندگان چارچوبی را که نظریه‌ها و آزمایش‌ها بر آن استوار است، و از طریق آن روش‌های رسمی به سنتز و شبیه‌سازی مرتبط می‌شوند، مرور می‌کنند.
یک روش تأیید رسمی برای تأیید ویژگی‌های کلی طرح‌ها و نشان دادن اینکه این روش در مقابله با مشکل پیچیدگی کارآمد و در یافتن باگ‌ها مؤثر است، فرموله شده است. با این حال، مداخله دستی در قالب انتخاب انتزاع و جداسازی زمان و عملکرد مورد نیاز است. حدس زده می‌شود که برای ویژگی‌های خاص، الگوریتم‌های کارآمد برای اعتبارسنجی رسمی کاملاً خودکار سیستم‌ها وجود دارد.
هم ارزی همزمان: روش های رسمی برای سیستم های جاسازی شده یک رویکرد رسمی کاملاً جدید برای تحلیل هم ارزی سطح بالا ارائه می دهد. راه‌های اکتشاف طراحی را باز می‌کند که قبلاً کشف نشده بودند. این اثری است که می تواند به تنهایی بایستد اما در عین حال کاملاً با چارچوب سنتز و شبیه سازی که در کتاب دیگری توسط ناشران آکادمیک Kluwer طراحی مشترک سخت افزار-نرم افزارسیستم های تعبیه شده توضیح داده شده است، سازگار است: رویکرد POLIS، توسط Balarin و همکاران.
هم‌ارزی همزمان: روش‌های رسمی برای سیستم‌های جاسازی شده مورد توجه طراحان سیستم‌های جاسازی شده (الکترونیک خودرو) خواهد بود. ، لوازم الکترونیکی مصرفی و مخابرات)، طراحان میکروکنترلر، توسعه دهندگان و دانشجویان CAD، و همچنین ارائه دهندگان IP، طراحان پلت فرم معماری، ارائه دهندگان سیستم عامل، و طراحان مدارها و سیستم های VLSI.

An embedded system is loosely defined as any system that utilizes electronics but is not perceived or used as a general-purpose computer. Traditionally, one or more electronic circuits or microprocessors are literally embedded in the system, either taking up roles that used to be performed by mechanical devices, or providing functionality that is not otherwise possible.
The goal of this book is to investigate how formal methods can be applied to the domain of embedded system design. The emphasis is on the specification, representation, validation, and design exploration of such systems from a high-level perspective. The authors review the framework upon which the theories and experiments are based, and through which the formal methods are linked to synthesis and simulation.
A formal verification methodology is formulated to verify general properties of the designs and demonstrate that this methodology is efficient in dealing with the problem of complexity and effective in finding bugs. However, manual intervention in the form of abstraction selection and separation of timing and functionality is required. It is conjectured that, for specific properties, efficient algorithms exist for completely automatic formal validations of systems.
Synchronous Equivalence: Formal Methods for Embedded Systems presents a brand new formal approach to high-level equivalence analysis. It opens design exploration avenues previously uncharted. It is a work that can stand alone but at the same time is fully compatible with the synthesis and simulation framework described in another book by Kluwer Academic Publishers Hardware-Software Co-Design of EmbeddedSystems: The POLIS Approach, by Balarin et al.
Synchronous Equivalence: Formal Methods for Embedded Systems will be of interest to embedded system designers (automotive electronics, consumer electronics, and telecommunications), micro-controller designers, CAD developers and students, as well as IP providers, architecture platform designers, operating system providers, and designers of VLSI circuits and systems.