++++++++++++++++++ FME2001: - Review reports for paper 72 +++++++++++++++++++++ - 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: 72 CATEGORY: 1 TITLE: Modular approach to specify and validate an Electrical Flight Control System AUTHOR(S): Marielle Doche, I. Vernier-Mounier and F. Kordon -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): This paper presents a method and tool-support for the specification and verification of modular, heterogeneous systems. Modularity plays a role in both structuring (and re-using) specifications and combining validation procedures (model-checking and test generation). A final effort is put on combining existing tools on top of an open CASE system platform. 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 is a paper of category 1 which pays tribute to the FME2001 "motto" ("Formal Methods for Increasing Software Productivity") by combining several notations and tools for formal modelling and verification, and by reporting its application to a real-life case-study. 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 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: 2 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 combination of several notations and their integration in a generic CASE platform is certainly significant but not necessarily new. 6. How WORTHWHILE is the goal of the authors? Comment: It is a very worthwhile goal. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: This is my main criticism to this paper: there is too much in it - notations, logics, tools, etc. It has 22 pages full of acronyms always challenging the reader with new ingredients. Couldn't this be trimmed down? 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: The running example is small and its specs read ok as far as I could see. 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 experimental results are relevant and no doubt the authors possess a vast knowledge about how to tackle a formal modelling problem in an industrial context. But again I stress that the machinery seems too heavy for the problem which is presented. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: See some minor comments below. 11. Were there any formatting or mechanical problems with this paper?: No Are the figures and length acceptable?: The paper is a bit long (22 pages). Figures 3 (p.6) and 5 (p.19) - mentioned on p.3 - should be moved ahead. Are the references correct?: Yes 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: On the pragmatic side, I like the paper: a real example, formal tools at work, etc On the technical side, I find that something basic is missing. For instance: - The notion of a "morphism" is not formally presented. What is a morphism? a finite mapping on interface symbols? What are the "properties of the morphism" mentioned in p.15 (you refer to [18] but this is not sufficient). - How do your morphisms relate to standard signature/algebra morphisms (eg ADJ-like, cf institutions, OBJ etc)? - What does "safe" mean in "safe formal connections between the specifications"? - Your main module combinator is called "partial composition" on p.5 and "partial product" in Figs. 2 and 3. A "product" in what sense. What do you do hierarchical) module sharing? Many authors use (at theory level) the notion of a colimit to express the modular inter-combination of specification logics. How does your approach relate to this? I agree that the above questions can be partly answered by downloading your "amast00.ps" paper [18], which I did. Why not mention this paper's URL in [18]'s BibTex entry? Details: Title: Why not "Modular approach to the specification and validation of an Electrical Flight Control System"? p.5 "and computes and provides a value": delete either "and computes" or "and provides" p.9 "means the formula F" -> "means that formula F" p.9 "each of them is a TRIO" -> "each of them being a TRIO" p.11 "what is needed by a module is offers by the one": rephrase p.11 "Such are properties that express" -> "Such properties express" p.12 "is applied in [10]" -> "is applied in [10]." (A "." also missing at the end of this page's footnote). p.13 "2,605,318 arcs" -> "2,605,318 arcs." p.14 "independently and in details" -> "independently (and in detail)" p.14 "the processes follow to deal": rephrase p.15 "Validite and unbiased... of the morphism": rephrase p.16 A "." missing at the end of this page's footnote p.20 "Moka" -> "MOKA" +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++ PAPER NUMBER: 72 CATEGORY: 1 TITLE: Modular approach to specify and validate an Electrical Flight Control System AUTHOR(S): M. Doche, I. Vernier-Mounier and F. Kordon -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): This paper presents a tool-supported modular approach with complementary validation techniques (model checking and test case generation). 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: 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.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 application of an industrial case study (very small though) using a combination of different formalisms and techniques. 6. How WORTHWILE is the goal of the authors? Comment: Very 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: Yes 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: It looks like it, after a fast reading. 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: There is a little bit of everything in this paper, so in a sense it may be trying to have too many messages to pass on to the reader but I feel that the applicability is resonably justified. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: Good. 11. Were there any formatting or mechanical problems with this paper?: No, not for me. 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: I like this paper, but maybe you should focus more on what your main message of it is: mdoularity, tool-support or case study? The main thing I am missing from this paper is a proper discussion of the complementary nature of model-checking versus test case generation. Both are techniques used to gain more confidence in a correct design of a system but what kind of benefits do each of them give and what is the price of applying it. Concerning abstraction of data domains I think that you should also say that the property proved over such an abstration will depend on the correctness of the abstraction conducted. I would also like to hear about to what extend the test cases could be used for the implementation and what kind of test coverage (statement, branch) coverage which can be expeced with the automatical generated test cases. Finally I definitely think that as a complement to the presentation you should make a demonstration at the FME 2001 tools exhibition of the tool support presented. Minor comments: p3,l-6: "both the" -> "both of the" p11,l8: "property" -> "properties" p11,second last paragraph: The "bad" values you describe are exactly what model-oriented formal techniques call pre-conditions p12,para 2: This is the assumption behind partition testing! p12,sec3.3,l-1: "to TRIO" -> "to the TRIO" p13,middle: dot missing at end of para + mention what platform you measure these figures. p14,l2: In previous FME conferences there has been a couple of other important test-case generation references which you could consider including here. p14,l-11: "according modular" -> "according to modular" p15,l-11: "Validite" -> "Valid" p21,ref10: "state" -> "State" +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++ PAPER NUMBER: 72 CATEGORY: 1 TITLE: Modular approach to specify and validate an Electrical Flight Control System AUTHOR(S): M Doche, I Vernier-Mounier, F Kordon -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The paper presents a tool-supported heterogeneous formalism for the compositional specification and analysis of embedded systems. The formalisms is introduced and illustrated on an example. The design of putative tool support 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: The paper covers a number of areas of interest: compositionality, model-checking and test generation. 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: This paper presents what is essentially a pragmatic unification of disparate modelling techniques. There is little new in each of them individually, or in the modular structuring, but the practical experience of using them together is worth reporting. 6. How WORTHWILE is the goal of the authors? Comment: The goals of compositional specification and analysis, and of supporting heterogeneous formalisms are worthwhile and contribute directly to the improved industrial take-up of formal methods. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: The goals are adequately explained and justified. However, more should be made of the need for industrial-strength tool support as well as training. There should be some consideration of the deployment of the VaMoS language and tools in commercial development processes. For example, how do they contribute to the production for safety cases (the paper makes reference to *critical* embedded systems)? 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: There is only limited technical detail -we see specifications only in outline and the underlying semantics is not presented formally. Although the FME audience would probably like more of this detail, the nature of the paper justifies its omission. Such technical content as there is appears to be 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 describes an applicable technology and describes practical experience of its application. However, the paper could contain more reflection on the classes of system to which the formalisms and tools might successfully be applied. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: The writing is generally clear. Only a small number of typographical errors were detected (See section 12 below). 11. Were there any formatting or mechanical problems with this paper?: The postscript had to be distilled in order to be printable. Are the figures and length acceptable?: The paper is too long (see Section 12) Are the references correct?: Yes 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: General comments 1. The real value of the paper is its record of the experience in applying the technology and developing tool support. However, the paper as a whole is too long. I would suggest reducing the amount of background discussion. For example, Section 2.1 contains that material that most of the readers will know already. You could delete the sections on reusability and modular operations, replacing them with a couple of sentences (the advantages of modularity are sufficiently understood). 2. The technology described in the paper should be of particular use in the development of critical embedded systems. Can you discuss the use of this technology in the production of a safety case for a (safety-) critical system? How do you envisage using the tools in requirements analysis, specification and testing? 3. Minor corrections: Title "A modular approach to the specification and validation of an Electrical Flight Control System" is better English. Pg 1 Abstract line 3 "The" before "Formal" Pg 1 Section 1 line 1 lower case "e" in "Embedded". Pg 2 paragrph 3 line 1 "on verification" not "to verification". Pg 2 last line "on the specified" not "of the specified". Pg 4 line 2 "allow us to verify" not "allow to verify". Pg5 Section 2.2 bullet pont 1 line 2. I did not understand what was meant by the "prototype of actions". Pg 7 Paragraph 2 line 2 "views of the same" not "views of a same". Pg 11 paragraph 2 line 1 "is offered" not "is offers". Pg 11 Section 3.1 paragraph 1. I did not understand the last two sentences of this paragraph. Please clarify or rephrase. Pg 12 Section 3.3 line 1 "CPNs" not "CPN". Pg 14 Section 4.1 bold face "Composition according to modular operations" not "Composition according modular operations". Pg 16 final paragraph line 1 "a" not "an". +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++