The Bio-jETI Framework - User-Level Workflow Design: A Bioinformatics Perspective - page 43

established in programming language compilers in the last decades [23] and
that has been shown to be realizable via model checking [293, 294, 295, 273]
can be applied. By providing a predefined set of desirable process properties to
the model checker, it is for instance possible to achieve a thorough monitoring
of safety and liveness properties within the framework. Similar to the built-
in code checks that most Integrated (Software) Development Environments
provide, this would help Bio-jETI users to avoid the most common mistakes at
workflow design time. Examples for data-flow-related errors whose detection
requires awareness of the whole model are manifold, ranging from undefined
variables or simple type mismatches to computational gaps and incomplete
processes.
As has been shown in [168, 171], intra procedural data-flow analysis via
model checking can in fact be carried out directly in the jABC framework
using the GEAR model checking plugin once atomic propositions are available
that describe which data a SIB reads (uses) and writes (defines). For instance,
an atomic proposition use(x) can be added to a SIB to express that a data
item x is used by the service, or def(x) to state that it is written (defined).
Based on such atomic propositions, it can now, for example, be checked that
a service can not use an input x unless it has been defined. In terms of the
GEAR syntax, this can be expressed as:

AWU ( ¬ “use(x)” , “def(x)” )

This is already sucient to ensure that the variable x has been defined,
but does not say anything about type correctness. As described in greater
detail in [174], it is therefore reasonable to extend the atomic propositions
and the constraints in order to include the types of the involved variables.
Accordingly, a formula like:

( “use(x)” ∧ “type(x)=y” ) ⇒ ASU ( ¬ “def(x)” , “def(x)” ∧ “type(x)=y” )

can be used to express that if a service uses x of type y , x must have been
defined before with precisely this type, without having been overwritten since.
It is of course possible to analyze other data-flow properties simply by pro-
viding the appropriate constraints. For a more comprehensive description of
data-flow analysis via model checking in the jABC in general and on Bio-jETI
workflows in particular, the reader is referred to [171] and [174], respectively.
As shown in detail in [173, 174], model checking of data-flow properties can
in fact help to detect common technical problems, like:

• Undefined data identifiers: a service uses a data item that has not been

produced before.

• Missing computations: a workflow step is missing, so that a required re-

source is not fetched/produced.

• Type mismatches: a certain service is not able to work on the data format

provided by its predecessor(s).