KODA Property Definitions

Overview

KODA property definitions allow temporal requirements to be specified directly alongside a task. Properties use a small controlled-language notation designed to describe the observable behaviour of KODA models without exposing the notation of a particular verification backend.

For example:

properties { no_parallel_motion: never drive is running and grip is running;

handle_rejection: if drive.to_position was rejected eventually fstop started;

charging_terminates: if batterymonitoring.charge started eventually batterymonitoring.charge stopped; }

Property definitions are backend independent. A verification backend may translate them to an appropriate formalism, such as LTL for nuXmv or a fixed-point logic for another verification backend.

Observations

Properties are defined over observations of flows, capabilities, and capability events.

The following observations are available:

Notation	Meaning
x is running	x is currently executing.
x started	The trigger of x was accepted successfully.
x was rejected	The trigger of x was rejected or failed to start.
x stopped	The execution of x terminated.
x succeeded	The running execution of x completed successfully.
x failed	The running execution of x completed with failure.
x was aborted	The execution of x was successfully aborted.

Not every observation is valid for every KODA entity. For example, trigger rejection is meaningful for a capability event but not for a capability as a whole. KODA checks observation compatibility during semantic analysis.

Logical and temporal operators

Property expressions can be combined using logical and temporal operators.

KODA	Meaning
not P	P does not hold.
P and Q	P and Q both hold.
P or Q	P or Q holds.
P implies Q	If P holds, Q also holds.
always P	P must hold throughout execution.
never P	P must never hold.
eventually P	P must eventually hold.
next P	P must hold at the next observable KODA step.
P until Q	P must continue to hold until Q occurs.

Property helpers

KODA provides additional constructs for common temporal requirements.

If

The if construct specifies a requirement that must hold whenever an observation occurs.

if drive.to_position was rejected
eventually fstop started

This means that whenever drive.to_position is rejected, fstop must eventually start.

For an LTL backend, this corresponds to:

G(rejected(drive.to_position) -> F(started(fstop)))

Between

The between construct specifies a property that must hold after one observation and until another observation occurs.

between drive.to_position started
and grip.handle started
not batterymonitoring.charge is running

This requires charging to remain inactive after drive.to_position starts and until grip.handle starts.

The terminating observation is required to occur. In an LTL backend, the construct therefore uses strong until:

G(started(drive.to_position) ->
  (!running(batterymonitoring.charge) U started(grip.handle)))

Helpers can be nested. For example:

if fdrive_loop started
between drive.to_position started
and grip.handle started
not batterymonitoring.charge is running

Example

A complete property block may look as follows:

properties {
    no_grip_and_drive:
        never drive is running and grip is running;
 
    handle_drive_rejection:
        if drive.to_position was rejected
        eventually fstop started;
 
    charging_terminates:
        if batterymonitoring.charge started
        eventually batterymonitoring.charge stopped;
 
    abort_stops_drive:
        if fdrive_loop was aborted
        next not drive is running;
 
    no_charging_during_pickup:
        between drive.to_position started
        and grip.handle started
        not batterymonitoring.charge is running;
}

Verification

KODA properties describe model behaviour rather than the syntax of a specific model checker. The KODA compiler resolves property references and validates their observations before they are passed to a verification backend.

A backend is responsible for translating the resulting property representation to the formalism it supports. For example, the nuXmv backend can translate KODA temporal properties to LTL.

This separation allows the same KODA property notation to be used with different verification backends while preserving the meaning of observations defined by KODA.