Features
PSC has been conceived through an accurate analysis devoted to understand what is required in a formalism to express a “useful set” of temporal properties while keeping in mind that easy use and simplicity are mandatory requirements to make a formalism adopted by industries. The mission while defining PSC was to find the “right” balance between expressive power and simplicity of use.
Within the PSC language, a property is seen as a relation on a set of exchanged system messages, with zero or more constraints.
Positive and negative scenarios
PSC may be used to describe both positive scenarios (i.e., the “desired” ones) and negative scenarios (i.e., the “unwanted” ones) for specifying interactions among the components of a system. For positive scenarios, we can specify both mandatory and provisional behaviors. In other words, it is possible to specify that the run of the system must or may continue to complete the described interaction.
Formal semantics
In order to unambiguously determine which execution sequences are allowed or not, PSC has a trace-based denotational semantics, which associates to each PSC the set of all the invalid traces.
Integrated with famous model checkers
The PSC language is corredated by an a tool called PSC2BA. PSC2BA is an automatic transformation of PSC properties in Büchi automata, more precisely in the textual notation called never claim. notation, ready to be used by common model checkers, such as Spin. In this way model checker users can define and use complex temporal properties by simply expressing them in PSC. PSC is more intuitive and closer to their natural language description.
Free to Use
Everybody can use PSC and integrate PSC in its tool. We will be very gratefull to be informed of the use you make of PSC.