Questions and Remarks on slides about Runtime Monitoring and Enforcement

AlexanderF
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 140
Registriert: 2. Mai 2010 17:55

Questions and Remarks on slides about Runtime Monitoring and Enforcement

Beitrag von AlexanderF » 22. Dez 2017 18:12

hello,

I have some questions and remarks on some slides from the slides set of Module 6 on Runtime Monitoring and Enforcement.

On slide 13 in the third text line between sigma' and delta'
I think it should be mu' instead of mu.

On slide 19,
I think it is a little bit silly to give the set {0, ..., n-1} the name N_{0, ..., n-1}
(Instead of N_{0, ..., n-1} one can also write {0, ..., n-1}).
Then maybe, the name N_n from the first version of the slides set is the better name.

The set N seems to denote the set of natural numbers including 0 in this slides set,
in contrast to the slides set of Modul 1 where N seems to denote the set of natural numbers excluding 0 and N_0 the set of natural numbers including 0.

On slide 24, I think it should be alpha ((E, Tr)) := E.

On slide 33, the formula describing "prefix closed" is wrong.
The given formula is a tautology (since Tr is a subset of E* one can always choose t1 to be t and hence t1 is element of Tr).
Right formulas describing "prefix closed" would be:
forall t element Tr: forall t1 t2 element E*: (t1 t2 = t => t1 element Tr)
as well as
forall t element Tr: forall t1 element E*: ((exists t2 element E*: t1 t2 = t) => t1 element Tr)

On the same slide is written
"Each predicate P on traces induces a trace property defined by ..."
where trace property is defined to be set of traces that is prefix closed.
but I do not see why the suggested {tr element Tr^infinity | P(tr)} should be prefixed closed.

On slide 63, do I see right that CRIT is a subset of alpha?
The intuition is described on the slide to send only critical events to the coordinator,
why then occures alpha union CRIT in the definition of INT(alpha, CRIT),
and not only CRIT?

On slide 64 I think the second line in the yellow box should be
"parametric in critical events and enforcement decisions"
rather then the same text as on the slide before.

And slide 69, I think, contains a reference to a wrong slide number (I think this was already remarked in the lecture).

best regards,
Alexander

Benutzeravatar
Linux-Fan
Neuling
Neuling
Beiträge: 10
Registriert: 15. Apr 2015 22:22
Kontaktdaten:

Re: Questions and Remarks on slides about Runtime Monitoring and Enforcement

Beitrag von Linux-Fan » 4. Feb 2018 21:18

e0628.png
e0628.png (74.71 KiB) 383 mal betrachtet
(Sorry for posting an image, but on my end, the use of the tex-BBCode caused some empty areas to be displayed and I found the issue subtle enough to not be directly apparent if only described without using the actual symbols).

AlexanderF
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 140
Registriert: 2. Mai 2010 17:55

Re: Questions and Remarks on slides about Runtime Monitoring and Enforcement

Beitrag von AlexanderF » 5. Feb 2018 12:19

hello,
I agree on the last observation and also have something to add:

On Slide 24, Notation,
there are a P and a Tr mentioned,
without saying what P and Tr are.

Is P a process (like defined in the slide above)
and is Tr := traces(P)?
but then Tr should by definition be a subset of E*,
and hence I do not understand the meaning of Tr_fin and Tr_inf,
since it would be Tr_fin=Tr and Tr_inf=empty set.

In the definition of slide 26,
I think the "E:=" in the first bullet point should better be written as "E =",
since it occurs as a requirement of the definition.

On slide 49, I think, the Q should be an E.

On slide 50, what should X subset E mean in the last bullet point?

best regards,
Alexander

Antworten

Zurück zu „Archiv“