Objective Definition File

An objective definition file is a TOML file used to create an objective in the Modality CLI.

Objectives encode an experimental design for Modality's experiment automation functionality. You can also test an objective's measurements against previously-recorded sessions. For guidance on designing and applying objectives, see How to Create an Objective.

Objectives have three main parts: mutation constraints, measurements, and stopping conditions.

# Table of Contents

# Objective Name

name
Required
string
The global human-oriented name of the objective.

Example Objective Name

# sample-objective.toml
name = "sample objective"

# Mutation Constraints

Mutation constraints provide guidance for what mutations to perform. This allows Modality to rapidly explore the space of system states relevant to your experiment.

# Global Mutation Constraints

mutation_constraints
Optional
table
Global mutation constraints. May include max_concurrent_mutations, mutation_precondition, and mutator_tags.
  • max_concurrent_mutations
    Optional
    integer
    Maximum number of mutations to perform at the same time.
  • mutation_precondition
    Optional
    string
    Trace expression to be used as a global precondition for the triggering of any generated mutation. Mutually exclusive with per-mutator precondition constraints.
  • mutator_tags
    Optional
    array
    Optional array of strings. Only consider mutators which have at least one of the specified tags.

Example Global Mutation Constraints

# Global mutation constraints
[mutation_constraints]

# Only perform 1 mutation attempt per mutation-epoch
max_concurrent_mutations = 1

# A global precondition trace expression to be used as a
# causal prefix for the triggering of any generated mutation
mutation_precondition = 'SYSTEM_STATE_READY@MONITOR'

# Only consider mutators which have at least one of the specified tags
mutator_tags = ['drone', 'environmental-forces', 'simulator']

# Per-Mutator Mutation Constraints

mutator
Optional
array of tables
Defines per-mutator constraints. May include name, probe, mutation_precondition, and param_constraints.
  • name
    Required
    string
    The mutator name.
  • probe
    Optional
    string
    Restrict mutations to a specific probe (in cases where this mutator is used at multiple probes).
  • mutation_precondition
    Optional
    string
    Mutator specific trace expression to be used as a precondition for the triggering of any generated mutation. Mutually-exclusive with global [mutation_constraints.mutation_precondition].
  • param_constraints
    Optional
    table
    Constraints on potential mutation parameter values for this mutator. May include name, range, or enum_options.
    • name
      Required
      string
      Name of the mutator parameter to constrain.
    • range
      Required
      array
      Not permitted for boolean or enum types. Array of length 2. Range of values for the parameter. It is an error if range is not contained within the hard_range for this parameter.
    • enum_options
      Varies
      array
      Required for enum types, otherwise not permitted. Array of strings. Set of values for the parameter.

Example Per-Mutator Mutation Constraints

# Per-mutator mutation constraints
[[mutator]]
name = 'simulation-environment-mutator'

# Restrict mutations to the specific probe SIM_MUTATOR_PLUGIN
probe = 'SIM_MUTATOR_PLUGIN'

# Mutator specific precondition trace expression to be used as a
# causal prefix for the triggering of any generated mutation
# I.e., Wait until the drone altitude (in the simulator) has reached 
# 20 meters before performing mutations
mutation_precondition = 'SIM_ALTITUDE@GAZEBO_MUTATOR(_.payload > 20)'

# Constrain the impact force to [0.1, 30.0] Newtons
[[mutator.param_constraints]]
name = 'impact-force-magnitude'
range = [0.1, 30.0]

# Constrain the impact force link to either ROTOR_0 or ROTOR_1
[[mutator.param_constraints]]
name = 'impact-force-location-link'
range = ['ROTOR_0', 'ROTOR_1']

# Measurements

Measurements allow you to see how your system reacts to the different states it is put in. Measurements are Modality queries that are recorded for each set of mutations.

measurement
Required
array of tables
Required array of tables that must contain at least one table. Measurements to take for each set of mutations.
  • name
    Required
    string
    The human-oriented name of this measurement.
  • check
    Required
    string
    The trace expression for this measurement, which will be given to check. This expression is parsed and sanity-checked when the objective is created in the CLI with modality objective create.
  • stopping_conditions
    Optional
    table
    Optional stopping conditions specific to this measurement. May contain passing_measurements and/or failing_measurements.
    • passing_measurements
      Optional
      integer
      Number of attempts where this measurement passed.
    • failing_measurements
      Optional
      integer
      Number of attempts where this measurement failed.

Example Measurements

# This measurement fails if any failure-like events with severity > 8 occur
[[measurement]]
name = 'No critical events occur'
# Measurement-specific stopping condition
# stop immediately if this check doesn't pass
failing_measurements = 0
# The trace query expression to check
check = 'NEVER *@*(_.severity > 8)'

# This measurement checks that we only observe up to 5 low severity events
[[measurement]]
name = 'Tolerate up to 5 low severity events'
check = '''
FOR AGGREGATE 
    *@*(_.severity <= 3) AS LowSeverityEvents
VERIFY
    count() <= 5
'''

# This measurement checks that the IMU gyroscope instability metric is nominal
[[measurement]]
name = 'IMU gyroscope instability is acceptable'
check = '''
FOR AGGREGATE
    IMU_GYRO_INSTABILITY@PX4_VEHICLE_IMU(_.payload != 0.0) AS GyroInstability
VERIFY
    max(GyroInstability.payload) < 0.45,
    mean(GyroInstability.payload) < 0.2,
    stddev(GyroInstability.payload) < 0.1
'''

