|
|
|||
|
||||
OverviewAn embedded system is loosely defined as any system that utilizes electronics but is not perceived or used as a general-purpose computer. Usually, 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. This book presents a formal approach to high-level equivalence analysis, opening design exploration avenues that offer new possibilities. It is a work that can stand alone but at the same time is compatible with synthesis and simulation frameworks. Full Product DetailsAuthor: Harry Hsieh , Felice Balarin , Alberto L. Sangiovanni-VincentelliPublisher: Springer Imprint: Springer Edition: 2001 ed. Dimensions: Width: 15.50cm , Height: 1.10cm , Length: 23.50cm Weight: 0.880kg ISBN: 9780792372622ISBN 10: 079237262 Pages: 136 Publication Date: 31 December 2000 Audience: College/higher education , Professional and scholarly , Postgraduate, Research & Scholarly , Professional & Vocational Format: Hardback Publisher's Status: Active Availability: In Print This item will be ordered in for you from one of our suppliers. Upon receipt, we will promptly dispatch it out to you. For in store availability, please contact us. Table of Contents1. Introduction.- 1. Emergence of Embedded Systems.- 2. Design of Embedded Systems.- 3. Requirements For An Effective Design Methodology.- 4. Proposed Design Approach.- 5. Motivation.- 6. Overview.- 2. The Polis Codesign Framework.- 1. The Polis Codesign Methodology.- 3. Codesign Finite State Machines.- 1. Background.- 2. CFSMs: Semantics.- 3. Mathematical Model.- 4. Formal Verification of CFSM Specifications.- 1. Verification Methodology.- 2. Verification Example: Seat Belt Alarm Controller.- 3. Verification Example: Shock Absorber Controller.- 4. Conclusions.- 5. Synchronous Equivalence.- 1. Motivation.- 2. The Synchronous Assumption and Synchronous Equivalence.- 3. Design Exploration Methodology.- 4. Analyzing Synchronous Equivalence.- 6. Static Equivalence Analysis.- 1. Scheduling Policy Analysis.- 2. System Graph Analysis.- 3. Mixed Analysis.- 4. Analysis of Heterogeneous Architectures.- 5. Conclusions.- 7. Communication Analysis.- 1. Execution Trace.- 2. Abstracting Communication.- 3. Conclusions.- 8. Refining Communication Analysis.- 1. Container Refinement.- 2. State Refinement.- 3. Pruning Execution Covers.- 4. Relationship with Exact Simulation.- 9. Conclusions and Future Directions.- 1. Conclusions.- 2. Future Directions.ReviewsAuthor InformationTab Content 6Author Website:Countries AvailableAll regions |