++++++++++++++++++ FME2001: - Review reports for paper 34 +++++++++++++++++++++ - 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: 34 CATEGORY: 2 TITLE: Reformulation: a Way to Combine Dynamic Properties and B Refinement AUTHOR(S): F. Bellegarde C. Darlot J. Julliand O. Kouchnarenko -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The paper supports model checking (PLTL) of more abstract (B) systems, by giving rules indicating when reformulated "concrete" PLTL properties guarantee "abstract" PLTL properties. 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: Or maybe a 4. Model checking large/infinite systems is what everyone would like to do - refinement should provide a handle on this problem. 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: 4-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: Seems original, although not sure to what extent covered by authors' earlier work - but in any case deserving to be heard at FME! The reformulation (in most cases: weakening) of properties through refinement is especially significant, although I'd like to see a move towards calculating rather than verifying such properties. 6. How WORTHWILE is the goal of the authors? Comment: Very - model checking on "abstract" systems may well be more feasible in terms of state space size, and more needs to be known about how properties get preserved or evolve in refinement. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: Clearly enough. Appealing example, even if it does require a theorem not included in the paper. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: They appear sound to me, though I haven't checked every proof step. Proofs in appendix are very detailed. 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: Good arguments in favour presented. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: Well written, some minor issues below. Good example, too much detail in proofs in appendix (useful for checking but some details too trivial for including in paper). p3 l11: why is the fact that it can't handle infinite systems worse than being unable to handle very large ones? It follows already ... p3 l-9: Unclear at this point what "old" and "new" events referred to. p9 l-10: "turned to *the* side", not sure about "preceding unloading" being beautiful English p10 l4: space before . p10 before 3.1: remove "the" before "guards" and "generalized .." p11 l4: remove first the non-determinism p11 start of 3.2: remove second the p11 l-8/9: "allows the user to have more possibilities" is 2x; unclear what is meant here anyway p13 bottom: "delay termination q_2 too long"? I don't understand. p14 l-4: there -> they p15 middle: need*s* to be strengthened p16 2nd line below fig9: does -> do p17 end of 2nd para: Does B also allow imposing an invariant (through trivial data refinement) which cuts down the state space to only the reachable states? What is the consequence of that? p17 just before 4: remove last the p17 l-13: remove second the (control) p17 l-7: what is the "modular refinement relation"? modular in what sense? like compositional? p18: remove the massive duplication between section 3.5 and section 4. Refs: 4. Fundamental 7. Protocol 8. Prentice Hall 14. Aug Appendix: system names (eg ROBOT0) in all caps in main paper, Robot0 here. P20 top: worthwhile explaining what these extra three implications are, intuition etc, and especially: why do we have to prove them? 11. Were there any formatting or mechanical problems with this paper?: No Are the figures and length acceptable?: Cut appendix proofs a bit Are the references correct?: See above 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: 34 CATEGORY: 2 TITLE: Reformulation: a Way to Combine Dynamic Properties and B Refinement AUTHOR(S): F. Bellegarde C. Darlot J. Julliand O. Kouchnarenko -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): When the event structure of a B event system is refined, temporal properties of are not generally preserved. The paper presents methods to reformulate PLTL properties during refinement and to show that the reformulated property holds. 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: Refinement is an important technique in formal methods and so are transition systems such as B event systems. 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: The methods reported permit temporal properties of refined systems to be shown valid not by model checking the refined system but by reformulating properties of the abstract system which are already known to hold. Since the abstract system has less states than the refined system, the penalty of carrying out proofs to show that the reformulated properties hold is likely to be slight compared to the penalty of model checking in the larger state space of the refined system. 6. How WORTHWILE is the goal of the authors? Comment: Very. 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: Yes (although I did not 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. The results also appears to be applicable to transition system refinements in general and not only to B event systems. 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?: The paper is a bit too long. The authors should consider shortening it, e.g. by dropping the appendix Are the references correct?: Yes. 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: Including page numbers will make it easier for the reviewer. +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++ PAPER NUMBER: 34 CATEGORY: 2 TITLE: Reformulation: a way to combine dynamic properties and B refinement AUTHOR(S): Bellegarde &al -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The paper considers the problem of verifying the dynamic properties of communicating systems specified using AMN with events. The notion of refinement admits both proof and model-checking. 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: Of interest to all those at the Symposium involved in distributed systems. 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: The combination of formalisms is a hot research topic at present. The novelty here lies in the combination of AMN and linear temporal logic. 6. How WORTHWILE is the goal of the authors? Comment: very worthwhile. It should be noted that the systems that may be developed in this style are all finite state ones. This restriction is quite severe. 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: I believe that all the technical material is 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: There is little in the paper that directly addresses the practical relevance of the work. The authors admit that it has yet to be applied to larger examples, let alone industrial-sized problems. So, the work is at an early stage; it looks promising, however. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: The presentation is 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: +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++