++++++++++++++++++ FME2001: - Review reports for paper 66 +++++++++++++++++++++ - 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: 66 CATEGORY: 1 TITLE: Using formal verification techniques to reduce simulation and test effort AUTHOR(S): O. Laurent P. Michel V. Wiels -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The paper discusses the application of formal verification to the flight control computer of the Airbus A340 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: 4 Please comment your rating: The fact that the application is the Airbus A340 makes this paper appealing. 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 particular system that is analyzed. 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 general goal is explained well enough. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: yes, except the definition of E -> F in section 3.1 looks fishy. 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: pure application 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: writing is adequate 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: There are no specifics provided about how the A340 fault detection, isolation and reconfiguration (FDIR) system works, so one is left with two abstract properties: P1: if we suppose that the two sidesticks cannot be faulty at the same time, there is always an active stick. P2: if the two primary computers PCI and PC2 are faulty, then the secondary computer SCI becomes operational. and no idea whatsoever what was required to prove them. If the model of the FDIR system is very abstract, the proofs were probably trivial. If the model is a detailed design (i.e. almost code), then the proofs could be quite challenging. I suspect we have the former case here. The only information given about the model of the system was Ten nodes were selected concerning this property, nodes that express the relationship between the inputs (pilot and copilot order, faulty sticks) and the outputs (transmitted order, priorities). These nodes are essentially composed of - nodes for the management of priorities, nodes for monitoring and nodes for the functional part. Then a main node was automatically built from these selected nodes. which was not sufficient to gain an understanding of the A340 system model. +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++ PAPER NUMBER: 66 CATEGORY: 1 TITLE: Using formal verification techniques to reduce simulation and test effort AUTHOR(S): O. Laurent P. Michel V. Wiels -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The paper describes the use of formal verification techniques (proof) in an industrial setting in order to reduce efforts during simulation and testing. 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 combination of verification and validation techniques in order to reduce costs and effort during the development phase is a meaningful undertaking. 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 idea of combining verification and validation techniques is not new nevertheless their deployment in an industrial setting and on a real life project are significant and worth reporting. 6. How WORTHWILE is the goal of the authors? Comment: As pointed out earlier, the goal is worth pursuing and the application of theoretical work in practice and the lessons learned are worth reporting. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: The goal is explained adequate and reasonably well justified. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: There seems to be no problem with the specifications. 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 examples are small and acceptable for a paper. The discussion of the examples is adequate. Unfortunately only the application of the technique is discussed and the goal of reducing the effort is ot demonstrated. This should not be difficult to add. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: It is a bit difficult to follow the examples if the reader is not familiar with avionics. And some of the explanations are not easy to follow because information is withheld from the reader. The reader is then not able to follow the argument described in the example. The use of for example "the pilot order is different from 0" (page 4) is confusing and can not be understood by the reader. 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: 66 CATEGORY: 1 TITLE: Using formal verification techniques to reduce simulation and test effort AUTHOR(S): O. Laurent P. Michel V. Wiels -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The paper reports on work towards a strategy for identifying and proving properties for specifications written in the Lustre language, with a major objective of reducing simulation and test efforts. The work has been carried out in the context of development of embedded systems for aircrafts. 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 approached by the paper is of much interest for the entire formal methods community, but the research seems still to be in a very initial stage of development. The results reported are very modest. Furthermore, some aspects of the proposed strategy should perhaps be considered in a more general software engineering process perspective. In particular, all the difficulties reported concerning the identification of the relevant properties to be verified is clearly a consequence of a development process without an adequate requirements elicitation phase. I understand that, for this first experiment, the work by the authors had to be inserted in the current development process of the company; however, rather than assuming this context for future experiments, it seems more natural to to invest in a process which contemplates a proper requirements elicitation phase, avoiding all the complexity reported for identifying properties. 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: 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: No general strategy has been proposed yet, just the report on some experiments. 6. How WORTHWILE is the goal of the authors? Comment: Very worthwhile, but considering the comments in item 2. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: the objectives are clear. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: Not much technical material. 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 work has been developed in an industrial context, so its applicability veru clear. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: A short report, but clearly presented. 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 ++++++++++++++++++++++