Tham khảo tài liệu 'petri net part 18', kỹ thuật - công nghệ, cơ khí - chế tạo máy phục vụ nhu cầu học tập, nghiên cứu và làm việc hiệu quả | Formalizing and Validating UML Architecture Description of Service-Oriented Applications 501 Fig. 2. Sender-Receiver Model by Algebraic High-Level Net Linear temporal logic Temporal formulas are built from elementary formulas using logical connectives -I and A and derived logical connective V and o universal quantifier V and derived existential quantifier 3 and temporal operators always future Ộ and until U. The semantics of temporal logic is defined on behaviors infinite sequences of states . The behaviors are obtained from the execution sequences of petri nets where the last marking of a finite execution sequence is repeated infinitely many times at the end of execution sequence. For example for an execution sequence Mo Mn the following behavior Ơ Mo . Mn Mn . is obtained where Mi is a marking of the Petri net. Let Ơ Mo Mi . be the behavior where each state Mi provides an interpretation for the variables mentioned in predicates. The semantics of a temporal formula p in behavior Ơ and position j is denoted by ơ j j p. We define For a state formula p ơ j p o Mj p ơ j 1 p o Ơ j p ơ j L p V q o ơ j L p or ơ j L q ơ j Lũ p ơ i L p for all i j ơ j 1 ộp ơ i 1 p for some i j ơ j 1 pUq o 3i j ơ i 1 q and Wj k I ơ k 1 p. Component and connector view Component and connector view was one of the four views proposed in 31 32 which is described as an extension of UML. The component and connector view describes architecture in terms of application domain elements. In this view the functionality of the system is mapped to architecture elements called components with coordination and data exchange handled by elements called connectors. 31 In the component and connector view components connectors ports roles and protocols are modelled as UML stereotyped classes. Each of them is represented by a special type of graphical symbol as summarized in Fig. 3. A component communicates with another component of the same level only through a connector by connections which connect .
