++++++++++++++++++ FME2001: - Review reports for paper 06 +++++++++++++++++++++ - 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: 06 CATEGORY: 2 TITLE: Verifying Implementation Relations AUTHOR(S): Jon Burton Maciej Koutny -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The paper presents a technique for verifying the implemnation relationship in a CSP framework and it introduces the notion of extraction pattern. 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: CSP models and the relationship betxeen models are very important for modelling concurrent and 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: 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 defintion of the implementation relationship over CSP processes and the extraction patterns are very simple new ideas. 6. How WORTHWILE is the goal of the authors? Comment: well 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: You might improve thye paper by case studies. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: 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: Further applications may be developed with these techniques. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: Very well written 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: I think that the presentation of CSP and the divergence model might be extended in the preliminaries section to allow a larger number of persons to understand the semanticla background of CSP. I know divergence models (although I am not from Oxford) but there are technical details which are useful for understanding the approach. Maybe, add a small example earlier. I am wondering what is the relationship between extraction problem and refinement mapping ( in your models). The definition of extraction pattern is very interesting and it is able to capture critical questions over traces and refusals. I think that extraction atterns should be more illustrated, since it is a new idea for defining implementation relationships. +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++ PAPER NUMBER: 06 CATEGORY: 2 TITLE: Verifying Implementation Relations AUTHOR(S): Jon Burton Maciej Koutny -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The paper defines the notion of "implementation relations" which are used to relate one CSP process ("the implementation") to another ("the "specification"). The definition caters for the fact that the two processes may have differing interfaces. In the second half of the paper, the authors also define a notion of a "communicating transition system", which is used to give a graph-theoretic semantics for a CSP process; they use this representation in designing an algorithm for checking the validity of an implementation relation. 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 (Majority interest) Please comment your rating: To get around the state explosion problem, abstraction mechanisms such as the implementation relations described in this paper are essential. Techniques describing such mechanisms are therefore of great interest to researchers using formal methods to improve software productivity. 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 (Weak reject) 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: Since I'm not an expert in the area, I can't answer this question with much confidence. Certainly the notion of refinement has been studied in the context of CSP before. My impression is that the notion of allowing one channel to be implemented by several others might be new. The interpretation of CSP processes by transition systems is definitely not new, but the algorithms for checking the conditions on an "implementation relation" are obviously new (since they check conditions introduced by the authors). 6. How WORTHWILE is the goal of the authors? Comment: Having the flexibility of allowing one channel to be implemented using many channels is useful when implementations use redundancy to provide fault-tolerance. (Otherwise, the flexibility seems merely a convenience, and its usefulness is not clear.) Unfortunately, the algorithms given in the paper do not deal with this case. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: Not too well. The abstract says very little (the only mention is in the key phrase "having different interfaces"). The introduction does devote some space to it, but the conclusion is somewhat abrupt. Some more description in the abstract and the conclusion would be helpful. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: Hard to say. Certainly the notation is terrible: quantifiers are implicit, and definitions and terms are overloaded without much warning. For instance, the set { (t,R) \in \phi P | (t,S) \in \phi P /\ R \subseteq S => R = S } is supposed to denote the set of pairs of the form (t,R) such that (t,R) \in \phi P /\ (Forall S : (t,S) \in \phi P /\ R \subseteq S => R = S) But looking at the first formula does not at all make it clear that the quantification over S is supposed to be universal (and not, say, existential). Some operators (e.g., o which presumably means concatenation of traces) are left undefined. Also it is not clear why conditions EP0 - EP8 are the right set of conditions to impose on extraction patterns, nor why IR1-IR5 are the right conditions for implementation relations. 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: Applicability is not addressed anywhere (not that I could see, anyway). 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: The body of the paper (sections 2 -- 8) are very hard to read, since they consist almost entirely of mathematical formulae, with little or no informal description. Given that notation is used somewhat sloppily, this makes these sections very hard to read (except perhaps for CSP mavens). At the very least, for every definition and set of conditions (R1-R2, EP0-EP8, IR1-IR5) the authors should give informal justifications. 11. Were there any formatting or mechanical problems with this paper?: No, none that I could see Are the figures and length acceptable?: Apparently Are the references correct?: I didn't check. 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: 06 CATEGORY: 2 TITLE: Verifying implementation relations AUTHOR(S): Burton & Koutny -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The work concerns the refinement of communicating processes. Given two such processes with differing interfaces, the authors establish an implementation relation between. The paper contains a graph-theoretic treatment of such relations, from which they derive algorithms for their automatic verification. 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: Not everybody is interested 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: 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: There is nothing new or original in the paper, as all the results have been previously presented at the International Workshop on Verification & Computational Logic. For this reason, I have suggested that the paper may be accepted or rejected, it can go either way. The PC must decide whether it is acceptable for the authors to have published a preliminary version of the paper. 6. How WORTHWILE is the goal of the authors? Comment: Very worthwhile. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: Adequately. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: 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 theoretical, but it's implications are clear. The authors also take care in section 9 to explain the practicalt suitability of the algorithms that they have derived. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: This is a well-written paper. 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 references are very narrow: there are no references to work outside your own (if one excludes the standard references, such as the CSP books). This is inappropriate: there is related work, and in shows a lack of scholarship to be ignorant of it. +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++