Đang chuẩn bị liên kết để tải về tài liệu:
Model-Based Design for Embedded Systems- P32

Model-Based Design for Embedded Systems- P32: This book contains information obtained from authentic and highly regarded sources. Reasonable efforts have been made to publish reliable data and information, but the author and publisher cannot assume responsibility for the validity of all materials or the consequences of their use. | 276 Model-Based Design for Embedded Systems terms of the resulting language. We have tested this simulation approach in SystemC 2.0 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 10.4. 10.3.3.2 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 10.2 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 1.8 GHz Xeon machine with 1 Gbyte of memory. When the state space .