++++++++++++++++++ FME2001: - Review reports for paper 47 +++++++++++++++++++++ - 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: 47 CATEGORY: 1 TITLE: Specification and Formal Analysis of the Light Control Problem by an integrated formal approach AUTHOR(S): J. Christian Attiogb=E9 -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The formalisation of the Light Control Problem using the "Configuration Machine Formalism" is illustrated. Techniques to analyse the resulting specification are presented. 2. RELEVANCE: Please provide a rating of the paper's relevance to the FME Symposium, using the scale: 0 =3D Out of scope 1 =3D Marginal interest 2 =3D Minority interest 3 =3D Majority interest 4 =3D Outstanding interest Numeric Rating: 2 Please comment your rating: Requirements formalisation and analysis are central to formal methods. However, the present paper is unclear and too long. 3. OVERALL RECOMMENDATION: Please provide a rating of the paper's acceptability, using the scale: 1 =3D Strong reject 2 =3D Weak reject 3 =3D Could go either way 4 =3D Weak accept 5 =3D Strong accept Numeric Rating: 1 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 =3D Know virtually nothing about this area 2 =3D Not too knowledgeable, but I know a bit 3 =3D Know a moderate amount, about average I'd say 4 =3D Not my main area of work, but I know a lot about it 5 =3D 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: I can not find much both new and significant material. The point of introducing the Configuration Machine Formalism (CMF) is not made clear. The basic structure of the formalism are transitions with preconditions and postconditions given as Z schemas with identical declaration parts. The advantages of this over the traditional expression of transitions in Z using implicit preconditions and primed variables in the postcondition is not made clear. I realise that there is a (slight) difference between the two approaches, but what makes it worthwile to introduce the CMF approach? 6. How WORTHWILE is the goal of the authors? Comment: Not very, unless it can be better motivated. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: Reasonably well. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: They appear mostly sound, although there are some mistakes. E.g. in section 4.2.2.3, when the outdoor light sensor fails, the *current* light scene is set to turn all lights on - not the *default* light scene. I have doubts about the soundness of the reasoning in section 6.1. The reasoning proves that starting from the initial configuration the sequence of transitions [user_in, Inv_Safe_Illumination] leads to safe illumination if a room is occupied. However, it is not shown that every sequence of transitions will (eventually) lead to (continuous) safe illumination. I also have a problem understanding what is meant by an "invariant" here (and also in section 2.1, third paragraph). Is Inv_Safe_Illumination actually a transition or an "proper" invariant - i.e. a requirement that any transition enabled when the invariant is enabled should make the invariant postcondition true? If it is an invariant, how do we know that the proper transitions respect the invariant (and how can we tell from the notation that it is an invariant)? Again, this illustrates that the CMF notation should be better explained and motivated. There is an inbalance in the technical presentations. Section 4 (requirements analysis and representation) is much too long and detailed, while Section 6 (Formal analysis) is sketchy. 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: No. See also 5 above. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: There are some problems with the English, but nothing that prevents the writing to be understood. 11. Were there any formatting or mechanical problems with this paper?: No. Are the figures and length acceptable?: No. The paper is much too long for its contents. Are the references correct?: Yes, I believe so. 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: Having page numbers will make things easier for the reviewer. +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++ PAPER NUMBER: 47 CATEGORY: 1 TITLE: Specification and formal analysis of the light control problem by an integrated formal appraoch AUTHOR(S): Attiogbe -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): As its title suggests, this paper contains a case study: the development of a solution to the light control problem using something called the Configuration Machines Formalism. The latter is a mixture of state-based and behavioural specification notations. 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: It will interest all those attendees whose work includes developing 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: It is a useful case study demonstrating one approach to unifying two different paradigms of specification techniques. 6. How WORTHWILE is the goal of the authors? Comment: This work relates to the current interest in combining different approaches to specification: that is certainly worthwhile. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: I was satisfied. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: Everything appears sound. However, the use of Z is rather clumsy: there is little structure in the schemas presented. This goes against the usual way of using Z. 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 paper contians the results of an experiment; the justification is obvious. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: Satisfactory. 11. Were there any formatting or mechanical problems with this paper?: no Are the figures and length acceptable?: no: the paper is 24pp. long, using a very big page format. This is not going to be satisfactory when llncs.sty is used. Are the references correct?: yes 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: You should be familiar with the work of Hoare & He. +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++