++++++++++++++++++ FME2001: - Review reports for paper 58 +++++++++++++++++++++ - 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: 58 CATEGORY: 2 TITLE: An Integrated Approach to Specification and Validation of Real-Time Systems AUTHOR(S): Adnan Sherif Augusto Sampaio Sérgio Cavalcante -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The paper describes a combination of Timed CSP and Z and a way of Mapping Timed CSP/Z specs to TER Nets, which can be analysed using The CABERNET tool. A small example is presented. 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: Combining formalisms is, although this has been Done for quite a while now and I no longer get very excited about it Myself, an important topic because it can potentially incease the Practical applicability of 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: 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: 3/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 Timed CSP/Z specs are converted to TER Nets. This raises the (unanswered) question whether or not semantics are preserved in the conversion. 6. How WORTHWILE is the goal of the authors? Comment: It is worthwhile to seek ways in which mechanical analysis can be performed on formal specifications that are otherwise difficult to analyse. 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: As far as I can judge, yes. 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. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: The quality itself is quite good. The beginning of section 2,2 has a number of typos: "none" -> "known", "bellow" -> "below", "hear" -> "here". Section 2.2 itself should be clearified, it ends with a formula without explanation. Section 2.3 and the first part of section 3 are completely unsatisfactory: the subject matter here is not well enough introduced. 11. Were there any formatting or mechanical problems with this paper?: Figures are placed on strange places on the page. Are the figures and length acceptable?: Length yes, figures are unreadable. Are the references correct?: Did not 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: 58 CATEGORY: 2 TITLE: An integrated approach to specification and validation of real-time systems AUTHOR(S): Sherif, Sampaio, Cavalcante -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): This is a case study that is broad rather than deep. It includes spcification in Timed-CSP-Z of a relatively simple case study, new results on translation of specifications in this language to Petri nets, and analysis of the translated specification using tools. The presentation leaves important questions unanswered. 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: 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.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: 6. How WORTHWILE is the goal of the authors? Comment: 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: It is very frustrating that the authors never say what the CABERNET analysis tool does. This makes it very difficult to make any sense of their comments about analysis. 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: 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: The paper could use additional proofreading and possibly checking of the English. In section 2.2, fourth line, the word is "known" rather than "none". Sec. 3.1: The term TER Net is used without having been defined. The authors frequently make comparisons among the observation models of various notations, without ever saying what these observation models are. The phrase, "a problem found using CABERNET" is ambiguous. Do you mean a problem in CABERNET or a problem in the specification? If I had any idea what CABERNET does, it would be easier for me to figure this out for myself. 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: 58 CATEGORY: 2 TITLE: An Integrated Approach to Specification and Validation of Real-Time Systems AUTHOR(S): Adnan Sherif Augusto Sampaio Sôergio Cavalcante -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): This paper presents a new notation formed by merging Timed CSP and Z. It is given a semantics via TER Nets, which enables the CABERNET tool to by used to analyse specifications. The notation is illustrated on a small example, but one that has been drawn from a larger industrial case study. 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 problem of how to handle the functional behaviour of real-time systems is one of the important problems facing many in the FM community, and these authors have attempted to tackle this by integrating two widely known formalisms, Timed CSP and Z (ensuring wide interest). Furthermore, they report on tool support for it, something which is a prerequisit to gain the interest of industrial representatives. 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: 3/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 originality of this work lies in details of the synthesis that it advocates between a timed process algebra, a model-based specification notation and Petri-nets. The significance of the work will lie in either the success that they have in developing a new formalism or in the approach to synthesis. The reviewer is not convinced that they paper describes a formalism which will find wide acceptance and use, but it seems to have some interesting ideas on synthesising these notations which should provoke some response amongst those who have presented alternative ways of integrating them. 6. How WORTHWILE is the goal of the authors? Comment: The goal is worthwhile. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: The goal is explained adequately, and a justification of it is given. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: I believe so. I have checked most of them to a reasonable degree. 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 (in the conclusions) interacts well with other similar papers and presents interesting arguments in favour of the new technique. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: The writing is adequate. In places it is a little awkward - but it is comprehensible. Suggestions for improvement (mostly minor comments): 1. Last sentence, para. 3, pape 1: This needs a little expansion - after all, some elitists (which many formalists are!) consider popularity/ popular notations things to be shunned! 2. Last words, end of 2.1, page 5: "end spec" repeated. 3. First sentence Section 2.2, page 5: delete "it" (the second word), and add comma after "mentioned". 4. Line 4, para1, section 2.2, page 5: "none" should be "known". 5. Section 3, page 7: "NEts" should be "Nets" 6. First sentence, section 3.1, page 7: This is the first use of "TER Net", and is a little surprising. What are they? What does "TER" stand for? 7. Axiom 3, page 13: "monotonically non-decreasing" is normally called "weakly monotonic". 8. Rule 4, page 13: "The time" should probably just be "Time" 11. Were there any formatting or mechanical problems with this paper?: It may not be in the LNCS format and is probably not done using Latex (something that shows in the type-setting of some of the formal text). Are the figures and length acceptable?: Yes. Although some of the figures could be bigger (i.e. have bigger text on them), Are the references correct?: They appear to be. 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: None. +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++