FMICS Review Comments
----------------------- REVIEW 1 ---------------------
-
Typo in the abstract: draw for -> drawn for - This is not a typo, it's supposed to be like that "power draw"
-
Some of the references are underspecified. Notably, in [11,16], volume of what? In [10], probably the Open University in the Netherlands is meant?
----------------------- REVIEW 3 ---------------------
Debatable assumptions:
-
negligible energy footprint of controller: A quick search seems to indicate that controllers draw about as much power as e.g. LED (used in example Fig 1), or some sensors: 1-10mW range. Maybe this footprint can be assumed constant across all program lines (and thus it is just a constant offset on the axis of the skyline)? But what about sleep/low power mode? Maybe model controller as a component, too? -
low algorithmic complexity of control software: what about PID controller? This is a very common type of controller, which contains integration and differentiation. But maybe this calculation can be hidden in library calls? These would have no impact on energy consumption, and thus could be left out of the analysis, as there is no component interaction in them. -
Loop iterations are bounded, and thus some paths not analysed. This is deemed "uncommon". Control software should not terminate (and stop controlling), but should loop indefinitely (see "main" method of example Fig 13). Then why "uncommon"? Can it be assumed that a few iterations suffice to discover all paths (i.e. not the looping is uncommon, but missing paths is)? In that case, why can this be assumed? -
Component calls have no input. What about e.g. a motor speed? How representative is this model of real-world components?
Semantic weaknesses:
-
what about global variables? Variables are declared as such in Sec 3.1. But "call" only sets x, making no other variables accessible to f. Maybe it is supposed to be "env'= env[x->v]"? Also, "S[return]" does not preserve global variables (resets everything except "#return") -
"S[e]" does not extend the skyline, thus a function call outside any assignment, etc. (e.g. Line 3 in Fig 13) does not get F(l). Meanwhile, "E[c.f()]" does extend the skyline, thus sensor reads like Line 8 get multiple "F(l)" (from "S" of assignment/if condition/ while, and from "E" of component call). Probably only "S" should extend the skyline. - This is a bug in the E[return] clause. n=lineOfCallSite must be used.
-
Semantics use "return" to wrap up function calls (e.g. to pop stack), but Fig 13 has functions without return. Probably an implicit return is used, but not mentioned. - Added explanation
-
I have made the parser more C-like (optional else, allow missing return, return void, types for variables). Do we need to update the syntax? In the paper it's abstract syntax. - It just costs space in the paper and does not add anything of value. In fact, it would require me to update the semantics. Not gonna do that.
-
bounding of loop iterations is not included in formal semantics. - I have revived the explanation of the clause, where it says "not shown here"
-
small details: in "E{c.f()]", it says "s_c = cstate[c]" instead of " s_c = sigma.cstate[c]"; -
in "E[f]", the notation "\bar E" is not defined (probably chains sigma, i.e. sig1=Ee1, sig'=\bar Ee2..eN? Or do all "E" get the same sigma?); -
"return" does not use "n=lineOfCallSite", so it can be removed; -
"registerSkyline" is not defined (must return a sigma. which one, given sigma?)
other proposed improvement:
-
In some loops, skylines can jump back to their own colour (e.g. red line in Fig 9, Line 9->5). However, this is not explicitly indicated like a jump to a different colour is. But it can also not be implicitly assumed, as e.g. Fig 5b cannot jump back to its own colour. Thus, a backward jump to own colour should be indicated just like a jump to another colour. - That's a tough one. The reviewer is correct, there should be a jump point to the own colour. Why is it not drawn?
- We explicitly delete those! 4d9222a7 Why did we remove them? Was there a specific reason?
- I have reverted this commit for now
-
update all diagrams with loops in the paper -
There is only one, fig. 9
-
Edited by Markus Klinik