++++++++++++++++++ FME2001: - Review reports for paper 22 +++++++++++++++++++++ - 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: 22 CATEGORY: 2 TITLE: Faithful Translations Among Models and Specifications AUTHOR(S): Shmuel Katz -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The paper proposes translations among different formalisms employed by different formal method tools. One of the concerns is how a correctness property proved with one tool can be translated for a suitable proof in another. This is an excellent paper that is not yet ready for publication. 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: 2 Please comment your rating: Many of the practitioners are wedded to a single tool; so, the paper does not address them. The paper is of interest to tool developers who may wish to integrate a variety of tools in a package, such as model checking and theorem proving. The paper attempts to address issues in such integrations. 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: 2 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: 3 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 work is original; no one has addressed this problem earlier, to my knowledge. The significance of the work --had it been completed-- would have been to point out several inconsistencies among various tools, and to provide a set of guidelines for design decisions to help future developers. 6. How WORTHWHILE is the goal of the authors? Comment: Excellent 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: Moderately well explained. Not very well justified. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: Mostly 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 is primarily conceptual, and the implications in terms of applicability are adequately justified. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: Fair. 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: The paper reads like a proposal to higher management, with the rules for faithful translations thrown in for good measure. I suggest that the author make up his mind which audience he is addressing, tool developers or end users, and present the material for them. I believe, if the work is carried to its logical conclusion it may very well result in a set of standards to be followed by tool developers. +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++ PAPER NUMBER: 22 CATEGORY: 2 TITLE: Faithful Translations Among Models and Specifications AUTHOR(S): Shmuel Katz -------------------------------------------------------------------------------- 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: 4 Please comment your rating: This paper should be in category 1 (theory) rather than 2 (practice). 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.5 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: 3 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: 6. How WORTHWILE is the goal of the authors? Comment: I found this paper interesting, even exciting, and potentially very valuable. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: My main concern is that the paper reads like an extended abstract. The author alludes to proofs, but does not give any, even though there is plenty of room to at least give a sketch. My enthusiasm is based on giving the author the benefit of the doubt--that there are proofs and they are 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: 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: The author is too brief sometimes. On page 3, what are I, P, and R? In Section 3.2, what is meant by "an optional assignment"? 11. Were there any formatting or mechanical problems with this paper?: Are the figures and length acceptable?: Are the references correct?: 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: 22 CATEGORY: 2 TITLE: Faithful translations among models and specifications AUTHOR(S): Shmuel Katz -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The author introduces the idea of a faithful relationship between the models of two formal methods, enabling one to move smoothly between different descriptions of a problem. 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: 2 Please comment your rating: I regard work in this area as being important, but it would be wrong to regard it as being anythign other than of minority interest at present. That doesn't detract from its importance. 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 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: 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: There is a lot of work going on this area: perhaps the most important is the work of Hoare & He on Unifying Theories of Programming. The author does not refer to this work, or even to be aware of it. The novelty of this work is to concentrate on a restricted semantic basis, rather than keep to the generality of Hoare & He: the author assumes a fair execution tree semantics. 6. How WORTHWILE is the goal of the authors? Comment: Very worthwhile. There is considerable theoretical and practical interest at present in unifying theories. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: Very well. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: Oddly enough, there is not much in the way of technical material to be checked: the paper is really a discursive one. 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: I'm happy about the applicability. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: It's fine. 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: The omission of references to Hoare & He's book and other work is, quite frankly, astonishing. You should add a section comparing and contrasting. +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++