++++++++++++++++++ FME2001: - Review reports for paper 44 +++++++++++++++++++++ - 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: 44 CATEGORY: 2 TITLE: How to Make FDR Spin LTL Model Checking of CSP by Refinement AUTHOR(S): Michael Leuschel Thierry Massart Andrew Currie -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The paper explores the refinement checking in the context of CSP models; it chooses also to express property and program in the same language. 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 refinemnt checing is a central point in development method as B for instance. 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 way they are using FDR and checking in the refinement of CSP processes and the use of one language for property and process. 6. How WORTHWILE is the goal of the authors? Comment: well 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: seems to be 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: it is one goal of the paper to apply and several small case studies are used. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: well 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: 44 CATEGORY: 2 TITLE: How to Make FDR Spin LTL Model Checking of CSP by Refinement AUTHOR(S): Michael Leuschel Thierry Massart Andrew Currie -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The paper describes two options to do LTL model checking in the frame work of refinement of Communicating Sequential Processes (CSP's). while the first option of standard refinement is conjectured to be unsuitable for verifying liveness properties, the second option of constructing a Buchi automaton as a tester and composing it with the system works. 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 work described in the paper addresses topics of major interest to the community, both from the theoretical and practical aspects. 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: I am not aware, nor the authors mention, previous work on this particular problem. 6. How WORTHWILE is the goal of the authors? Comment: Since the problem of LTL model checking is very general, any new direction competing with current techniques is worthwhile trying. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: the paper, in general, is very well written and explained. There is a good introduction of the material: CSP, LTL, etc. The fact that not only the successful approach is presented, but also the one that failed contributes a lot. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: All claims are accompanied by proofs, which seems 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 no 'benchmark-based' comparison between their method and, say, standard LTL model checking. In this case it's not extremely important because the theoretical contribution is significant enough. Future work can complete this part. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: Here are several suggestions for corrections: page par. line comment ========================= 2 2 3 'show that is..' -> 'show that it is' 2 5 4 here and elsewhere refrain from starting sentences with e.g. In this case it should actually be: ... 'semantics of P, thus trace refinement ...' 3 2 9 '... action $a$ of A, P..' -> 'action $a \in A$ in P..' 4 1 1 'and ... invisible action..' -> 'rather than states carry labels, and some of the transitions are labeled by the invisible action...' 5 3 3 'any number' -> 'any finite number' 5 The conclusion you arrive to later that the problem is with liveness, can be mentioned right from the beginning, since it is not very surprising, given that you can only use finite traces. For this matter, formal definition 1 in the bottom of the page is not really necessary at this point. You can move it to section 2 as part of the preliminaries. 6 3 1 You do not need the subtitle 3.2 'a more refined approach' because this paragraph doesn't really introduce a more refined approach. It's only an explanation of why refinement doesn't work in general. The first paragraph of this section is a direct continuation of the last paragraph in the previous section. (do not start sections with 'Furthermore'.) 6 4 1 Do not make this a \begin {example} section, Your 'for example' in the beginning is enough. 6 5 2 'E.g' -> 'For example..' 6 8 1 'alternate' -> 'alternative' 6 9 2 'to finally' -> 'and finally' 8 1 2 $\delta $ shouldn't it be '$\delta^\omega$' ? 8 2 4 rewrite the sentnce starting with 'Therefore'. Perhaps: 'Therefore, we must build a tester which tests both infinite traces and deadlocking traces'. 8 10 1 (point 3) 'removed' -> 'removed.' 10 9 2 'by obtained by' -> 'be obtained by' 11 1 1 change to 'Let us show now an example which proves the incompleteness ...' 11 4 1 (right under title of sec. 4.4) 'Tester by ..' -> 'Tester be' 11 last 2 'processe' -> 'process' 11 last 3 'we know' -> 'we know that' 12 1 3 '. I.e' -> ', i.e.' 12 last 1 'manage write' -> 'manage to write' 13 6 9 ' checking that our' -> 'check that his/her' .. There are two places where I thought some more clarification could be helpful: 1. example 3 in page 6. wasn't clear to me why is it sufficient to check that S' cannot diverge in the initial state. what about other states in a finite prefix ? 2. Definition 2 in page 8. The distinction between infinite traces and finite traces with deadlock is the reason for this definition of Buchi \Delta automaton, as I understand. But can't you reduce it to a regular Buchi by including D in F, and changing every deadlock state into a 'sink' state? If this is possible, then this simplifies everything. 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: The preliminaries should include, perhaps, the principle differences between the refinement approach to LTL model checking, and the more standard algorithm of e.g. Pnueli & Lichtenstein. It should somehow be included in the motivation of your work. +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++ PAPER NUMBER: 44 CATEGORY: 2 TITLE: How to Make FDR Spin LTL Model Checking of CSP by Refinement AUTHOR(S): Michael Leuschel Thierry Massart Andrew Currie -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The paper shows how the model checker FDR can be used to test whether a finite state CSP process satisfies a LTL formula. 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: Clearly of interest, as it potentially makes it easier to capture requirements of systems, and so make a powerful tool easier to use. 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: 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: This is (I believe) the first time that the power of FDR has been combined with the ease of specifying using FDR. 6. How WORTHWILE is the goal of the authors? Comment: Very. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: Reasonable. It might be nice to see some examples of properties that are difficult to capture using refinement-based techniques, but easier using LTL. On the other hand, it would be useful to point out the limitations of the LTL formulae in the paper. For example, they cannot capture the property "an a is not refused initially", which is easy to capture using refinement-based techniques. This problem could be overcome by adding additional atomic formulae. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: The results appear to be technically sound. The authors suggest (Section 3.2) that it is not possible to capture the LTL formula [](a => <>b) ("always a implies eventually b") using "standard" refinement techniques. In fact, it is possible to capture this using a one-to-many renaming (but doing so is very non-trivial, which supports the authors' assertion that an automatic way of capturing LTL formulae is useful). However, I conjecture that it's not possible to capture <>[]a ("eventually always a") in this way (but I haven't proved it). Perhaps <>[]a would be a better example. 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 is my major objection to the paper. The technique the authors use involves doing a refinement check where the system being analysed appears on the *left* hand side (i.e. specification side) of the refinement check. The model checker FDR works far less effectively when the left hand side of the refinement is a large process (because it normalizes this process). For this reason, it is normal to have the system being analysed on the right hand side of the refinement. I suspect that this will severely limit the applicability of the authors' techniques. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: In places the authors' should be clearer on whether they are talking about finite state processes, or potentially infinite state processes. In fact, as FDR cannot deal with infinite state processes, it makes sense to stick to finite state processes (except, perhaps, in Proposition 5). It would be useful to have a brief overview of your construction near the beginning of Section 4.2: that you construct processes Q, Q' and CSP functions F, F', such that P does not satisfy phi iff F(P) [T= Q and F'(P) [F= Q' 11. Were there any formatting or mechanical problems with this paper?: Are the figures and length acceptable?: Are the references correct?: Mostly ok. 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: The translation of a LTL formula into a CSP process goes via several intermediate forms: can this be shortened? The proof of Proposition 6 could be shortened by appealing to monotonicity. At the beginning of Section 5, P and Q are mixed. System 4 in Appendix B *does* satisfy <>b (did you mean to use a nondeterministic choice?). +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++