When a property (Proof Obligation or PO) is falsified, Playground provides a step-by-step explanation to help you understand why. This explanation starts by:

• Displaying the original equation representing the PO.
• Clearly stating why the PO is false, by breaking down the equation, showing the values of each component.

Playground then delves deeper by:

• Identifying a specific part of the equation that contributes to the falsification.
• Repeating steps 1-3 for the chosen part, continuing until:
  • An input value (from the “Inputs” section) is reached.
  • A literal (a basic value like true or false) is reached.

This process helps you pinpoint the exact source of the falsification within your model.

In some counterexamples, Playground might analyze multiple time steps to identify the source of the falsification. This information is indicated by '[depth n]', where n represents the specific time step being examined. For example, '[depth 1]' signifies that the analysis is focused on the second time step.

Playground supports the user-friendly language HLL (High-Level Language) specifically designed by Prover for formal verification. Here's a quick description of its components to help you build your own model:

Structure:

HLL models are organized into distinct sections (you can repeat all the sections):

• Constants: Define variables with values that do not vary over time.
• Types: Create custom data types for more complex variable definitions.
• Inputs: Specify the system's inputs.
• Outputs: While not used by Playground itself, you can define system outputs for your own reference.
• Constraints: Set up equations to restrict the possible values of variables.
• Declarations: Declare new variables within your system.
• Definitions: Define the behavior of your system by assigning values to variables.
• Proof Obligations: List the properties you want to verify about your model.
• Namespaces

Execution flow:

At each time step:

• Inputs: All inputs are read.
• Constraints:All defined constraints are evaluated and used as assumptions.
• Variable update: All declared variables are updated simultaneously.
• Outputs and Proof Obligations: Outputs are calculated, and proof obligations are evaluated based on the updated system state.

Tips for writing HLL models:

• Start simple: Begin with basic models to grasp the language and build confidence.
• Utilize examples: Explore Playground's pre-defined models for reference and inspiration.
• Document your model: Clearly explain your model's structure and logic for future reference and collaboration.
• Use online resources: Use the HLL cheat sheet or the HLL Language Definition Document to understand all the constructions of the language.

Prover Station Playground contains a limited version of Prover PSL, provided to you as a way to try out the language HLL and the capabilities of Prover PSL. It is intended for evaluation purposes and training only. For production use, please contact Prover to license the more powerful complete version of Prover PSL.

If you need a trusted model checker for your safety case, you can purchase a license for Prover Certifier. It contains Prover PSL but offers also complimentary checks that make the result trustworthy to the highest software integrity levels. Prover Certifier has been approved by TÜV NORD as a CENELEC EN50128-compliant T2 tool for SIL4 applications.