Patrizio Pelliccione

Dipartimento di Informatica, Università degli Studi dell'Aquila
Via Vetoio, I-67010 L'Aquila (Italy)

Property Sequence Charts (PSC)



PSC is a simple but expressive graphical formalism for specifying temporal properties. Two are the main requirements of PSC, simplicity and expressiveness. Remaining close to the graphical notation of UML2.0 Sequence Diagrams, the requirement of simplicity is satisfied. The PSC expressiveness is measured with the property specification patterns. PSC describes interactions between a collection of components that can be simultaneously executed and that communicate by message passing. PSC distinguishes among three different types of messages called arrowMSGs (see Figure 1.a). Regular messages: the labels of such messages are prefixed by "e:". They denote messages that constitute the precondition for a desired (or an undesired) behavior. It is not mandatory for the system to exchange a Regular message; however, if it happens the precondition for the continuations has been verified. Required messages: are identified by "r:" prefixed to the labels. It is mandatory for the system to exchange this type of messages. Fail messages: the labels are prefixed by "f:". They identify messages that should never be exchanged. Fail messages are used to express undesired interactions. We also define Constraint operators that impose "restrictions" on the set of messages (called intraMSGs) possibly exchanged between the considered message and its predecessor or successor (the predecessor of the first message of a PSC is the startup of the system). Restrictions specify either a chain of intraMSGs or a boolean formula (over a set of intraMSG labels). Parallel, Loop, and Simultaneous operators are introduced with a UML 2.0 like graphical notation.