++++++++++++++++++ FME2001: - Review reports for paper 19 +++++++++++++++++++++ - 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: 19 CATEGORY: 1 TITLE: Evaluation of B specifications using Constraint Logic Programming with sets AUTHOR(S): Fabrice Bouquet Bruno Legeard Fabien Peureux Laurent Py -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): Theoretical basis for animating B specification via Constraint Logic Programming 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: 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: 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: 6. How WORTHWILE is the goal of the authors? Comment: The goal is to be able to execute B specifications for validation purposes. This is an important capability. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: The goal was explained well. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: 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: theoretical 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: quality of the writing is 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: I am concerned that there is not much difference between this paper and the paper presented at LPSE'2000 (July 25, 2000). If I am wrong about this I would gladly raise my score. +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++ PAPER NUMBER: 19 CATEGORY: 1 TITLE: Evaluation of B specifications using Constraint Logic Programming with sets AUTHOR(S): Fabrice Bouquet Bruno Legeard Fabien Peureux Laurent Py -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The authors present a CLP-based constraint solver for the simulation of B specifications. This solver is able to compute with sets of states described by constraints. 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: 1 Please comment your rating: Being assigned to category 1, the paper covers the "use of formal methods" but doesn't fit into any of the elements of the following "including" section. Furthermore, the paper's range is "all other aspects of the use of FM" and does not really address one of the eight given subjects - a little bit of "enhancing analysis techniques for validation and verification" maybe. The paper might be better suited for a conference on Constraints, or on the B method, respectively. 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: 1 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? Well - yet another B specification simulator. In the conclusion, the authors claim their simulator or rather their concepts may entitle one to perform model checking of B specifications (as opposed to the simulator in Atelier-B, but not quoting the tremendous amounts of work on the verification of B specifications). This is, however, not the subject of the paper; it's merely the simulator that is described. If I got it right, one crucial point is that they perform computations with "constrained states" or, thus, sets of states. The operational model induced by the constraint solver thus amounts to a sort of abstract interpretation (see, e.g., their example where congruence classes of states are being computed). But - this operational model is not complete in that not all traces of the original system are covered (which, w.r.t. a class of properties, I'd call incorrectness rather than incompleteness). Which traces are missing? And I wonder how the "abstract traces" - traces of sets of states - relate to concrete traces. Model checking of an abstraction does only make sense if we can ensure something like A|=P => C|=P where C is the concrete, A the abstract system, and P a property. I'd call this correctness w.r.t. a class of properties. Achieving correctness if the constrained (abstract) traces do not even cover all concrete traces. What properties are to be checked - i.e., which properties are preserved by the "constrained system"? When talking about invariants of a constraint store - p. 12, without touching upon the problem of invariance preservation of the operations on the constraint store - these invariants are not invariants of the system but rather of a snapshot of the constraint store. If invariance preservation is not guaranteed (which may or may not be the case) : what's the use of such invariants? Due to the "incompleteness", the "constrained system" is a mixture between generalization and concretization. I think it is possible to shed a different light on the author's approach by considering it a technique for testing (where incompleteness is a general problem, anyway). The authors talk about "validation" and use "model checking" and "animation" as the only instances - animation is achieved by other simulators, model checking is not really taken into account, and, in my opinion, will not work in a sufficiently generalized setting with this approach. One new point is the augmentation of constraint solvers for sets with sets that may contain variables rather than merely atomics. However, I think the relationship between model checking, abstract interpretation, and CLP deserves some serious attention. I'd suggest to consult Cousot's work on model checking and abstract interpretation, Bruynooghe's on AI for CLP, Dams&Gerth&Grumberg or Clarke&Grumberg for the problem in general (with a bias towards reactive systems). Graf's, Bensalem's, Rushby's work on automated abstraction also is closely related to this topic. Gaudel's or Tretman's/Brinksma's ideas on formal testing could be interesting, too. 6. How WORTHWILE is the goal of the authors? Very worthwhile - if the focus is on general validation and not some ad-hoc simulation or ad-hoc union of system traces. In my opinion, and according to my view on their work (which boils down to some kind of an abstract interpretation approach, see above), CLP is a high potential for that kind of abstraction-based validation. However - this topic is not sufficiently treated; it rather looks like an ad-hoc implementation. No properties of the "abstract", or "constrained", system are actually proved. 7. How well is this goal EXPLAINED and JUSTIFIED? Not really. There are no references to validation/verification approaches for B specifications; the focus is on their implementation on the basis of CLP with sets. Furthermore, one crucial restriction of their work is the focus on finite systems, which also applies to model checking. A reduction of the number of states from exponential to quadratic order is claimed for their example, but the relationship between original and abstract system, i.e., the system based on constrained states, is not clear. Again, what's the relationship between the original and the "constrained" system? 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Sound - looks like it (exc. page 8, see below), complete - no. The paper is not self-contained at all, which I'd highly recommend for future versions. Crucial concepts such as "constraints" or "state variables" are not defined. The computation domain of sec. 2.1 is paraphrased as "B method set theory without" - I could use some more formalism here. In sec. 2.3, "constraints management" talks, blurrily, about several domains, stating that "this calculus is not possible with a deterministic approach". Well, nobody talked about a calculus yet. Definition 5 defines "meaningful" without ever reccurring to this term. On page 8, invariants are claimed to hold iff a set of constraints contains them - without talking about the transitive nature of entailment (it might be the case their claim is true - which I doubt - but in this case, a proof or justification would be helpful). The same point arises in section 3.1, where, again, the problem of the calculus's incompleteness arises (see comments above w.r.t. abstracted programs). On page 15, bottom, it is claimed that "invariant constraints are satisfied or could be entailed" - but the process of checking entailment is not taken into account. What are the invariants you talk about? Those of a snapshot of the constraint store? If so - why is this interesting; a proof or justification of the preservation of invariants is necessary. Finally - is "satisfied" the same as "satisfiable" in sec. 2.3? 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? As stated under 5 and 8, I see the need for justifying the applicability of the author's approach. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. I'd suggest to put the example not in an appendix since it is quite necessary to understand the application related parts of the paper. I'd also suggest to make the paper a little more self-contained, a little less roughly describing the concepts underlying B, and more precisely talking about terms such as constraints". Other than that, the paper is written in a somewhat nasty English. In terms of content or argumentation, I'd propose to include a paragraph on the nature of properties that can be verified using their approach. Without this, the simulator is just another simulator which claims to be potentially suitable for validation/verification purposes. 11. Were there any formatting or mechanical problems with this paper?: no Are the figures and length acceptable?: I don't see the need for tables 1 and 2. Are the references correct?: yes. (lacking some, see above). 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: To highlight my main points of criticism: 1) A simulator is presented that is claimed to be suitable for validation purposes such as model checking. There are lots of simulators; for me it is not clear how model checking with the author's approach could work. They don't really take care of this point. 2) The nature of the induced system (by simulation of sets of traces) w.r.t. the original one is not clear. Which properties are preserved? In terms of related work that could be interesting, see point 5. Furthermore: I'd suggest a thorough spell checking of the entire text. Abstract: "constraint resolution to" should be "of" "consistence" -> "consistency" Sec. 1, p.1 "in terms of abstract machine" -> "an abstract machine" p.2, top: call->called what's a substitution? "This approach lies between ...": there you even explicitly say you cover only a subset of all traces. Why model checking, then? (see above). middle: "do not provide sufficient ..." - be more specific! p.3 top: Predicates: FO predicates. bullet 4: of all given setS Def. 2 - why don't you formalize everything in a positive manner? bullet 2: "Given set" -> "Given sets are" p.4: what's a substitution? what's a state variable? bottom: triplet->triple p.5 top: what's a constraint? first paragraph: first sentence ambiguous; which calculus? Def. 4: defined by "the" constraint - which? Def. 5: meaningful? p.7: ex 5, line 2: et -> and Def. 7, line two, second last word: "as" -> "such that"? Ex.6: satisfied=satisfiable? "If we take" -> "If we took" p.7, Thm 1.: satisfiable? Note: satisfiable? How can completion be performed? As you noticed, I think it's a crucial point. p. 8: P2 - Don't you induce a loss of information here (concerning incompleteness)? why?! bottom: (E=> ...) what is "so"? Justify or prove the claim - I don't believe it, see above. Furthermore, what exactly are the invariants you are talking about? It would be interesting to talk about invariants of the system rather than of the constraint store. I'd like to see a result on how invariants are preserved by the inference/rewriting rules, see above. p. 10/11: What do you need the tables for? p .12, middle: "activable"? bottom: invariant verification: I don't believe it - prove me wrong! (I see a problem with transitive entailment here) p. 14: put the example here - it's needed! p.15, bottom: "could be entailed" - well, that's what I meant the whole time! How can entailment be checked? p.17 top: no "of" in the first line. p.18, appendix, is "the set of sex processes" a bad joke? +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++ PAPER NUMBER: 19 CATEGORY: 1 TITLE: Evaluation of B specifications using Constraint Logic Programming with sets AUTHOR(S): Fabrice Bouquet Bruno Legeard Fabien Peureux Laurent Py -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The paper presents a system for the evaluation of B specifications using constraint logic programming. It provides support for propagation of non-determinism and calculation of the graph of reachable states. It does not adequately address structuring of B specifications into machines and so the scalability of the approach is questionable. 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 approach is interesting and potentially very useful. There is some doubt whether the semantics offered by CLP is equivalent to the B semantics (although this probably does not diminish the usefulness of the tool). It is not demonstrated that the approach is scaleable - the example specification is very small and does not use B's structuring mechanisms which are a major strength of the method. 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 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 approach is new and, if scaleable, has potential to be a great significance. But it needs to be shown to be able to utilise appropriately the structuring mechanisms available in B. If this could be done, it could provide a useful addition to the functionality already offered by the B-toolkits. 6. How WORTHWHILE is the goal of the authors? Comment: The ability to model check B specs is a very worthwhile goal. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: The paper is well structured and clearly explained. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: The paper looks sounds (modulo differences between CLP and B semantics) although I did not check it in absolute detail. 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 application of CLP to B is new, but the work does not adequately address the structuring of B specifications which is a major feature of the B method. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: Some improvements to the English would help ease of understanding. 11. Were there any formatting or mechanical problems with this paper?: No. Are the figures and length acceptable?: Yes. Are the references correct?: Yes - I have seen the example process scheduler before (perhaps in Dick's paper which you cite), please give reference. 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 ++++++++++++++++++++++