++++++++++++++++++ FME2001: - Review reports for paper 17 +++++++++++++++++++++ - 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: 17 CATEGORY: 1 TITLE: Model Checking Verification of Logic Control Programs in SIPN AUTHOR(S): Xiying Weng Lothar Litz -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The paper describes some additional theoretical background aspects of the CTL model checking approach for logic control programs presented in [14] by the same autors. 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: It does fit into the scope of the symposium, but the transformations presented in the theoretical part of the paper are very basic and straight-forward. For a category-1 paper, as it is declared, it does lack any substantial case-studies and methodological comparisons. 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: 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 used methods and tools all are well-known and the central "case study" demonstrating the applicability has already been published in more detail elsewhere. The small remaining part, description of the Boolean representation of SIPN transition relations to express action based CTL formulas, is straightforward. 6. How WORTHWILE is the goal of the authors? Comment: CTL based model checking of 1-safe net systems is well-known for several years now. The SMV tool by Ken McMillan does exist since 1994. SIPNs are only a "subclass" of general 1-safe systems - the firing rule is restricted here in such a way that transitions are enabled only when their postset is empty (neglecting side loops). Signals are basically a labelling of the nodes of the net. All in all, the presented transformations are not very surprising. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: The theoretical part of the paper has been done in a more informative way by explaining the necessary transformations by means of a small example. These descriptions are sound and written clearly. The paper does not present any new definitions, propositions or algorithms. 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: I have some difficulties here because the paper cannot be exclusively assigned to be practical resp. theoretical. The main idea, adaptation of SIPNs for the verification with the SMV tool, is a more practical result (This may be the reason for the placement in category 1). That study has already been presented elsewhere by the authors. The theoretical background presented in the paper on hand is too straightforward to justify this separate paper, this could have been done as an appendix of the other one. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: The paper is written clearly, but it somewhat lacks the "balance" which kind of reader it tries to address: For example, on page 2 below the exact (trivial) definition of set difference (operator '\') is given, on the other hand the notation '<-' (page 7) is neither defined nor explained elsewhere. Well-known basics about CTL or trivialities like the representation of markings of a 1-safe net system as Boolean vectors (whole sect. 3.4, about one page out of 12) are explained lengthy and in detail, while central aspects like the idea behind (O)BDDs and about their preference and applicability to the chosen approach are skipped completely. Some misprints, typos and general comments: p.2, l.1: remove the ',' after 'fundamentals' l.9: You define "F:(P\times T)\cup (T\times P) here" which is a set containing exactly 2*|P|*|T| nodes, whcih cannot be right. Either you define F as a subset of the above set: F\subseteq (P\times T)\cup (T\times P) or you can define F as a mapping: F:(P\times T)\cup (T\times P)\rightarrow N l.10: Say that M_0 is a subset of P: M_0\subseteq P. l.12: Set intersection: Change "I\wedge O" to "I\cap O" p.3, l.3: In a Boolean algebra you should also give the operation "negation" since it is not derivable from '+' and '.'. Also, the negation is used at several places later in the paper. l.-17: Insert ',': ... and x_i, respectively. l.-7: Insert ','; change '\subset' to '\subseteq': ... in a Petri net, M\subseteq P. p.4, l.-14: algebra form -> algebraic form p.4, l.-7: is -> build p.5, l.-5: "Assuming e_1 = ... = e_5 = 1": Why? Explanation! p.6, l.17: Interpunction: ... explained. l.18: for all computation path -> for all computation paths l.21: ... state, if there exits a successor of that state, in -> state if there exists a successor of that state in l.23: path, in which -> path in which l.26: \cup -> U (for CTL's "until", no set union here!) l.30: why [...] instead of (...) here? p.7, l.7: Explain the meaning of the "\leftarrow" operator l.8: delete "the" in "...satify the \exists ..." l.14: elements, which -> elements which Table 1: why are the places p_4...p_1 etc. (columns) given in descending order? l.-2: in the m_0, in -> in m_0 in p.9, l.-7 to -2: suddenly, you use some other symbols for the Boolean operators (SMV syntax: ~, &, ->, ...). Why? At least explain! p.10, l.-8: of the structure -> the structure p.11, l.4: is given, which -> is given which p.12, l-4: The URL is erroneous: wwwcad -> www-cad 11. Were there any formatting or mechanical problems with this paper?: Are the figures and length acceptable?: Are the references correct?: No complaints here. 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: In my opinion, the paper should concentrate more on either the theoretical or the practical part of the main idea. For the pratical side, try a rather exhaustive experimental analysis of this technique, such that not the technique itself but the experimental results are the main contribution. You applied the verification only to a single and very small system of academical nature (even if you declare the second one as an industrial one - note that it does only consist of 4/6 places and 9 transitions). Did you actually test some more "real-life" industrial examples? Up to what system size a reasonable verification is possible (in terms of time and space)? The discussion of such small systems may be enough for innovative techniques, but not for a rather straightforward one based on classical, well-known ideas. If you like to stress the theoretical part, above all you have to compare your approach with other existing ones. On page 6 (last paragraph) you state that "model checking algorithms in available tools are *usually* manipulated based on OBDD representations of Boolean functions". Notice that there are *many* other methods to face difficulities of the state explosion problem in the verification of concurrent systems. Have a look at the URL http://www.daimi.aau.dk/PetriNets/tools/db.html for an overview of existing Petri net based tools, many of them include a verification component that also meet the demands of SIPNs. Why do you think the OBDD method seems preferable to some of the other methods that exist? Did you actually compare them? What are the special properties of OBDDs used in the verification of SIPNs? What about concurrency? A small comparison of relevant methods/tools would be helpful here. +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++ PAPER NUMBER: 17 CATEGORY: 1 TITLE: Model Checking Verification of Logic Control Programs in SIPN AUTHOR(S): Xiying Weng Lothar Litz -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The paper establishes an isomorphism between Signal Interpreted Petri Nets (SIPNs) and propositional logic. It shows how properties of SIPNs can be expressed in CTL and verified by simbolic model checking. 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 area of logic control programming is huge, and the proposed methods appear easy to use, both in modelling and verification. 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: 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: 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: The use of SIPNs and symbolic model checking to avoid the state explosion problem in the context of logic control programming. 6. How WORTHWILE is the goal of the authors? Comment: Very worthwhile. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: Clearly. 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 is sound and has potential to scale up. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: Good quality. 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: Section 2: perhaps extending the definition of A to sets of places is in order. In particular that A({p,q}) = - if A(p) = A(q) = -, but also if A(p) = 1 and A(q) = 0. This becomes clear only at the end of the example. Section 5: typo in EF\phi: \union should be U Section 6, property 3. You are slightly cheating as the informal property does not mention Dist_Ma. I think there might be a simpler SIPN than Fig. 6 that satisfies the requirements: two places (Ma=0 and Ma=1) with a token moving between them, and similar for b. +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++ PAPER NUMBER: 17 CATEGORY: 1 TITLE: Model Checking Verification of Logic Control Programs in SIPN AUTHOR(S): Xiying Weng Lothar Litz -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): A theoretical explanation of symbolic representation of Petri net (with signals) and of the process of model checking. With a short example of model checking a SIPN model (that was already published in detail). 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 deals with model checking of a class of Petri nets. The subject itself is interesting. 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. I don't see why there should be a correlation. The first has to do with the subject of the paper that is interesting. I think that the paper itself is unfortunately not interesting. 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: The paper does not seem too original. The paper consists of a survey of how to translate a Petri net to a boolean function in order to facilitate using state-space minimization techniques (SMV). The construction seems straight-forward and as using SMV on general Petri nets is a common practice, I believe that the analysis does not reveal anything new. Furthermore the explanation of CTL model checking is also not relevant and there are various publications on the subject. 6. How WORTHWHILE is the goal of the authors? Comment: Explaining the theory behind symbolic model checking is a worthwhile goal. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: The paper is very well written. It is clear and legible. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: Sound but seems quite obvious. 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 7. 11. Were there any formatting or mechanical problems with this paper?: Are the figures and length acceptable?: Are the references correct?: Typo: Page 6 definition of A(phi U psi) there is a \neg missing after the = symbol The example: It seems that the example given in Fig. 3 is a very bad example. Although the net does exactly what the specification wants it to do, it seems that SIPN (or the definition of CTL the authors choose to use) is not sufficient to cope with the specification and needs the integration of two superfluous locations (in Fig. 6). The best solution in my opinion would be to set Ma=S1 and Mb=S2. In this case all the proofs work for Fig. 3 (as S1+S2+S4+S5=1 and S2+S3+S4+S6=1 are invariants of the system it is clear that Ma=1 iff s1=1 and the same for Mb). The authors actually use variables like S1 and S2 in another formula they check. So there is no reason not to use it in the first place. So it seems to me that the authors are in fact giving an example why SIPN should not be used because it causes an unnecessary blow up in the nets. 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: The authors' work from ACC2000 is a bit hard to access. It would have been very useful if it was available on their web page. +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++