Requirement Checker

Note: There is a strong relation between checker and requirement or property . A Checker will check a requirement on a trace. In PLASMA Lab, they are grouped under the same object, heriting from AbstractRequirement . Thus we say that a Requirement verify itself.

But we make a distinction between the Checker/Requirement/Property and the textual content, the requirement/property.

AbstractRequirement

Each Checker inherits from the AbstractRequirement class which inherits from AbstractData. AbstractData describes a container for a data such as a property (but also a model) and provides functions such as getName, getContent and checkForErrors. As this abstract class is quite simple we won't get too much into details and will mostly focus on the AbstractRequirement.

CheckForErrors

checkForErrors come from the AbstractData class. A call to this function will parse the property and initialize any data structure needed before checking the property. If errors were found, the function returns true.

After modifying the property, a single call to checkForErrors is needed before starting a batch of verification (several call to check).

Check

The check function takes an initial InterfaceState as a parameter and check the property from this state. It then returns a double once a decision has been made. Depending on the property language, the number returned may represent a boolean or a value.

Although the simulation is initialized (call to newPath) before starting the verification, the checker is in control of the simulation. During the simulation, the checker will call the simulate method. State are produced on demande. A DeadlockException may be thrown after a call to simulate.

A second version of the check function take an integer as an additional parameter. This parameter, untilStep, tell the checker to verify the simulation until a given step. The purpose of this function is to use it with the simulation mode of PLASMA Lab. Using this mode, the simulation is directly under control of the user. If the verification reach the untilStep bound, the Checker must not call the simulate method. If no decision can be made once the bound has been reached, the Checker can use the NaN constant (Not A Number) with the meaning undecided.

Clean

The clean method is called after an experiment was completed and before a new one start. It is used in case were some operations must be done in order to return to a safe state. It was added to close the CADP proxy (see CADP plugin for more details) in AbstractModel and extended to AbstractRequirement.

Others

The AbstractRequirement provides several others methods and functions.

• setModel set the AbstractModel object to verify.
• getLastTrace retrieves the initial state of the trace currently being checked.
• setSpecificParameters is an optional method whose sole purpose is to facilitate specific parameters to be passed to specific requirements types.

• getOptimizationVariables retrieves optimization variables declared by this property.
• generateInstantiatedRequirement this function instantiates a list of AbstractRequirement from this Requirement and the range of requirement variables declared by it.

For details on optimization variables see the Optimization Variables section in the 2.3 Simulator article.

Requirement variables are similar to Optimization Variables but used to generate a set of requirements instead of a set of initial state.