++++++++++++++++++ FME2001: - Review reports for paper 45 +++++++++++++++++++++ - 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: 45 CATEGORY: 2 TITLE: Avoiding State Explosion for Distributed Systems with Timestamps AUTHOR(S): Fabrice Derepas Paul Gastin David Plainfossé -------------------------------------------------------------------------------- 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: 2 Please comment your rating: The paper essentially concerns a state space reduction technique for model-checking, which is likely to be of more relevance to conferences such as CAV or TACAS. It does not report significant fresh progress on applying formal methods. 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 or 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: 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: a small amount that is new, but of minor significance. 6. How WORTHWILE is the goal of the authors? Comment: The specifc goal of state space reduction for timestamped systems is worthwhile. But the ideas presented are not of great significance and developments reported are not striking. The technique has various limitations on its use and it is unclear what speed up it will deliver across a range of applications - even if they meet the restrictiosn to enable the techniques to be applied. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: The basic idea is fairly simple, but it is not well explained. The proof of soundness are a technical contribution, but the presentation is laboured and restrictions on the method are not clearly stated. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: There are restriction on applying the methods presented. If the original model has state transitions depending on explicit values of timestamps, rather than relative values, then the method will not be sound. This is a global restriction which needs to be stated explicitly (it is only alluded to). The method is also only applicable for modelling systems in which synchronised clocks are also provided - this is not mentioned at all. As a cinsequnce, the work verges on being unsound. 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: New techniques are presented, for application. The benefits of the techniques, for a range of applications, are not to clear. The 'results' presented are too superficial to judge. The techniques will be of no value in a system with only one timestamp. To judge general applicability the techniques have to be applied to a number of systems and performance against variations in the following criteria supplied: - total number of time increments in model - total number of timestamps 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: Quality of writing is not great. The basic concept in III B, is quite simple but not well described. Definition 1 seems excessive, is really all needed for the proofs..? Basically a medium sized paper for a simple idea. 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: 45 CATEGORY: 2 TITLE: Avoiding State Explosion for Distributed Systems with Timestamps AUTHOR(S): Fabrice Derepas Paul Gastin David Plainfoss=E9 -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The paper presents a method to apply data abstractions on the fly in an enumerating model checker to reduce the range of timestamp variables. 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: Techniques for reducing the state space in model checking are important. However, the scope of the described technique is rather narrow. 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: 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 =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: 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 method of computing and applying data abstractions on the fly in model checking. 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: It appears so, but I didn't check everything. 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: Yes. Judging from the experimental results, the methods works very well, making the state space size independent of the timestamp variable ranges. 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, as far as I could tell. 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: 45 CATEGORY: 2 TITLE: Avoiding State Explosion for Distributed Systems with Timestamps AUTHOR(S): Fabrice Derepas Paul Gastin David Plainfoss=E9 -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The topic of paper are distributed systems that use timestamps and a restricted set of operations on the timestamps. For such systems, the paper presents an algorithm to considerably reduce that state space needed for the timestamps for model checking purposes. 2. RELEVANCE: Please provide a rating of the paper's relevance to the FME Symposium, using the scale: Numeric Rating: 3 Please comment your rating: See reponses 6-9. 3. OVERALL RECOMMENDATION: Please provide a rating of the paper's acceptability, using the scale: Numeric Rating: 4 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: I believe that the algorithm of "shrinking" the state space required to store the clock values is new. By itself, it may not be of major significance, unless applicable to the verification a wide, or important, range of systems/properties. Obviously, these systems/properties have to be such that the obstacle in verifying them is the timestamps, and these have to be in the limited form studied. Unfortunately, the system for which the algorithm was tested is described too abstractly, and its properties were not presented, hence it is difficult to appreciate the practical significance. 6. How WORTHWILE is the goal of the authors? Comment: Both goals, that of reducing the state space of a distributed systems, and that of formally verifying a real communication systems, are highly desirable. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: The goals are well explained and justified. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: The technical parts are basically sound. See response 10 for more detailed comments. 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 seems to be rather theoretical, though it was used to verify a 'real' system. The algorithm presented is sound. Unfortunately, in terms of experimental results, neither the system, nor the properties verified, are discussed in a manner that will allow drawing conclusions about the general applicability. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: In general, the paper is clear. In more details: The definition of the function rho may be clearer if, e.g., its image is clearly defined. In the proof of Lemma 2, the second subcase in the second case doesn't cover the x=3D0 (and z>0). 11. Were there any formatting or mechanical problems with this paper?: N Are the figures and length acceptable?: Y Are the references correct?: N 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 ++++++++++++++++++++++