++++++++++++++++++ FME2001: - Review reports for paper 37 +++++++++++++++++++++ - 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: 37 CATEGORY: 1 TITLE: Debugging a Real-life Protocol with CFFD-Based Verification Tools AUTHOR(S): Antti Kervinen Antti Valmari Risto Järnström -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The paper explains how model checking techniques were applied to debug a communication protocol. The protocol is one developed for industrial use. 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 is about an industrial application, and the technique seems effective. 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 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 approach is not new, but the application is. 6. How WORTHWILE is the goal of the authors? Comment: Highly rated. 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: The paper is not very technical. It seems to be based on sound theory. 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: Seems very applicable. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: The ideas behind the method, and the actual work done, are generally well described, 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 discovery of the error in section 5.4 is interesting. But that described in section 6.4 is much less clear. Is this an error? If so, what was done about it? The term "CRC error" should be explained when it is first used. The claims made about visual verification, including the idea that they can show errors that would not even have been considered in requirements, are interesting. The paper would be much improved with some pictorial examples. The rather wordy descriptions, especially earlier in the paper, could be compressed to make space. +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++ PAPER NUMBER: 37 CATEGORY: 1 TITLE: Debugging a Real-life Protocol with CFFD-Based Verification Tools AUTHOR(S): Antti Kervinen Antti Valmari Risto Järnström -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The analysis of an industrial communications protocol is described. This includes the history of the project, the various modeling phases, and the interaction between the university and industry. 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: The presentation, especially in the first part of the paper, is not focussed and in cases the material is not germane to this paper. The lack of definitions and clear statements of the results proved leads me to conclude that there will be minority interest in this paper. 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: 3 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: The analysis of the communications protocol. 6. How WORTHWILE is the goal of the authors? Comment: Their goal is to debug a communications protocol using their tools. I think it is a reasonably worthwhile goal. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: It is explained clearly. I don't think they justified it, but I don't think they had to; it is clear enough. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: There are no technical results in this paper. There are rough descriptions of previous work; there are rough descriptions of the protocols and the debugging effort, but no definitions, algorithms, proofs, etc. 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: This question is not applicable to this paper. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: The quality of the writing is acceptable, but there are many awkward sentences. Here are some suggestions. 1. In the abstract, "effects to the design" should be "effects on the design". 2. Page 2, par. (paragraph) 1, "effect to the design" should be "effects on the design". 3. Page 2, par. 2, Regarding "Section 4 discusses the protocol", it is much better to say "In Section 4 we present ..." since Section 4 does not "discuss". 4. Page 2, 1st par. of Section 2. "He worked part-time in the project" should be "He worked part-time on the project". 5. Page 2, 2nd par. of Section 2. I suggest rewriting "were found already during this stage" as "were found during this stage". 6. Page 2, 3rd par. of Section 2. I suggest rewriting "worked full-time in the project. First the" as "worked full-time on the project. First, the". 7. Page 2, 3rd par. of Section 2. I suggest rewriting "in the operation of the protocol design was found" as "in the protocol was found". 8. Page 5, Section 3.4, par. 1 add "a" in front of "congruence". 9. Page 7, 1st line "the pictures occasionally show out" should be "the pictures occasionally exhibit". 10. Page 7, 3rd par., 4th line. Remove "the" before "academia". 11. Page 10, last par. "was put in parallel" should be "was composed in parallel". 12. Page 11, 1st line. "The message source 1" should be "Message source 1". Several other references to "the message source" should be rewritten as "message source 1". 13. Page 11, 1st par., line 4, "had had" should be "had". 14. Page 11, par. 2, line 1, "sent" should be in the present tense so "sends" is best. 15. Page 15, par. 1, "forbad" should be "forbade". 11. Were there any formatting or mechanical problems with this paper?: No Are the figures and length acceptable?: Yes Are the references correct?: I think so 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: In the abstract, you say "Visualisation gave answers to ...". This is not explained in any detail, so why is it in the abstract? On page 2 you say "Because the common use of the word "verification" has drifted away from its formal meaning ...". This should be qualified, e.g., say "in this community", but see my comments below which might make this a moot point. Sections 2 - 3.3 are verbose and mostly irrelevant. Section 2 is verbose and has overlap with the introduction. I suggest folding it in to the introduction. Sections 3-3.3 should be elided. Here are some reasons why: 1. In Section 3, why do you attempt to explain the meaning of "verification"? This has nothing to do with your paper and is not appropriate for this audience. In addition you "define" the term "formal verification" by using the word "formal" (or a derivative) three times (e.g., you say that formal verification "means proving formally that a formally given model ... satisfies a formally given ...". 2. You say "even if the correctness of an implementation cannot be formally established, it would be valuable to know whether the design is correct". What does this mean? How do you know if the design is correct? The only answer is that you formally check it. 3. You say it may be "impossible" to encode a "vague notion" and so on. This seems like a tautology. 4. You mention PSPACE-complete problems. Again, this has nothing to do with this paper. It seems like an opportunity to reference your work. These sections are not germane. Sections 3.2 and 3.3 discuss well-know concepts and again seem to be here only to reference your work. You spend so much space describing CFFD-equivalence that it is a pity you do not give any definitions. On page 11, you claim that the protocol is data-independent. Did you prove this or are you assuming it? Doesn't the protocol check to see if a message is a control message, in which case, how can it be data independent? I would have like to see a description of the tools used, the lessons learned from the verification effort, what limitations of the tools were discovered by the verification effort, and a discussion of the "coverage" of the verification effort. +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++ PAPER NUMBER: 37 CATEGORY: 1 TITLE: Debugging a Real-life Protocol with CFFD-Based Verification Tools AUTHOR(S): Antti Kervinen Antti Valmari Risto J=E4rnstr=F6m -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): A communications protocol is modeled and analysed as part of an industrial development project. The analysis is carried out by visual inspection of transition systems obtained by reductions of the transition systems of the protocol model. 2. RELEVANCE: Please provide a rating of the paper's relevance to the FME Symposium, using the scale: 0 =3D Out of scope 1 =3D Marginal interest 2 =3D Minority interest 3 =3D Majority interest 4 =3D Outstanding interest Numeric Rating: 2 Please comment your rating: The topic as such has higher relevance, the rating is based on how it is presented in the paper. 3. OVERALL RECOMMENDATION: Please provide a rating of the paper's acceptability, using the scale: 1 =3D Strong reject 2 =3D Weak reject 3 =3D Could go either way 4 =3D Weak accept 5 =3D Strong accept Numeric Rating: 1 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 =3D Know virtually nothing about this area 2 =3D Not too knowledgeable, but I know a bit 3 =3D Know a moderate amount, about average I'd say 4 =3D Not my main area of work, but I know a lot about it 5 =3D 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: Except for the case study itself, not much. The paper describes at length the background of the work, the protocol itself etc. What would really be interesting and significant, such as the CFFD-based reductions and the visual validation are mentioned almost in passing. 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: No. 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?: No, the paper is too long. Are the references correct?: Yes, as far as I could tell. 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: The paper seems to focus on the wrong things (see 5 above) and is far too long for the technical contents it has. On the other hand, if the technical information was expanded, the paper could be a good basis for a tutorial article. +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++