TAILIEUCHUNG - Model-Based Design for Embedded Systems- P54

Model-Based Design for Embedded Systems- P54: 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. | 506 Model-Based Design for Embedded Systems Products in Terms of Guards and Actions We return now to our formalism of ESM where products are naturally defined. The above mathematical syntax for HRC state machines induces a corresponding mathematical syntax for ESMs. Accordingly the product of two ESMs E Ei x E2 is refined as follows invariants 1 11 A 12 guards y y1 A y2 actions a proj-L. ai n proj-. a2 This formula has several interesting special cases If yi i 1 2 involves only ports of type pure then y1 A y2 in Equation expresses that the two ESMs must synchronize on their shared ports. If ii i 1 2 involves only flows then 11 A 12 in Equation denotes the system consisting of the continuous evolutions for the two ESMs. If yi i 1 2 involves only ports x y z where y is shared and has the form 71 y f x Y2 z g y then Y1 A 72 in Equation denotes the conjunction of y f x and z g y . This case captures the composition mechanism of dataflow formalisms thus the composition mechanism of dataflow formalisms is supported by guards not by actions. Note that the dependency of z on x through y is immediate that is involves no logical delay. If yi i 1 2 has the form 71 y f x 72 z g vy where y is a port and Vy is a state variable storing the value of y at previous transition a2 Vy y then 71 A 72 introduces a logical delay in the composition of the two systems. Thus we see here a simple syntactic condition to ensure the existence of a logical delay from input ports to output ports while composing two ESMs. Multi-Viewpoint State Machines 507 Categories as Specialization of HRC State Machines We now specialize our model of HRC state machine into several categories of assertions or viewpoints generically denoted by the symbol r. This is achieved by 1. Restricting the subset of ports and variables that characterize a category formally we define subsets Pr c P and Vr C V. 2. Specializing how the two transition relations p and 6 restrict to these ports

• Phần cứng
• sửa chữa máy tính
• sổ tay phần cứng
• MainBoard
• thiết bị máy tính
• thiết bị mạng
• lắp ráp máy tính
• Phần cứng máy tính
• lỗi máy tính
• hệ thống mạch máy tính
• điện máy tính
• Tài liệu máy tính