++++++++++++++++++ FME2001: - Review reports for paper 56 +++++++++++++++++++++ - Dear author(s) : this file was extracted automatically from a very large - mailbox. In case you find any problem concerning mail encodings (or any - other kind of anomaly disturbing your understanding of the reviews) please - email any of the PC cochairs (pamela@research.att.com,jno@di.uminho.pt). ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ PAPER NUMBER: 56 CATEGORY: 2 TITLE: Test-Case Calculation through Abstraction AUTHOR(S): Bernhard K. Aichernig -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): This paper present a new approach for generating test cases from a formal specification based on program synthesis and transformation methods. It differs from the finite state machine approach (test-sequencing on model-oriented specifications) pioneered by Dick and Faivre in that it is based upon finding compositions of interactions determined by abstraction rules which are derived using the refinement calculus. 2. RELEVANCE: Please provide a rating of the paper's relevance to the FME Symposium, using the scale: 0 = Out of scope 1 = Marginal interest 2 = Minority interest 3 = Majority interest 4 = Outstanding interest Numeric Rating: 3 Please comment your rating: 3. OVERALL RECOMMENDATION: Please provide a rating of the paper's acceptability, using the scale: 1 = Strong reject 2 = Weak reject 3 = Could go either way 4 = Weak accept 5 = Strong accept Numeric Rating: 4 NB: There should be a correlation between the two rates above. 4. CONFIDENCE LEVEL: Please provide a rating oof your expertise in the area addressed by the paper, using the scale: 1 = Know virtually nothing about this area 2 = Not too knowledgeable, but I know a bit 3 = Know a moderate amount, about average I'd say 4 = Not my main area of work, but I know a lot about it 5 = My area of work, I know it extremely well Numeric Rating: 2 NB: PC members are responsible for ensuring that 1 is not used here. 5. ORIGINALITY. What is NEW and SIGNIFICANT in the work reported here? Comment: Application of program synthesis and transformation methods to the test generation problem. It then extends the methods to apply to interactive systems. 6. How WORTHWILE is the goal of the authors? Comment: Testing is an extremely costly component of software development. This work attempts to increase the efficiency of testing through automatic generation. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: The goal of the research is explained well and illustrated on the classic academic process scheduler problem. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: The paper appears to be technically sound. 9. APPLICABILITY. If the work is primarily theoretical or conceptual, are the implications in terms of applicability adequately justified? If the paper is about a new formal technique, are satisfactory arguments presented in favor of the new technique? If a methodology is proposed, is it sound? If experimental results are presented, is their relevance justified? Comment: Theoretical research with ultimate goal of building practical tools. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: The paper is reasonably well written though the first sentence of the paper is bizarre: " In the past of computer science a large gap between the testing and the formal [methods community could be realized." 11. Were there any formatting or mechanical problems with this paper?: no Are the figures and length acceptable?: yes Are the references correct?: yes 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++ PAPER NUMBER: 56 CATEGORY: 2 TITLE: Test-Case Calculation through Abstraction AUTHOR(S): Bernhard K. Aichernig -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): 2. RELEVANCE: Please provide a rating of the paper's relevance to the FME Symposium, using the scale: 0 = Out of scope 1 = Marginal interest 2 = Minority interest 3 = Majority interest 4 = Outstanding interest Numeric Rating: 3 Please comment your rating: 3. OVERALL RECOMMENDATION: Please provide a rating of the paper's acceptability, using the scale: 1 = Strong reject 2 = Weak reject 3 = Could go either way 4 = Weak accept 5 = Strong accept Numeric Rating: 4 NB: There should be a correlation between the two rates above. 4. CONFIDENCE LEVEL: Please provide a rating oof your expertise in the area addressed by the paper, using the scale: 1 = Know virtually nothing about this area 2 = Not too knowledgeable, but I know a bit 3 = Know a moderate amount, about average I'd say 4 = Not my main area of work, but I know a lot about it 5 = My area of work, I know it extremely well Numeric Rating: 4 NB: PC members are responsible for ensuring that 1 is not used here. 5. ORIGINALITY. What is NEW and SIGNIFICANT in the work reported here? Comment: The new part about this work is the use of refinement calculus in order to synthesize test cases. 6. How WORTHWILE is the goal of the authors? Comment: Very 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: Well 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: Yes 9. APPLICABILITY. If the work is primarily theoretical or conceptual, are the implications in terms of applicability adequately justified? If the paper is about a new formal technique, are satisfactory arguments presented in favor of the new technique? If a methodology is proposed, is it sound? If experimental results are presented, is their relevance justified? Comment: The work reported here is conceptual but although industrial application of the work is mentioned the implication of the work is not properly justified and set in perspectives. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: Good 11. Were there any formatting or mechanical problems with this paper?: no Are the figures and length acceptable?: yes Are the references correct?: yes 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: A few minor comments: p9,sec4.1,l2: "this" -> "these" p10,sec4.3,l4: end bracket missing p13,sec6,l5: What type of system are you then envisaging to use it on? Why are you not using that type of system in the example illustrating the principles? +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++ PAPER NUMBER: 56 CATEGORY: 2 TITLE: Test-Case Calculation through Abstraction AUTHOR(S): Bernhard K. Aichernig -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The paper proposes a novel approach based on the refinement calculus to calculating correct test-case scenarios from formal specifications. The method offers a synthesis method that eliminates the need for computing a finite state machine for producing test cases. 2. RELEVANCE: Please provide a rating of the paper's relevance to the FME Symposium, using the scale: 0 = Out of scope 1 = Marginal interest 2 = Minority interest 3 = Majority interest 4 = Outstanding interest Numeric Rating: 3 Please comment your rating: The paper proposes a very interesting and potentially useful method for testing interactive programs starting from formal specifications. If backed up by suitable tools, the method can probably be adopted by the industry. 3. OVERALL RECOMMENDATION: Please provide a rating of the paper's acceptability, using the scale: 1 = Strong reject 2 = Weak reject 3 = Could go either way 4 = Weak accept 5 = Strong accept Numeric Rating: 5 NB: There should be a correlation between the two rates above. 4. CONFIDENCE LEVEL: Please provide a rating of your expertise in the area addressed by the paper, using the scale: 1 = Know virtually nothing about this area 2 = Not too knowledgeable, but I know a bit 3 = Know a moderate amount, about average I'd say 4 = Not my main area of work, but I know a lot about it 5 = My area of work, I know it extremely well Numeric Rating: 5 NB: PC members are responsible for ensuring that 1 is not used here. 5. ORIGINALITY. What is NEW and SIGNIFICANT in the work reported here? Comment: Unlike other works on synthesis of test cases from formal specifications, the approach described in the paper is based on program transformation techniques. The refinement calculus, which is a formal framework for reasoning about the refinement and correctness of imperative programs, is used for calculating test-cases. As far as I am aware, this is a definite innovation. 6. How WORTHWILE is the goal of the authors? Comment: Research in testing techniques and in particular those having a strong mathematical foundation is certainly worthwhile and the approach proposed in the paper is undoubtedly interesting. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: Quite well, although in a sense it's self-explanatory. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: In general, yes, but there are a few (minor) technical problems. In particular, the definition of scenarios and all the related theorems cannot be defined in higher-order logic. A sequence comprehension expression is a convenient notation for the corresponding construct but one cannot define such arbitrary sequences in HOL. Moreover, since these schemas are not predicate transformers proper, one cannot use them in the refinement relation connecting two predicate transformers, as in Theorems 4 and 5. I would suggest that the author soften the claims to reflect this discrepancy, stating that the framework is "rigorous" rather than "formal", or maybe just explaining that the reasoning is done outside higher-order logic. 9. APPLICABILITY. If the work is primarily theoretical or conceptual, are the implications in terms of applicability adequately justified? If the paper is about a new formal technique, are satisfactory arguments presented in favor of the new technique? If a methodology is proposed, is it sound? If experimental results are presented, is their relevance justified? Comment: The applicability arguments are adequate. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: The quality of writing is acceptable; I suggest some improvements below. 11. Were there any formatting or mechanical problems with this paper?: No Are the figures and length acceptable?: Yes Are the references correct?: Seem to be, but I haven't checked very carefully. 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: page 3: As in our previous work, he uses... -> it's unclear who "he" is. next sentence: [15] demonstrates that... -> rephrase, it's better not to start a sentence with a non-word. last sentence in this section: their is still space -> there is still space last sentence on this page: Back's theory of refinement -> Back and von Wright's theory of refinement page 4: unambiguously and sound -> unambiguously and soundly next paragraph: functional state transformers $$ -> functional state transformers $f$ (because in [6] $$ represents a predicate transformer formed from the functional state transformer $f$) same paragraph: relations are modelled by functions mapping the states to a Boolean value (T or F) -> relations are modelled by functions mapping the states to Boolean-valued predicates. next paragraph: In our work, the user... -> In our work following [5,6], the user... same paragraph: non-deterministic updates from the angel's point of view -> updates that are non-deterministic from the angel's point of view next paragraph: The angelic choice operator ... the demonic choice operator -> The angelic choice ... the demonic choice same sentence: define deterministic and non-deterministic choice -> define a non-deterministic choice (because both C_1 \sqcup C_2 and C_1 \sqcap C_2 define non-deterministic choices, they only define a deterministic choice if preceded by mutually exclusive assertions/assumptions). page 5: mapping postcondition predicates to preconditions -> mapping postcondition predicates to precondition predicates next sentence: We write... Rephrase, because this notation is rather traditional Next paragraph: rules of the calculus ensures -> rules of the calculus ensure two para below: formula abort.q = F should be abort.q = false where false is the universally false predicate. Same about "true" instead of "T" in the formula for magic. page 6: || -> |f| page 8: This assumptions -> These assumptions same page: This partitions describe -> These partitions describe page 9: Remove the second before last sentence, T;Q is not present ion the expr. above. page 10: It's probably a good idea to give an example of what a sequence composition expression expands to. Theorem 4: See my comment above. The lhs of the formula is a predicate transformer while the rhs is a schema of predicate transformers. Strictly speaking, you cannot connect the two via the refinement relation. Maybe this needs commenting to avoid further criticism. Shouldn't there be parentheses around {g_i};S_i? You mean ({g_i};S_i)(k), don't you? page 11: In the formula on top of the page remove {g_i};S_1 page 12: What values j ranges over in Corollary 3? same page: this compositions -> these compositions (several times) page 13: to valid test-scenarios -> to validate test-scenarios page 14: Figure 1, either explain that P_{set} stands for {p} or just use {p}. In Swap "ready" should be just "r" and a_{s}et should be a_{set}. Same in Fig.3 page 15: Figure 3 presents new partitions -> Figure 3 presents new partitions after some simplification. page 16: In many cases a precondition ... Why? Please explain more. next sentence: p in the formula p \neq true can be confused with p:Pid in the example. next paragraph: In this presentation ... g are skipped. Why? What does this mean altogether, why do you need this g at all? Please explain. same page: more practically -> more practical page 17: needs to choose -> is needed to choose (?) same page: tabular of possible compositions -> table of possible compositions +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++