Runtime checking

Verification can be used to make sure a model does not include errors. Some errors are tied to the specificities of a model, whereas others are more generic. Generic ones can be verified no matter which model is to be verified. As for errors related to models themselves, we provide a feature allowing the modeler to express specific properties about its models.

Those properties can be checked during simulation, at runtime. Albeit this feature is not meant to perform an exhaustive exploration of all possible states of a model, invalid states can eventually be detected during an iteration of the modeling and simulation process.

The Verifiable mixin provides the runtime verification framework. Classes including this module holds a reference to components encapsulating user-defined rules used to test properties (i.e. RuntimeChecker). The modeler can specialize this component or use a predefined subclass.

Verifications are triggered after each state transition, during simulation. For performances reasons, this features is disabled by default and can be switched through simulation configuration.

Example

To illustrate the use of runtime verifications, let's consider a compass model. Its state is defined by a "north" angle value (expressed in degrees), representing the direction the compass is pointing to. As it is representing an angle in degrees, values should always be in the [0,360[ range.

The closest primitive data type able to represent such value is a 2 bytes integer, or Int16, which encompasses the allowed range. A check keyword with the numericality option can be used to verify that the angle is valid using the provided NumericalityChecker:

class Compass < Quartz::AtomicModel
  state_var north : Int16 = 90
  check north, numericality: {greater_than: 0, lesser_than: 360}
end

If a state transition assigns an invalid value to @north during simulation with the runtime verification option enabled, the error is catched.

If the verification mode is non-strict, the error is logged as follows:

(10:17:51:273) > ’compass’ is invalid (context: ’internal’ transition). Errors: ['north' must be greater than or equal to 0]

If the verification mode is in strict mode, a StrictVerificationFailed error is raised (strict: true should be specified as an attribute of the check keyword).

Note you can give a contextual hint on when to apply a verification (e.g. after a given transition or after a set of transitions), via the on: attribute, as follows:

check north, numericality: {greater_than: 0, lesser_than: 360}, on: :internal

Valid contexts are :internal, :external, :confluent and :init. Several contexts can be passed as an array, as follows:

check north, numericality: {greater_than: 0, lesser_than: 360}, on: [:internal, :external]

Custom checker

If the provided runtime checkers does not satisfy the modeler verification needs, a custom checker can be defined and used via the check_with keyword, as follows:

class CustomChecker < Quartz::Verifiers::RuntimeChecker
  def check(model)
    if domain_specific_test
      model.errors.add(:phase, "must satisfy a domain specific need.")
    end
  end
end

class MyModel < Quartz::AtomicModel
  check_with CustomChecker
end

---

Next: Underlying theory