++++++++++++++++++ FME2001: - Review reports for paper 07 +++++++++++++++++++++ - 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: 07 CATEGORY: 1 TITLE: Transacted Memory for Smart Cards AUTHOR(S): Pieter H. Hartel Michael J. Butler Eduard de Jong Mark Longley -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): This paper describes an attempt at modelling, prototyping and testing a memory model for smart cards that supports persistent management of multiple generations of data (based of EEPROM technology). The specifications and refinements re (mostly) in Z, the prototypes in C and SPIN. 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: 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 paper is a bit of a mixed affair. On the one hand it is nice to see formal techniques applied to real problems. On the other hand there are lots of gaps in this development, and the paper refers the reader to a tech report for most of the technical details. Thus the technical difficulty of the whole enterprise is hard to asses from the paper alone, although it is probably not completely trivial. Although I would have preferred a more technical description, the paper is acceptable if the authors fix some of the problems I mention below. 6. How WORTHWILE is the goal of the authors? Comment: Very 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: Very well 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: There are a number of gaps that are acknowledged, but otherwise it seems 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: 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: see below 11. Were there any formatting or mechanical problems with this paper?: Are the figures and length acceptable?: Are the references correct?: 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: Please add more technical details, in particular: 1. the refinement relation in step 1 2. a discussion of the non-Z constructs you used and why 3. a description of the assertions used in the SPIN runs. Point 3 is absolutely essential - otherwise the reader has no idea what has actually be shown by SPIN. As a compensation you should cut back on the very verbose descriptions in 4. For example 4.4 contains parts of 3.1, which does not need repeating. It is also a bit frustrating that the second refinement step is not really a refinement because it adds extra behaviour. The authors should say more clearly how they would deal with this problem in a real verification. +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++ PAPER NUMBER: 07 CATEGORY: 1 TITLE: Transacted Memory for Smart Cards AUTHOR(S): Pieter H. Hartel Michael J. Butler Eduard de Jong Mark Longley -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The paper presents the specification of a model of transacted memory and its refinements using Z. Then the model is manually implemented in C and prototyped in SPIN. Lessons about the use of several formalisms and tools are sketched at the end of the paper. 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: Clearly, the paper addresses the use of formal methods. The approach is presented through a case study, but Section 6 aims at extending the scope 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 The paper is only based on a case study and some parts are very technical and difficult to read. Nevertheless the lessons learned can be useful. 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 case study has not been specified before. The presented approach with a formal development followed by translation in C for testing and in SPIN for animating is interesting. 6. How WORTHWILE is the goal of the authors? Comment: The main worthwhile thing is the discussion about the merits and drawbacks of the proposed development with several formalisms. However, it is rather limited to the kind of errors found at various stages. Moreover, the refinement proofs as well as the final translations are not formally checked. This weakens the guarantee of development correctness. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: The goal is well explained. Some parts are very technical, for example Section 5 with C or SPIN fragments of the case study. I am not sure that the reader is able to understand the paper without knowledge of the used languages. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: The paper is only based on a case study. 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 falls in the last case (experimental results). The authors claim that the case study comes from a real challenge, namely to reach the EAL7 level of Common Criteria for the smart card operating system kernel. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: Quality is good excepted when too technical details are presented. Specially Section 4 (introduction of the "realistic constraints" and error recovery) and Section 5 are difficult to read. 11. Were there any formatting or mechanical problems with this paper?: No Are the figures and length acceptable?: Yes Are the references correct?: I think so. 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: The work done with other formalisms on the specification of smart card memory transactions should be mentioned and optionally compared. For example: [D. Sabatier, P. Lartigue] The Use of the B Formal Method for the Design and the Validaion of the Transaction Mechanism for Smart Card Applications, in FM'99, pp.348-368, LNCS 1708. Finally, it is not clear if the approach presented in the paper should be followed in the future (see your last sentence). So, this paper does not provide a convincing contribution to the benefits of formal methods. +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++ PAPER NUMBER: 07 CATEGORY: 1 TITLE: Transacted Memory for Smart Cards AUTHOR(S): Pieter H. Hartel Michael J. Butler Eduard de Jong Mark Longley -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The authors present a memory management model for smart cards. The model is formalised in Z and refined into C/Promela code. Experience from the development process is given. 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: Applied methods and experiences should be of interest to most FME participants. 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: 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: From a formal methods point of view, not much. The paper is an exercise in program development by refinement. Many such exercises have been published. The significance of the paper is primarily to be found in the discussions of problems with the specification/refinements and how they were found. However, the results are essentially what one would expect. The approach of performing analyses of code translated from refinements (assertion checking Promela programs, testing C code) is interesting, but there is no discussion comparing this with the more direct methods of proving assertions from the Z specifications or checking the specification by animation. 6. How WORTHWILE is the goal of the authors? Comment: Very. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: Briefly. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: Yes. 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 proposed is sound. The relevance of the experimental results is not sufficiently justified. See 5 above. 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 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: On page 11, the reference to section 5.1 should be section 5.3. +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++