TAILIEUCHUNG - 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 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 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 We denote these two evolutions by p t and p t respectively. We thus have the decomposition p p t p t 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 ESM .

TAILIEUCHUNG - Chia sẻ tài liệu không giới hạn
Địa chỉ : 444 Hoang Hoa Tham, Hanoi, Viet Nam
Website : tailieuchung.com
Email : tailieuchung20@gmail.com
Tailieuchung.com là thư viện tài liệu trực tuyến, nơi chia sẽ trao đổi hàng triệu tài liệu như luận văn đồ án, sách, giáo trình, đề thi.
Chúng tôi không chịu trách nhiệm liên quan đến các vấn đề bản quyền nội dung tài liệu được thành viên tự nguyện đăng tải lên, nếu phát hiện thấy tài liệu xấu hoặc tài liệu có bản quyền xin hãy email cho chúng tôi.
Đã phát hiện trình chặn quảng cáo AdBlock
Trang web này phụ thuộc vào doanh thu từ số lần hiển thị quảng cáo để tồn tại. Vui lòng tắt trình chặn quảng cáo của bạn hoặc tạm dừng tính năng chặn quảng cáo cho trang web này.