From a node's contract annotations, it has requirements that can be assumed invariant, and guarantees that have to be shown invariant. Each caller of a node must show it keeps the requirementes of the callee at call site invariant.
Besides these proof obligations from contracts, a node may be annotated with properties that are to be shown invariant under the assumption of the requirements from its contracts.
Every proof obligation of a called node is instantiated at call site as a proof obligation of the calling node. An instantiated proof obligation is less general than the one it is generated from, because it is embedded in the context of the caller.
Only proof obligations of the top node are considered, the proof obligations of sub-nodes are disregarded in the analysis. All proof obligations are considered together, but some verification engines may be able to prove invariance of a subset of the proof obligations before other proof obligations.
To generate proof obligations for a transition system, we exploit instantiation of proof obligations, multi-property verification and information from previous analysis runs in the following way.
For every node with a contract but the top node, add a proof obligation for its requirements. This proof obligation will be not be seen by the analysis, but is instantiated by each caller. The requirements of the top node are assumed to be invariant.
For every node, unless it is abstracted to its contract, add its guarantee as a proof obligation. If the guarantee has been shown in a previous anaysis run, it becomes an invariant instead. If the guarantee remains a proof obligation, it is instantied in each calling node, and is proved together with all other other proof obligations, thus strengthening the analysis. For every node that is abstracted to its contract, add the guarantee as an invariant, since it can only be proved by providing the implementation.
This approach works for any combination of modular and compositional analysis.
A Lustre expression
LustreExpr.t is rewritten to a normal form
in the following ways.
There is exactly one
-> operator at the top of the expression,
thus an expression can be represented as a pair of expressions
(i, t) without
The argument of a
pre operator is always a variable, therefore
pre x operator can be represented by the variable
x at the previous state. A non-variable expression under a
is abstracted to a fresh variable that is defined by this
There are no node calls in a Lustre expression. They are
abstracted out and the results are captured in fresh variables. If
an input parameter of a node contains a
pre operator, the
expression has to be abstracted to a fresh variable.
A Lustre node
LustreNode.t is simplified and rewritten in the
Streams are flattened such that each element of a tuple, a record or an array becomes a separate stream. Constants are expanded in expressions.
An equational definition of a stream becomes an association of the variable of the stream to a Lustre expression as described above, where no temporal operators occur, and all node calls are abstracted out. Each unguarded pre operators is replaced by a fresh constant variable that is an oracle for the initial value.
Assertions are Lustre expressions of Boolean type, properties are abstracted to variables of Boolean type.
When creating simplified Lustre expressions, all node calls are
abstracted such that the return values are assigned to fresh
variables. Further, expressions under a
pre operator and
parameters of node calls that contain a
pre operator are
abstracted to definitions of fresh variables.
The definitions of variables are ordered such that the definition of
x occurs before all definitions that use variable
Each Lustre node is translated to two definitions of fresh uninterpreted predicate symbols over a set of stateful variables of the node. The first predicate constrains the initial values of the variables, the second predicate constrains the set of primed variables as a function of the set of unprimed variables.
A variable is stateful if it is
preoperator in any expression in the node, or
max_depth_input control the abstraction of
the nodes for which a contract is available. Both are constants
and are inputs of the node. When instantiating a node with a
contract, the value of the depth input is the caller's depth input
plus one, meaning that since this node has a contract we are going
down one abstraction level. The max depth input always has the
same value and is passed as an input for the sake of uniformity.
The init / trans predicates are conditional on the depth input. If the value of the depth input is greater than the max depth input, then the contract definition of the node is used instead of the actual init / trans predicate. In this case, lifting the properties of the subnode might not make sense since the actual init / trans predicate is not used. The abstract predicates therefore constrain all the properties to evaluate to true.
Predicates are thus defined as
(depth_input < max_depth_input) => contract and (props = true)
not (depth_input < max_depth_input) => concrete_predicate
If a node call has an activation condition that is not the constant true, additional fresh variables are generated. One variable is initially false and becomes and remains true on the first time the activation condition is true. Further, all input variables are duplicated to shadow input variables that freeze the input values at the last instant the activation condition has been true.
init_flag flag is
true from the first state up to the
state when the clock first ticks, including that state. After that
state, the flag is false forever.
state 0 1 2 3 4 5 ... clock false false true false true false ... init_flag true true true false false false ...
clock and init_flagis true when and only when clock ticks for the first time. The
init_flagflag will be passed down to the called node as its init flag. It is mandatory for invariant lifting: two state invariants are guarded by
init_flag or inv, and substitution takes care of rewriting that as
clock => init_flag or inv.
The initial state constraint of the called node is a conjunction of formulas representing the following:
init_flagflag is true (see paragraph above):
init_flag = true
clock => shadow_input = actual_input
clock => init(init_flag,args)
not clock => out = default
init_flagflag is true in the current state iff it was true in the previous instant and the activation condition was false in the previous instant:
init_flag' = init_flag and not clock
and their previous values if the activation condition is false. More generally, all the arguments of the subnode init/trans stay the same:
clock' => shadow_input' = actual_input'
not clock' => (args' = args)
init_flagflag is true in the next step:
(clock' and init_flag') => init(init_flag',args')
init_flagflag is false in the next step.
(clock' and not init_flag') => trans(init_flag',args',init_flag,args)
val trans_sys_of_nodes :
LustreNode.t SubSystem.t ->
Analysis.param -> TransSys.t * LustreNode.t SubSystem.t