UML-B Specification for Proven Embedded Systems Design

این کتاب دیدگاه پروژه را در مورد محیط‌های مشخصات سیستم یکپارچه‌کننده پارادایم برای طراحی الکترونیکی اثبات‌شده (PUS SEE) همانطور که در طول تحقیق در سال‌های 2002 تا 2003 تصور شد، ارائه می‌کند. بیانیه اولیه تحقیق به صورت زیر فرموله شد: هدف PUSSEE معرفی اثبات رسمی ویژگی‌های سیستم در سراسر یک روش طراحی سیستم مدولار است که تأیید مشترک زیرسیستم‌ها را با پالایش سیستم و قابلیت استفاده مجدد از اجزای سیستم مجازی یکپارچه می‌کند. این کار با ترکیب زبان‌های UML و B انجام می‌شود تا امکان تأیید مشخصات سیستم از طریق ترکیب زیرسیستم‌های اثبات شده (به ویژه رابط‌های خاص با استفاده از استاندارد VSIAISLIF) فراهم شود. پیوند B با C، VHDL و SystemC، فرآیند طراحی صحیح با ساخت را به مراحل پایین‌تر توسعه سیستم روی تراشه (SoC) گسترش می‌دهد. بر اساس کار VSI Alliance، ابزارهای نمونه اولیه برای تولید کد از UML و B توسعه خواهند یافت، و ابزارهای تأیید B موجود برای پشتیبانی از استفاده مجدد از IP گسترش خواهند یافت. روش‌شناسی و ابزارها از طریق توسعه سه کاربرد صنعتی تأیید می‌شوند: یک پایانه تلفن همراه بی‌سیم-یک سیستم مخابراتی روی تراشه مبتنی بر پروتکل HIPERLANI2 و یک ماژول ضد برخورد برای خودروها. مشکل سخت و دامنه بلندپروازانه شناخته شده بود. اما هفده فصل بعدی که نتایج اصلی به‌دست‌آمده را تشریح می‌کند نشان‌دهنده موفقیت تحقیق است که توسط داوران اروپایی تایید شده است. آن‌ها منتشر شده‌اند تا به بزرگ‌ترین مخاطبان امکان یادگیری و استفاده از آن‌ها را بدهند.

This book presents the perspective of the project on a Paradigm Unifying System Specification Environments for proven Electronic design (PUS SEE) as conceived in the course of the research during 2002 -2003. The initial statement of the research was formulated as follows: The objective of PUSSEE is to introduce the formal proof of system properties throughout a modular system design methodology that integrates sub-systems co-verification with system refinement and reusability of virtual system components. This will be done by combining the UML and B languages to allow the verification of system specifications through the composition of proven sub-systems (in particular interfaces, using the VSIAISLIF standard). The link of B with C, VHDL and SystemC will extend the correct-by-construction design process to lower system-on-chip (SoC) development stages. Prototype tools will be developed for the code generation from UML and B, and existing B verification tools will be extended to support IP reuse, according to the VSI Alliance work. The methodology and tools will be validated through the development of three industrial applications: a wireless mobile terminal-a telecom system-on-chip based on HIPERLANI2 protocol and an anti-collision module for automobiles. The problem was known to be hard and the scope ambitious. But the seventeen chapters that follow, describing the main results obtained demonstrate the success of the research, acknowledged by the European reviewers. They are released to allow the largest audience to learn and take benefit of.