++++++++++++++++++ FME2001: - Review reports for paper 28 +++++++++++++++++++++ - 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: 28 CATEGORY: 1 TITLE: Validation of UML models thanks to Z and Lustre AUTHOR(S): Lydie Du Bousquet Sophie Dupuy -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The paper deals with translating UML to Z with a view to using the formal notation of Z as a means of validating a design expressed in UML. 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 - 3 Please comment your rating: The paper deals with the integration of graphical object-oriented design techniques, specifically UML, with formal methods, which is a popular and interesting area. 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: The general idea of linking formal and informal techniques is not especially new, but the paper deals with a specific application of this to UML and Z and also discusses the application of specific tools to this transformation. 6. How WORTHWILE is the goal of the authors? Comment: The general subject area is interesting and popular, there being a significant amount of work aimed at improving the validation of informal designs in this way. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: The explanations are generally OK, but there are a few places where I think some clarification might be useful (see point 10). 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: Mostly, but there seem to be a few mistakes or incompletenesses. First, it is not clear where the basic types appearing in the UML diagram in Figure 4 are defined (AMOUNT, ACCNB, CARDID, etc.) nor how these are dealt with in the translation to Z. And the same applies to the function codefct2, which is introduced apparently from nowhere at the bottom of page 8 but which does not appear in the UML diagram. Also, it seems that the constraint on the codepin (bottom of page 8 again) is not really a constraint on the class CARD, which would imply that it was a property of all objects of that class, but rather a property of the set of cards belonging to a particular bank -- different banks could surely have different coding functions. Finally, the field MaxAmount in the class CARD in Figure 4 does not appear in the Z specification of that class. Presumably it should. 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: Generally. However, the claim at the end of section 4.1 that RoZ generated the complete Z specification from the class diagram and its forms seems to be somewhat misleading since it appears from the paper that much of the actual Z specification is contained in the forms and this has to be input by the user directly. Similar concerns relate to the claim (at the beginning of the first paragraph on page 9) that the complete specifications of the operations can be produced automatically -- it seems that again much of the actul specification has to be written directly by the user. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: The paper is generally clearly written and understandable. However, I found it very difficult to understand the last 4 paragraphs of section 4.1 (beginning "Following the same principles of annotations, ...." at the top of page 9). In particular, the word "annotations" appears to be used to describe consttraints in the Z specifications as well as some property of the UML diagrams, and the distinction is not always clear. In addition, it is not clear where the forms fit into the process. Perhaps this section could be rewritten. In addition, it is not clear where the guards (first paragraph on page 11) coe from as there is no obvious counterpart for these in either the UML diagram or the StateCharts. MOre explanation would be useful here. I also spotted a few typos: in the abstract: "lake" should presumably be "lack" in the first paragraph at the top of page 3, "default" should be "fault" in figure 4, the attribute "banlName" of BANK should presumably be "bankName", and in CARD the attribute MaxAmt should have type "AMOUNT" 11. Were there any formatting or mechanical problems with this paper?: No Are the figures and length acceptable?: OK Are the references correct?: OK 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: It might be nice to include examples and brief explanations of the other kinds of schemes mentioned at the end of seection 4.1, i.e. those describing the associations and operations (or in the latter case a pointer to the scheme CARDUpdateDateAmount and a brief explanation of how it corresponds to the UML diagrams). +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++ PAPER NUMBER: 28 CATEGORY: 1 TITLE: Validation of UML models thanks to Z and Lustre AUTHOR(S): Lydie Du Bousquet Sophie Dupuy -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The paper describes how to validate UML class diagrams and statecharts by translating class diagrams into Z specifications and statecharts into Lustre programs. The Z specification can them be validated with the Z/Eves tool, the Lustre program using the Lutess tool. 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: Relating UML with formal techniques is in the mainstream of current research. 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: 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 work presented in the paper is quite practical. The ideas are straightforward, and there are no deep research results. The merits of the paper are that the approach is systematic and tool-supported. The significance lies in the practical applicability of the work, the novelty in the concrete languages and tools used. 6. How WORTHWILE is the goal of the authors? Comment: Validating requirements is a very worthwhile goal. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: The goal is explained quite well and illustrated using a case study. By way of examples, it is demonstrated how flaws in the informal requirements document and the UML diagrams can be found. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: The technical quality of the paper could be improved. I would like to see at least one of the activity diagrams motivating the questions given on p. 4. Moreover, Section 5, where the validation of the dynamic part is described, lacks rigor and technical detail. Apart from these points, the technical parts of the paper 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: The methodology is sound, the problem treated is relevant. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: The English is fairly bad. I suggest to have the English corrected by a native speaker. For example, the frequent use of the term "thanks to" sounds strange. For suggested changes, see Point 12. 11. Were there any formatting or mechanical problems with this paper?: no Are the figures and length acceptable?: yes Are the references correct?: except some typos (e.g., pvs instead of PVS in ref. 5) and French words (e.g., Suede in ref. 8), yes. 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: Abstract, line 2: "lack" instead of "lake" Fig.3: shouldn't the use case "cancel" be <> in the other use cases? Fig. 4, class CARD: "|N" instead "\nat", "AMOUNT" instead of "AMOUT". Page 6, constraint 6: "... corresponding to the card" instead of "... corresponding to the till". Fig. 5: "ABORT" instead of "ABORD". Page 12: the last sentence of Section 4 is a repetition. There are so many errors concerning the English that I cannot list them all here. +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++ PAPER NUMBER: 28 CATEGORY: 1 TITLE: Validation of UML models thanks to Z and Lustre AUTHOR(S): Lydie Du Bousquet Sophie Dupuy -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): This paper combines a graphical, semi-formal language (UML) with two formal notations (Z, Lustre) applicable to resp. the static and dynamic semantics of the problem to model. The main goal is to start a design intuitively by using the informal diagrammatic notation, which is enriched at a later stage with more formal descriptions which pave the way to verification (integrating with resp. Z-EVES and Lutess). This strategy is illustrated with the FM'99 "cash point" problem. 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: See my comments to the next point. 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. This is a paper of category 1 which pays tribute to the FME2001 "motto" ("Formal Methods for Increasing Software Productivity") by combining informal design with formal modelling, OO-design with model-oriented specification, animation with verification, all this with a clear emphasis on pre-existing tool integration (without making a mess of everything!) Of course this has been done before, but the plan is carefully justified: each tool is used in the right context (for its own purpose) and integration is almost automatic. Should the paper be free from the defects I mention below, I would have rated it 5. 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 work is more "significant" than "new". A number of approaches to combine UML with formal modelling are available, but this one links to verification and animation in a quite sensible way. 6. How WORTHWHILE is the goal of the authors? Comment: It is worthwhile because it paves the way to the effective use of formal methods by non-formalists (eg industry). 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: The explanation is based on the FM'99 cash point problem and is in general easy to follow (modulo the problems with the English language mentioned in item 10 below). However, some aspects of the translation scheme are not put in evidence by this example (see item 12 below.) 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: not applicable 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: As I said above, this kind of approach is widely applicable (perhaps not in the formal, but in the pragmatic sense). 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: In general, the English needs improving and a careful review is required in this respect. Pages 12-14 are particularly bad. Some suggestions are listed below: p.1, l.-13: "([18, 10, 15, 17, 14])" -> "[18, 10, 15, 17, 14]" p.1, l.-10: "semantics to support" -> "semantics not only to support" p.2, l.+9: "adequation" -> "adequacy" p.2, l.+18: "statechart diagrams" -> "statecharts diagrams" p.2, l.+21: "the system models" -> "system models" p.3, l.-12: "So this part gives" -> "This section provides" p.3, l.-7: "to the statement" -> "to the problem statement" p.3, l.-1: "to express it" -> "to express this" p.4, l.-20: "No a card can be damaged and then unreadable" -> "No, a card can be damaged and then become unreadable" p.4, l.-3: "No the customer" -> "No, the customer" p.5, Fig.4: "MaxAmt: AMOUT" -> "MaxAmt: AMOUNT" p.6, l.+4: "The last day of an card" -> "The last day of a card" p.6, l.+12: "withdrawn preserves the " -> "withdrawn preserve the" p.6: isn't "state-machine" preferable to "statemachine"? p.6, l.+20: "expressed with a hierarchical statechart. The diagram 5(a)" -> "expressed by a hierarchical statechart. Diagram 5(a)" p.6, l.+26: "Informally, the statechart 5(a) represent" -> "Informally, statechart 5(a) represents" p.6: "3.4 Summary" instead of "3.4 Conclusion"? p.10, l.-7: "the operation to update" -> "the operation which updates" p.11, l.+18: "be inferior to the" -> "be less than the" p.11, l.-2: "simple theorem." -> "simple theorems." p.12, l.-20: "of Z-EVES helps us" -> "of Z-EVES helped us" p.12, l.-20: "to make precise some annotation" -> "to improve some annotation" p.12, l.-18: "The tool helps us three" -> "The tool helps in three" p.12, l.-17: "a constraints is difficult to write, the tool help us to write" -> "constraints are difficult to write, the tool helps in writing" p.12, l.-15: "we discover" -> "we discovered" p.12, l.-13: "the case that" -> "the case in which" p.13, l.+4: "It is from the responsibility of the till to determine" -> "The till is responsible for determining" p.13, l.+6,+8: "If there is stolen or damage cards," -> "If there are stolen or damaged cards," p.13, l.+9: "for the clarity of the figure," -> "for improved readability," p.13, l.+11: "and observes" -> "and observing" p.13, l.+15: "we use Lutess" -> "we used the Lutess" p.14, l.-27: "allows is to" -> "allowed us to" p.14, l.-26: "it is possible to detect" -> "we could detect" p.14, l.-24,-20:"shows" -> "showed" p.14, l.-18: "allows us" -> "allowed us" p.14, l.-15: "how semi-formal language (with UML)" -> "how a semi-formal language (UML)" p.14, l.-13: "Lustre ones. We illustrate it" -> "Lustre. We illustrate this" p.14, l.-7: "more precise" -> "even more precise" p.15, l.+3: "requires to have a" -> "requires a" 11. Were there any formatting or mechanical problems with this paper?: No Are the figures and length acceptable?: Yes Are the references correct?: Yes, in general 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: p.5, Fig. 5: This diagram involves no hierachy of classes and inheritance. How does your RoZ translator cope with multiple inheritance? You don't seem to take advantage of translating UML to an "object-dialect" of Z, eg Object-Z. Is this intentional? p.8, Z-schemas for CARD: Where is the Z constraint ensuring that attribute "cardid" is a key of "CARD"? Alternatively, you could model "Card" in "CardExt" has a finite function from CARDID to CARD (modified by removal of the "cardid" attribute). Can you transform your RoZ output in this way? Can the user enforce new translation rules of this kind in RoZ? p.14, Conclusions: A comparison of this approach to other technologies which have been around the UML, some of them already available commercially - eg VDMTools, cf http://www.ifad.dk/Products/VDMTools/rose-vdmpp.htm) - is not provided. How different is the Z <-> UML translation in RoZ from the UML <-> VDM++ "round-trip" translation mechanism provided by VDMTools? p.14, Conclusions: The paper describes how the RoZ techniques can be applied to forward engineering. Is your system ready to be applicable to *reverse-engineering* of legacy information systems? +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++