devel:verification:refinement

This notion is similar to 1-way conformation but without flaws. It is based on Def. 6.1 of [1].

An STG is defined as a tuple *N = (P, T, W, M _{N} , In, Out, Int, l),* where

**Deﬁnition 6.1. (Correct Implementation with Internal Signals)**
A deterministic STG *C* (with internal signals) is a *correct implementation* of an STG *N* without internal signals if *In _{C} ⊆ In_{N}, Out_{C} = Out_{N}, Int_{C} ∩ Ext_{N} = ∅,* and for all

(IC1) There is a trace *v* of *C* such that *M _{C}[v»* with

For every trace *v* of *C* such that *M _{C}[v»M′* with

(IC2) If *a ∈ In _{N}* and

(IC3) If *x ∈ Out _{N}* , then

A *violation witness* is a reachable marking *(MC,MN)* of *C×N* such that some of the following conditions holds:

*MN[a±»*(can replace by*MN[a±>*), where*a±*is an input of*N*that is not ignored by*C*, and*¬MC[a±»*(where the enabledness is via dummies*but not*internal; if we know that in*C*no internal signal can trigger an output, e.g.*C*is input-proper, then can replace this by enabledness via dummies*and*internal).

**Note:**this requirement always holds (and thus does not have to be checked) if*C*is a circuit-STG, provided that the initial states of inputs are the same in both STGs.*MN[x±»*(can replace by*MN[x±>*), where*x±*is an output of both*N*and*C*, and*¬MC[x±»*(where the enabledness is via dummies and internal).

**Note:**this requirement makes refinement relation different from 1-way conformation, and so one can drop it if, e.g., a concurrency reduction has been performed.*MC[x±»*(can replace by*MC[x±>*), where*x±*is an output of both*N*and*C*, and*¬MN[x±»*(where the enabledness is via dummies and internal).

If some of the transformations required for *refinement* check are skipped, then the same REACH expression can be used to verify a weaker *1-way conformation* property (it allows removing traces, e.g. due to concurrency reduction). Such transformation steps that need to be skipped are annotated in brackets.

- We assume that both STGs are input-proper.
- We assume that both STGs are output-determinate whatever the interpretation of internal signals is (as dummies or as outputs). we likely have to require full determinacy, not just output-determinacy, e.g. if one makes the STG for (a|b)+(a|c) with all signals being inputs and a choice implemented by two dummy transitions which are then contracted, the resulting output-determinate but not determinate STG will not be a refinement of itself and will fail the test below.
*In*and_{C}⊆ In_{N}*Out*._{C}= Out_{N}

- Replace internal signals by dummies for:
- in N
- in C (skip this step for 1-way conformation check)

- Compose the two STGs using PCOMP with option
`-o`

to enable composing outputs. - Add shadow transitions into the composition for:
- all inputs of N known to C (skip this step if C is a circuit-STG and the initial states of input signals are the same in both STGs)
- all outputs of N (skip this step for 1-way conformation check)
- all outputs of C

- Add a choice place for all shadow transitions; this is to enforce consistency and simplify unfolding.

Check the following REACH property on the modified composition STG:

// Check whether one STG (implementation) refines another STG (specification). // The enabled-via-dummies semantics is assumed for @, and configurations with maximal // dummies are assumed to be allowed - this corresponds to the -Fe mode of MPSAT. let // Names of all shadow transitions in the composed STG. SHADOW_TRANSITIONS_NAMES = {"a+", "a-", "x+/1", "x-/2", ""} \ {""}, SHADOW_TRANSITIONS = gather n in SHADOW_TRANSITIONS_NAMES { T n } { // Optimisation: make sure shadow events are not in the configuration. forall e in ev SHADOW_TRANSITIONS \ CUTOFFS { ~$e } & // Check if some signal is enabled due to shadow transitions only, // which would mean that some condition of violation witness holds exists s in (INPUTS + OUTPUTS) { let tran_s = tran s { exists t in tran_s * SHADOW_TRANSITIONS { forall p in pre t { $p } } & forall tt in tran_s \ SHADOW_TRANSITIONS { ~@tt } } } }

In many practical cases if the grants of a mutex are internal, hiding them will result in an non-output-determinate STG. E.g. if we take a mutex STG and buffer the grants, so that the mutex grants become internal and the outputs of buffers become outputs – then executions `r1+;r2+;(g1+)`

and `r1+;r2+;(g2+)`

have the same projections on the visible signals but enable different outputs (`buf1+`

and `buf2+`

, respectively).

Hence we handle an STG with *K* mutex places as an abbreviation for a product of *K* mutex STGs with the original STG, i.e. in a hierarchical model one more level of hierarchy is introduced. Conjecture: the mutex implementability check then implies the N-way conformation passes. Note that this should be checked for both strict and relaxed mutex protocols.

If there is no solution reported by MPSat, then the property holds.

If a solution (or a collection of solutions) is reported for the composition STG with shadow transitions, then the following processing of each violation trace needs to be performed:

- Project the violation of the composition STG to the original implementation STG. Use PCOMP composition details in
`details.xml`

and dummy substitutions map. - Determine unexpectedly enabled and unexpectedly disabled interface signals. Use MPSAT
*continuations*to identify in the signal enabledness after the violation trace via dummies.

Copyright © 2014-2021 workcraft.org