++++++++++++++++++ FME2001: - Review reports for paper 35 +++++++++++++++++++++ - 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: 35 CATEGORY: 2 TITLE: From CSP to B: Specifications of a Post Office AUTHOR(S): Marielle Doche Andrew Gravell -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The paper discusses a case study specified using a combination of CSP and B. FDR is used to provide some simple model checking, and a CSP to B tool is used to generate the B specification. 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 is clearly within the scope and aims of FME. 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: 1.5 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: 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: There is little new here, and what significance there is is hidden. The authors describe their work as a methodology, but the work presented doesn't go that far. It is a case study, albeit with some interesting features, but the generalisation to a methodology is not clear. Moreover, and unfortunately, the interesting aspects of the case study are well hidden behind poor prose and rather uninteresting specification details. 6. How WORTHWILE is the goal of the authors? Comment: The goals are worthwhile (assuming them to be a distributed systems methodology involving integrated formal notations). 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: The goals are never really stated. At maximum the description consists of solely the first line of the introduction. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: The technical quality, in terms of the specification as written, is sound. However, the technical discussion is poor and the lessons drawn from the case study weak. In a paper of this sort, the case study should be used to illustrate generalities that will be applicable in a wider environment. Clearly there are useful things to be said here, but the authors concentrate on details which are not relevant. Specifications such as POsets on pp12 add nothing to the discussion. 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 paper claims a new methodology. As commented above the use of this term is not covered by what the authors present. Concentration on just presentation of the specification obscures whatever interesting aspects there are in the case study. Moreover the standard of presentation of the paper obscures some technically important points to a degree that it is uncertain as to what is being proposed. For example, csp2B provides a translation between two languages, yet the authors talk of "a csp2B machine". What does this mean? 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: The presentation is poor on a number of levels: Spelling. Both accuracy, for example "see bellow" on pp16, and consistency, for example "centre" vs "behavior". English. The English is poor, for example meaning of the sentences in the itemised list on pp10 is unclear to a point where they obscure the intended meaning. Scientifically. For example, in a table on pp8 the units of time are given as seconds which is clearly inappropriate given most of the columns then claim infinitely fast computation. The second author, as a native English speaker, clearly did not read the paper. 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: Notwithstanding some of the negative comments made above, there is worth in the paper. In its current form it is not suitable for publication at FME, however, it could make a useful contribution to the field if it was reworked to bring out some more of the interesting aspects of the work. +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++ PAPER NUMBER: 35 CATEGORY: 2 TITLE: From CSP to B: Specifications of a Post Office AUTHOR(S): Marielle Doche Andrew Gravell -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The paper presents a case study on the conjoined use of the FDR and Csp2B tools to specify and analyse a post office system. This example has been considered using other formalisms elsewhere. 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: 1 Please comment your rating: This paper does not present any new methodology of development, but just a case study applying existing techniques and tools. It seems to be me that it would have been more appropriate to submit it as a category 1 paper. Nevertheless, since the case study has already been widely explored, even in that category, the interest would be restrict. 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 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: An example of how the Csp2B tool can be used to effectively translate an existing CSP specifications. It is made clear what steps still need to be carried out manually. 6. How WORTHWILE is the goal of the authors? Comment: The authors seem to intend to extend the Csp2B tool to further assist in the process of translation. This seems as a very worthwhile goal, but it is not the subject of the paper. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: The authors claim to have presented a methodology of development, but they have actually exemplified the conjoined use of existing tools. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: I could not find any problems and, since the work has been checked using tools, it is unlikely there are considerable flaws. 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 authors have summarised the effort required to carry out the case study, in terms of computational resources and degree of automatic support available. They conclude that using FDR they reduced in half the amount of proof-obligations generated. There is no evidence, however, that the same sort of success rate can be achieved in other case studies. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: The paper is well structured and well written. There are a few problems, however. Many definitions need more explanation. More importantly, however, the authors explain FDR and its notation, but assume knowledge of the Csp2B tool. This is not a reasonable: people are more likely to be familiar with FDR than with Csp2B. This lack of explanation affects the readability of Section 4. 11. Were there any formatting or mechanical problems with this paper?: Are the figures and length acceptable?: Are the references correct?: Figure 1 is too heavy. 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: 35 CATEGORY: 2 TITLE: From CSP to B: Specification of a Post Office AUTHOR(S): Marielle Doche and Andrew Gravell -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): A method is suggested for specifying distributed systems. It involves using CSP to describe the architecture of the system, checking aspects with FDR. This is translated into AMN so that a more sophisticated system can be described. Information from the CSP analysis is used in checking the AMN specification. 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: This paper is of direct relevance to the aims of the FME Symposia. I've given it a score of "3", since 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: 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 originality lies in the case study: no new results are presented. The authors rely on the theoretical work of others, applying it in a novel way. 6. How WORTHWILE is the goal of the authors? Comment: The specific goals of the work are: 1. To combine a state-based formalism with a behavioural one. 2. To give one practical application of this combination. 3. To generalise the results of model checking with bounded types. 4. To reduce the burden of proving state-based refinement by using the results of the model checking. These are all worthwhile goals. (1) and (3) are the subject of much current research; (2) is an important validation step; (4) is very interesting. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: Well enough for me to understand it! 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: I found no technical mistakes at all. 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 authors claim to have a "methodology" (by which they mean "method", of course!). I don't see that; it appears that they have one example of using their combined techniques. A method requires more than that. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: The quality is very good: there are a few typographical errors that need attention, however. 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, very narrow. The authors fail to refer to the large body of work that is going on in this area. If one subtracts the standard references (i.e., B, CSP, FDR), then one is left with just nine references; of these, only four originate from outside the authors' institution. This would be acceptable if there was little work going on outside Southampton, but this is not the case at all. It is a symptom of a lack of scholarship, I'm afraid. +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++