++++++++++++++++++ FME2001: - Review reports for paper 16 +++++++++++++++++++++ - 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: 16 CATEGORY: unspecified TITLE: Towards a Formalization of the UML State Machine using Object-Z AUTHOR(S): Soon-Kyeong, Kim David Carrington -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The authors use the Object-Z language to define a formal semantics to the State Machine package of UML. The paper somehow complements previous work (by the authors) dedicated to the formal semantics of other UML packages. 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 topic addressed is an important one in the sense that UML is becoming increasingly accepted in industry, and that there is no formal semantics of consensus yet for UML. Nevertheless, the contribution of the paper is confined to one more formalisation of the state machine package. Apart from being strongly based on statecharts (which has itself several formal semantics), there are already formal semantic definitions specifically addressing the UML variation. While the authors justify that the UML state machine has important semantic differences to classical statecharts, they do not present any concrete benefits of their semantic contrasting to references [16] and [17]; only a very vague argument is giving: "In our opinion, however, their semantics are not complete and less formal". This affirmation should certainly be supported by a more careful and precise explanation. Another important justification for this work should be presented in terms of how suitable this semantics is for formal validation and verification; nothing is mentioned in this direction. 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: 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 authors claim that their semantics is complete, modular and extensible, but no comparison with, for example, references [16] and [17] is presented. 6. How WORTHWILE is the goal of the authors? Comment: The goal of having a complete formal semantic definition for all UML model elements is certainly worthwhile, but this has to evolve together with a proof theory and strategy. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: The goal is clearly explained, but not well-justified, as already mentioned in item 2 above. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: As far as I can tell the definitions are 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: This is a major weakness of the work. No use of the semantics is reported; therefore the arguments about its benefits are vague. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: In general, the paper is well-written and presented. - The AirConSystem example (page 2) has a small typo: constant "desiredTemP" is used in the invariant part as "desTemp". - A brief explanation of Figure 2 would help. 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: 16 CATEGORY: unspecified TITLE: Towards a Formalization of the UML State Machine using Object-Z AUTHOR(S): Soon-Kyeong, Kim David Carrington -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): This paper defines the semantics of the State machine package of the UML meta-model. The UML models of this package are translated into Object-Z specifications which are completed by constraints corresponding to the English or OCL descriptions of the package. 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: Defining a semantics of UML is worthwhile in order to better understand it. Moreover the use of formal specifications should permit to detect the eventual inconsistencies of the UML meta-model. But I wonder if Object-Z (in particular this extension for timed refinement calculus) is the most appropriate formal language: it does not really have itself a precise semantics and it does not provide tools to analyze the specifications. Finnaly, the conclusion is too short and does not give any perspective of the work. 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: 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 rests in the definition (into a single formalism) of the semantics of the dynamic part of UML which includes the UML meta-model and its comment in English or in OCL. 6. How WORTHWILE is the goal of the authors? Comment: The goal is very worthwile: UML is widely accepted for modeling, but its semantics needs to be better defined in order to avoid misinterpretations and bad use. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: All the goals are explained and justified in the introduction. But I think the advantages of using Object-Z should be cited instead of refering to other papers. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: Globally, the Object-Z specifications seem correct. Nevertheless I have the following questions/comments: In page 13, in the State class, the only operation visible are Enter and Exit. Why (how accessing to ExecuteEntry, ExecuteActivtity ...)? In page 16, the operational semantics of transitions do not mention the end of activities before executing the exit actions. Why? In page 4, there must be an error in the AirConSystem: in the definition part, the name used for the desired temperature is "desiredTemp" whereas in the timed refinement calculus part, it is "desTemp". 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: Working with UML as modeling language shows a concern of useability. The choice of Object-Z is also justified by a concern of readability of the formalization. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: A well-written paper, but sometime some part of the Object-Z specifications should be better explained. Each constraint should be formulated in english in the text. * page 4: the first part of the AirConSystem is not explained * page 8 and 9, constraint 6 and 8: the mapping from the english text to Object-Z is not evident * page 14: give the english expression for the constraint of the CompositeState class * page 15: the explanation of constraint 1 is not really clear 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 introduction is a bit too long and the general explanation of the solution (from In our work...) is not really understandable before reading the whole paper. I think this part could be shortened or reused in the conclusion. Develop the conclusion by giving perspectives of the work. Could you also explain how the Object-Z specifications could be used for consistency checking? +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++ PAPER NUMBER: 16 CATEGORY: unspecified TITLE: Towards a Formalization of the UML State Machine using Object-Z AUTHOR(S): Soon-Kyeong, Kim David Carrington -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): This paper uses Object-Z and timed refinement calculus to formalize, in a modular way that fits with the author's formalizations of other parts of UML, the 'state machine' package which is part of the UML meta-model. 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 does not contribute new results or ideas. Rather, it uses known ideas to give a formal definition for a key part of UML. This will interest a good part of the FME community, as UML is widely used in practice. 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 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 work gives a more formal semantics for UML than has been given, but there do not seem to be significant new ideas. 6. How WORTHWILE is the goal of the authors? Comment: Given that UML is widely used, it could be valuable to formalize its semantics, especially using relatively accepted formalisms like object-Z and interval temporal logic (timed refinement calculus). 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: Adequately, but not compellingly. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: There is essentially nothing but definitions. The paper does not include all of the definitions, which appear in a tech report, and I am not sufficiently expert to be sure that they accurately reflect the informal UML spec. But I believe the work is 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: The paper does not make a compelling case for the usefulness of the formalization, but rather relies on the reader to believe that there is value in formalizing UML semantics, and in doing so using modular notations of Object-Z. But this is quite reasonable. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: The writing is fairly clear. I had a small amount of confusion about terminology. A 'denotational' semantics is given for what I would call static aspects of the dynamic semantics (e.g. description of state) and 'operational' semantics is given for sequences of states. This is in contrast with the typical use that denotational and operational are two different styles of describing the same dynamic phenomena. 11. Were there any formatting or mechanical problems with this paper?: 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 ++++++++++++++++++++++