Back-end Functions:
| Value |
Description |
|---|
| verificationSetup |
Setup the DSVERIFIER_HOME and model checkers visibility (ESBMC or CBMC) in a variable environment |
| verificationParser |
Reads the system in MATLAB form and translate to a ANSI-C file |
| verificationExecution |
Function to get the parameters, system and implementation to start the verification |
| verificationReport |
Shows the report about the verification: successful or failed, and generate the counterexample in .MAT format. |
Verification Functions - Transfer-Function for Open-Loop Systems:
| Value |
Description |
|---|
| verifyOverflow(system, intBits, fracBits, rangeMax, rangeMin, realization, kbound) |
Checks overflow property violation for digital systems using a bounded model checking tool. |
| verifyError(system, intBits, fracBits, rangeMax, rangeMin, realization, error, kbound) |
Checks quantization error property violation for digital systems using a bounded model checking tool. |
| verifyLimitCycle(system, intBits, fracBits, rangeMax, rangeMin, realization, kbound) |
Checks limit cycle property violation for digital systems using a bounded model checking tool. |
| verifyMinimumPhase(system, intBits, fracBits, rangeMax, rangeMin, realization) |
Checks minimum phase property violation for digital systems using a bounded model checking tool. |
| verifyStability(system, intBits, fracBits, rangeMax, rangeMin, realization) |
fChecks stability property violation for digital systems using a bounded model checking tool. |
Verification Functions - Transfer-Function for Closed-Loop Systems:
| Value |
Description |
|---|
| verifyClosedStability(controller, plant, intBits, fracBits, rangeMax, rangeMin, connectionMode) |
Checks stability property violation for closed-loop digital systems using a bounded model checking tool. |
| verifyClosedLoopLimitCycle(controller, plant, intBits, fracBits, rangeMax, rangeMin, realization, kbound, connectionMode) |
Checks limit cycle property violation for closed-loop digital systems using a bounded model checking tool. |
| verifyClosedLoopQuantizationError(controller, plant, intBits, fracBits, rangeMax, rangeMin, realization, kbound, connectionMode) |
Checks quantization error property violation for closed-loop digital systems using a bounded model checking tool. |
Verification Functions - State-Space for Open-Loop Systems:
| Value |
Description |
|---|
| verifyStateSpaceControllability(system, inputs, intBits, fracBits, rangeMax, rangeMin) |
Checks controllability property violation for digital systems (state-space representation) using a bounded model checking tool. |
| verifyStateSpaceObservability(system, inputs, intBits, fracBits, rangeMax, rangeMin) |
Checks observability property violation for digital systems (state-space representation) using a bounded model checking tool. |
| verifyStateSpaceQuantizationError(system, inputs, intBits, fracBits, rangeMax, rangeMin, errorLimit) |
Checks quantization error property violation for digital systems (state-space representation) using a bounded model checking tool. |
| verifyStateSpaceStability(system, inputs, intBits, fracBits, rangeMax, rangeMin) |
Checks stability property violation for digital systems (state-space representation) using a bounded model checking tool. |
Verification Functions - State-Space for Closed-Loop Systems:
| Value |
Description |
|---|
| verifyStateSpaceControllability(system, inputs, intBits, fracBits, rangeMax, rangeMin, K) |
Checks controllability property violation for digital systems (state-space representation) using a bounded model checking tool. |
| verifyStateSpaceObservability(system, inputs, intBits, fracBits, rangeMax, rangeMin, K) |
Checks observability property violation for digital systems (state-space representation) using a bounded model checking tool. |
| verifyStateSpaceQuantizationError(system, inputs, intBits, fracBits, rangeMax, rangeMin, errorLimit, kbound, K) |
Checks quantization error property violation for digital systems (state-space representation) using a bounded model checking tool. |
| verifyStateSpaceStability(system, inputs, intBits, fracBits, rangeMax, rangeMin, K) |
Checks stability property violation for digital systems (state-space representation) using a bounded model checking tool. |
Parameters from the functions:
- system: digital-system represented in transfer-function or state-space format;
- intBits: number of integer bits;
- fracBits: number of fractional bits;
- rangeMax: the maximum dynamical range;
- rangeMin: the minimum dynamical range;
- kbound: the k-bound to be employed during the verification;
- realization: the realization form (delta or direct -forms); delta-forms: DDFI, DDFII and TDDFII; direct-forms: DFI, DFII and TDFII;
- error: the maximum error for quantization-error verification;
- controller: for closed-loop verification, the controller is represented by tranfer-function format;
- plant: for closed-loop verification, the plant is represented by tranfer-function format;
- connectionMode: the connection mode for closed-loop verification; the value must be ‘series’ or ‘feedback’;
- inputs: the inputs matrix used verification for state-space systems;
- K: the feedback matrix used in closed-loop verification for state-space systems;
