Prover Station - Playground

Playground, a module of Prover Station, is a simple formal verification tool, providing an accessible introduction to formal methods. It allows you to try the HLL language for system modeling and a basic version of the model checker Prover PSL.

Try using the HLL model in the left panel. Look for the 'Proof Obligations' section to see the specific properties stated for that model. When you click the 'Prove' button, you'll instruct the model checker to check whether those properties are valid, that is, always true. You can edit the model or change it completely.

Playground displays the verification status of each property (Proof Obligation or PO) in the 'Results' area. Each property has one of the following outcomes:

• Valid: This indicates the property is always true, meaning no scenario exists where it's false.
• Undecided: Playground couldn't definitively prove or disprove the property. This could be due to:
  • Insufficient information in the model.
  • Overly complex properties requiring simplification.
  • Restrictions in the tool. Contact Prover for a quotation of a more powerful version.
• Falsifiable: Playground identified a scenario where the property is false, providing a counterexample (CEX). This counterexample is displayed under the results for each falsifiable PO.

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.