TAILIEUCHUNG - Model-Based Design for Embedded Systems- P11

Model-Based Design for Embedded Systems- P11:The unparalleled flexibility of computation has been a key driver and feature bonanza in the development of a wide range of products across a broad and diverse spectrum of applications such as in the automotive aerospace, health care, consumer electronics, etc. | 276 Model-Based Design for Embedded Systems terms of the resulting language. We have tested this simulation approach in SystemC 49 Java 3 and C with a thread library. In addition we have devised a service-based formalism 62 that can effectively integrate models specified at different abstraction levels in different specification languages and with different MoCs. We also enhanced our simulation tool to support the co-simulation of these heterogeneous models. Further this service-based formalism became the foundation of the second generation of the Metropolis environment covered in Section . Formal Property Verification Both academia and industry have long studied formal property verification but the state-explosion problem restricts its usefulness to protocols and other high abstraction levels. At the implementation level or other low abstraction levels hardware and software engineers have used simulation monitors as basic tools to check simulation traces while debugging designs. Verification languages such as Promela which are used by the Spin model checker 28 allow only simple concurrency modeling and are not amenable to the system design specification which requires complex synchronization and architecture constraints. In contrast Metropolis with its formal semantics automatically generates verification models for all the levels of the design 15 . our translator automatically constructs the Spin verification model from the MMM specification taking care of all system-level constructs. For example it can automatically generate a verification model for the example in Figure and verify the medium s nonoverwriting properties. Further as the translator refines the design through structural transformation and architectural mapping it can prove more properties including throughput and latency. This kind of property verification typically requires several minutes of computation on a GHz Xeon machine with 1 Gbyte of memory. When the state space .

• Quản trị mạng
• Hành trình mạng không dây
• mạng WiFi
• khắc phục sự cố mạng
• chia subnet
• giáo trình mạng máy tính
• Nhiễu kỹ thuật
• kết nối mạng không dây
• mạng không dây
• Các kỹ thuật kết nối mạng không dây
• công nghệ thông tin
• hệ điều hành
• kỹ thuật lập trình
• quản trị mạng
• WiFi
• WiMax
• Lập trình web Internet
• mạng máy tính
• tài liệu mạng máy tính
• chuyên ngành mạng máy tính
• câu hỏi về mạng máy tính
• giáo trình mạng cisco