[aadl]: [AADL Forum] Some issues on error propagation paths in EMV2

[Denis Buzdalov]

Brian,

> Are you talking about consistency rules C5-7 in E.7.3?

Unfortunately, the document we use has extremely bad numbering
(spaghetti numbering like in AS5506C), so I can't say yes or no to you.
If you sent the version of document you use, I would answer clearer.

> I agree that they could be expressed more clearly.  Actually, I'd
> like to get rid of error_containment entirely, because it's both
> unnecessary, and possibly contradictory.
>
> I vaguely remember weakly objecting to error_containment at the time
> with Peter insisting that explicitly stating what error types will
> not occur had value.  All types not expressly out propagated are
> contained; all types not expressly in propagated are unexpected.

Yes, the original question was what should we understand under
"unspecified" error types if we have explicitly "propagated" ones and
explicitly "not propagated", i.e. "contained" ones.

But, again and again, looking at the _process_ of models development, it
is really important sometimes to express that some error types _cannot_
be propagated just to specify that this or that component is _intended_
to manage some kinds of errors. This is really useful both for final
consistency checks and for analysis of partial models. Correct me if
you think I'm wrong.

> Here are my suggestions for improvement:
> 
> (C5) All error types out propagated by a propagated by a propagation
> path source, must be in propagated by its destination.

Oh, my internal parser has broken down at this sentence. Did you mean
that propagated error types set at the destination side must be a
superset of propagated error types set at the source side? I.e.
$p_d \supseteq p_s$ or samely $p_s \subseteq p_d$ in our denotions.
If yes, it is the first legality rule, in fact.

> (C6) Error type sets of error propagation and error containment must
> be disjoint for both error propagation path sources and destinations.

Did you mean "respectively" here?
I.e. $p_s \cup c_d = \varnothing$ in our denotions.
If yes, it is the first statement of the first consistency rule, which
is a consequence of definitions.

So, if both are yes, then (as it was discussed in the last paragraph of
section 4.4 in the whitepaper) only definitions and two legality rules
(i.e. the very beginning of the table in the whitepaper) are enough to
express all needed limitations on sets of propagation paths. And, these
statements also do not use the "unspecified" notion. It means, that
there's no need in consistency and semantic rules in this section at all.

--
Denis Buzdalov
Software Engineering Department, ISPRAS