PSC is a simple but expressive language 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 and Message Sequence Charts (MSC), the requirement of simplicity is satisfied. The PSC expressiveness is measured with the property specification patterns.
PSC facilitates the non trivial and error prone task of specifying, correctly and without expertise, temporal properties. A PSC property 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.
Required messages: the labels of such messages are prefixed by "r:" prefixed to the labels. It is mandatory for the system to exchange this type of messages.
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.
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 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).
Parallel, Loop, and Simultaneous operators are introduced with a UML 2.0 like graphical notation.