A formal syntax for probabilistic timed property sequence charts

Probabilistic properties are considered as the most important requirements for a variety of software systems, since they are used to formulate extra-functional requirements such as reliability, availability, safety, security and performance requirements. Currently, several probabilistic logics have been proposed to specify such important properties. However, due to the inherent complexity of the underlying temporal logics, these probabilistic logics are rather complex and software developers have problems using them to correctly specify the intended properties. To overcome this problem, we define a formal and graphical property specification language called Probabilistic Timed Property Sequence Charts (PTPSC) which is a probabilistic extension of Property Sequence Charts (PSC). We illustrate the use of PTPSC in the context of a vehicle-to-vehicle communication device for avoiding traffic accidents.