# This measurement checks that the unsafe tilt detection and reaction 
# mechanisms occur as expected
[[measurement]]
name = 'The system successfully detects unsafe tilt and terminates flight'
# Additional measurement-specific stopping conditions may be specified
# passing_measurements = 1
check = '''
FOR EACH
    # Either roll or pitch is in bounds for the tilt detector
    *@*((_.event = "IMU_ROLL" OR _.event = "IMU_PITCH") AND (_.payload > 45 OR _.payload < -45)) AS ExcessiveTilt
VERIFY
    ExcessiveTilt -> UNSAFE_TILT_DETECTED@PX4_COMMANDER -> FLIGHT_TERMINATED@PX4_COMMANDER
'''

# Stopping Conditions

Stopping conditions give you different ways to specify when to stop generating new runs of your experiment.

stopping_conditions
Optional
table
Global stopping conditions. Multiple conditions will be combined with OR so that any condition being met stops the mutation generator.
  • attempts
    Optional
    integer
    Number of sets of simultaneous mutations to attempt.
  • time
    Optional
    string
    Total time running this objective.
  • passing_measurements
    Optional
    integer
    Number of attempts where all the measurements passed.
  • failing_measurements
    Optional
    integer
    Number of attempts where all the measurements failed.

Example Stopping Conditions

# Global stopping conditions, combined together with OR
[stopping_conditions]

# Maximum number of related mutation-epoch attempts
attempts = 50

# Maximum wall-clock time of related mutation-epoch attempts
time = "2h 15min"

# Maximum number of times all the measurements passed
passing_measurements = 10

# Maximum number of times not all the measurements passed
failing_measurements = 5

# Example Objective Definition

# sample-objective.toml

name = "sample objective"

# GLOBAL MUTATION CONSTRAINTS

[mutation_constraints]
# Only perform 1 mutation attempt per mutation-epoch
max_concurrent_mutations = 1
# Only consider mutators which have at least one of the specified tags
mutator_tags = ['drone', 'environmental-forces', 'simulator']
# A global precondition trace expression to be used as a
# causal prefix for the triggering of any generated mutation
mutation_precondition = 'SYSTEM_STATE_READY@MONITOR'

# PER-MUTATOR MUTATION CONSTRAINTS

# For more information about this mutator, see its definition
# in modality-sut/sample_component/mutators/sim-env.toml
[[mutator]]
name = 'simulation-environment-mutator'
# Restrict mutations to the specific probe SIM_MUTATOR_PLUGIN
probe = 'SIM_MUTATOR_PLUGIN'
# Mutator specific precondition trace expression to be used as a
# causal prefix for the triggering of any generated mutation
# I.e. Wait until the drone altitude (in the simulator) has reached
# 20 meters before performing mutations
mutation_precondition = 'SIM_ALTITUDE@GAZEBO_MUTATOR(_.payload > 20)'
# Constrain the impact force to [0.1, 30.0] Newtons
[[mutator.param_constraints]]
name = 'impact-force-magnitude'
range = [0.1, 30.0]
# Constrain the impact force link to either ROTOR_0 or ROTOR_1
[[mutator.param_constraints]]
name = 'impact-force-location-link'
range = ['ROTOR_0', 'ROTOR_1']

# MEASUREMENTS

# Measurement fails if any failure-like events with severity > 8 occur
[[measurement]]
name = 'No critical events occur'
# Measurement-specific stopping condition
# Stop immediately if this check doesn't pass
failing_measurements = 0
# The trace query expression to check
check = 'NEVER *@*(_.severity > 8)'

# Measurement checks that we only observe up to 5 low severity events
[[measurement]]
name = 'Tolerate up to 5 low severity events'
check = '''
FOR AGGREGATE 
    *@*(_.severity <= 3) AS LowSeverityEvents
VERIFY
    count() <= 5
'''

# Measurement checks that the IMU gyroscope instability metric is nominal
[[measurement]]
name = 'IMU gyroscope instability is acceptable'
check = '''
FOR AGGREGATE
    IMU_GYRO_INSTABILITY@PX4_VEHICLE_IMU(_.payload != 0.0) AS GyroInstability
VERIFY
    max(GyroInstability.payload) < 0.45,
    mean(GyroInstability.payload) < 0.2,
    stddev(GyroInstability.payload) < 0.1
'''

# This measurement checks that the unsafe tilt detection and reaction 
# mechanisms occur as expected
[[measurement]]
name = 'The system successfully detects unsafe tilt and terminates flight'
# Additional measurement-specific stopping conditions may be specified
passing_measurements = 1
check = '''
FOR EACH
    # Either roll or pitch is in bounds for the tilt detector
    *@*((_.event = "IMU_ROLL" OR _.event = "IMU_PITCH") 
    AND (_.payload > 45 OR _.payload < -45)) AS ExcessiveTilt
VERIFY
    ExcessiveTilt -> UNSAFE_TILT_DETECTED@PX4_COMMANDER 
    -> FLIGHT_TERMINATED@PX4_COMMANDER
'''

# GLOBAL STOPPING CONDITIONS

[stopping_conditions]
# Maximum number of related mutation-epoch attempts
attempts = 50
# Maximum wall-clock time of related mutation-epoch attempts
time = "2h 15min"
# Maximum number of times all the measurements passed
passing_measurements = 10
# Maximum number of times not all the measurements passed
failing_measurements = 5