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

Model-Based Design for Embedded Systems- P53: 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. | 496 Model-Based Design for Embedded Systems used in both continuous and discrete evolutions. States correspond to the assignment of a value to each variable s V D. A finite set of ports P is then considered. Events correspond to the assignment of a value to a port therefore an event is a pair p d e P x D. Interactions also called labels in the sequel are sets of events. The only restriction is that a given port may yield at most one event in an interaction. Hence interactions are partial mappings A P D. The set of all interactions is denoted by A P D . The empty interaction ep over ports P is the unique mapping ep P D that is undefined for any p e P. Regarding continuous dynamics we restrict ourselves to the case where a unique global physical time is available denoted generically by the symbols t or t and called the universal time. Other time bases can be used but need to be related to this universal time as part of the assertion specification. Investigating the consequences of relaxing this restriction is part of our future work. Similarly for Vc c Vc the domain of continuous evolutions on Vc denoted by C Vc is the set of all functions C Vc def p I p R Vc Dc 15.6 such that we write p t v instead of p t v 1. dom p 0 t for some t 0 where symbol denotes either or call t the duration of p and denote it generically by tv. 2. For every v e Vc t p t v is smooth enough typically at least differentiable on 0 t and possesses a left limit Exit p e DVc defined by Exit p v def lim p t v 15.7 T t Each p e C Vc can be decomposed for all t e 0 t as the concatenation p pi p2 where p1 t p t for0 t t dom pi 0 t p2 t p t t for0 t tv t dom p2 0 tv t 15.8 We denote these two evolutions by p t and p t respectively. We thus have the decomposition p p t p t 15.9 15.3.2 ESM Definition Having defined variables ports labels and interactions it is possible to introduce ESMs as a syntactic means of defining assertions in HRC components. Multi-Viewpoint State Machines 497 Definition 15.1 ESM .