++++++++++++++++++ FME2001: - Review reports for paper 29 +++++++++++++++++++++ - 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: 29 CATEGORY: 2 TITLE: Model Checking X-Machines: Towards Integrated Formal Development of Safety Critical Systems AUTHOR(S): George Eleftherakis Petros Kefalas -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The paper recommends the use of X-Machines in the development of safety and business critical systems, while proposes a way of model checking X-Machines. Finally, it argues that X-Machines with model checking form an integrated formal method. 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: Although the authors argue that X-Machines are attractive nowadays, the paper is not convincing on using X-Machines instead of other more well-known formal languages. In particular, currently, almost all formal methods have their model checking or theorem proving associated support. Also, the paper presents initial work towards model checking X-Machines; the strategy needs to be further investigated before publication. 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: 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 technique of model checking X-Machines is argued as new. Except for the previous contribution, the paper is simply a survey about other works related to X-Machines, specifically on specification and testing. 6. How WORTHWHILE is the goal of the authors? Comment: Important for X-Machine users, since the authors present a way of model checking X-Machines. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: The authors simply show that an X-Machine can be transformed into a Finite-State Machine. As the latter has well-known model checking algorithms, the goal is achieved. 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: For finite-state systems I think the authors' goal is achieved without further considerations, since the derivation of a finite-state machine from an X-Machine seems very simple. However, for infinite-state systems I think the authors should look at the problem with more care once this problem was not solved in general, even for well-known formal languages such as CCS, CSP, etc. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: The overall organisation of the paper is good and simple. The considerations, in Section 3.4, about handling infinite domains is very informal and should be modified. The section presents this problem as a very easy task but this is not true in general. Due to this informality, I think it is more interesting to rewrite paragraphs 4, 5, 6 and 7 in order to accomplish this topic with appropriate care. There are also many typographical errors. Therefore, I think it is interesting to revise the whole paper before publishing. 11. Were there any formatting or mechanical problems with this paper?: No. Just those already pointed out in the previous topic. Are the figures and length acceptable?: Yes. Are the references correct?: Yes. But, references 9 and 12 are using " instead of `` and '' to enclose their titles. Reference 17 has a comma inside the title instead of outside. 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: In Section 3, last paragraph, the authors present the technique of Symbolic Model Checking as a technique which avoids the state explosion problem. In reality, it is one more technique which tackles the state explosion problem but it does not solve this problem in general. +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++ PAPER NUMBER: 29 CATEGORY: 2 TITLE: Model Checking X-Machines: Towards Integrated Formal Development of Safety Critical Systems AUTHOR(S): George Eleftherakis Petros Kefalas -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The paper proposes the formalism of X-machines as a specification language for safety-critical systems and claims that this notation and formalism has advantages for incorporating a formal development methodology which includes both formal verification for establishing properties of the specification, and testing to establish a correspondence between the specification and the implementation. It is possible to summarize the paper as "yet another language which extends FSM's by unbounded data-structures." 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 topic of systematic application of formal methods to a rigorous development of safety-critical systems is certainly of central interest in the FME community. It is only a pity that the paper's contributions to this important topic are not very significant. 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 idea of extending finite-state machines with unbounded data is very old. Indeed, the authors trace the origin of the X-machine formalism to Eilenberg's book circa 74. However, it is very surprising that the authors paint a picture by which nothing in this direction has been done since 74. Certainly, any proposal of using graphical automata-like notation for transition systems should be compared with languages such as Statecharts, and Levenson's various specification languages, which accomplish the same goal with higher sophistication and elegance. The authors coverage of model-checking techniques is very naive. The part that is covered in a more interesting way is the description of the W method for systematic testing. This sounds like an interesting theory, however it is not original with this paper. The weakness of the method are the strong assumptions made about the distinguishing capabilities of the partial functions \phi, and the strong assumption that the specification and implementation have precisely the same operations on the unbounded data (memory). These could be discussed more thoroughly and should be better justified. 6. How WORTHWHILE is the goal of the authors? Comment: If the goal of the authors is to propose a methodology for formal development of safety-critical systems, then it is a very worthy goal. On the other hand, if the goal is to convince us of the great value of X-machines as the ultimate specification language for achieving this methodology, then the case is very weak. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: Since X-machines were not compared at all with any other transition-based extensions of FSM's, the claim that X-machines are the best there is, has not at all been justified or supported. The fact that you can do verification relative to an X-machine, once you explicitly expand the data-dependent parts of the machine, is self-evident and, similarly that by abstracting away the data operations we can check for equivalence of two machines is also obvious. The same is true of many other FSM extensions. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: Whatever claims there have been made are sound and reasonable. 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 do not have the feeling that the authors have tried their tools on even medium-size examples. Otherwise, they would have realized the need for various ways of structuring a graphical representation of a large system. Perhaps by considering a set of communicating X-machines or other structuring techniques. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: The paper is well written. I find it strange that in presenting the frame for formal verification , the authors did not find it necessary to specify initial states. I do not know how to do verification of TL properties when the initial states are not specified. 11. Were there any formatting or mechanical problems with this paper?: No. Are the figures and length acceptable?: Yes. Are the references correct?: Greatly lacking in comparison with other state-based specification formalisms. 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: 29 CATEGORY: 2 TITLE: Model Checking X-Machines: Towards Integrated Formal Development of Safety Critical Systems AUTHOR(S): George Eleftherakis Petros Kefalas -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): This paper presents a methodology for applying model checking to system models composed from X-machines, essentially an augmented state-transition formalism. It reviews elements of the theory of X-machines and aspects of model checking before discussing the checking of CTL formulae over X-machine structures. A small example is included. 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: X-machines deserve closer attention, but this paper does not address a substantial enough step forward in their analysis to reach majority interest. 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: 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: X-machines have transitions labelled with functions accessing memory states as well as system states. The paper reports that the memory states must be taken into consideration when performing model checking, adding an additional dimension to the state space. This result is fairly obvious, although the paper does go to the trouble of presenting the necessary constructions in detail. 6. How WORTHWILE is the goal of the authors? Comment: The authors' goal appears to be to develop a methodology of system development using X-machines. This is worthwhile, although the work is not yet sufficiently mature to warrant reporting at the 2001 Symposium. It will become more worthwhile once the results have been applied to substantial case studies demonstrating an improvement in expressiveness or analytic capability over other formal techniques. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: I am unclear as to the "added value" that the use of X-machines is meant to bring over other formalisms. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: The constructions appear 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 results are demonstrably applicable, but the state explosion caused by admitting infinite data types in the X-machine memory has to be seriously addressed in order for the work to represent a step forward. Exploitation of data type invariants and the use of symbolic transition systems would appear to be promising steps forward. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: The introduction, referring to the deficiencies of the "tradition development life cycle" seems to me to be a little arrogant. The general style of the paper is fine, although there are a few little slips of phrasing. 11. Were there any formatting or mechanical problems with this paper?: No Are the figures and length acceptable?: Are the references correct?: Length is long for the actual original content: the relevance of the section on X-machine Testing (Section 2.3) was not established. References OK. 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: The paper reports a logical step forward in the development of analysis techniques for X-machine models. The work, and the paper, has some useful points. However, the impression given to the reader (rightly or wrongly) is that the step forward is too small to warrant a separate publication at this stage. It appeared to me that the paper simply says that the inclusion of potentially unbounded memory containing potentially unbounded values in X-machines means that the space of states required for model checking using conventional techniques is subject to explosion. This poses a challenge - but the paper should also report some work towards a solution. I was missing a discussion of how the techniques used to conquer state explosion in other model checking contexts can be applied here. I am sure that work towards this goal will be interesting and well worth reporting at a later stage. A specific suggestion regarding the structuring of the paper: either omit the section on X-machine testing or do more to establish its relevance to the rest of the paper. I was not clear why it was included. If it is only to establish the credibility of X-machines as a formalisms worthy of consideration for system specification, then it would be enough to simply cite the relevant literature without reproducing the constructions. The introduction could be improved in a number of ways: - Do not be so dismissive of informal development processes - they have made computing the business that it is, and that pays for our research :-) - Your methodology (Fig 1) is naïve and partial. The development of a safety critical system involves several issues that you have not considered. For example, safety analysis has to be performed on system models: this consists of inductive and deductive reasoning for the detection of hazards, not simply the analysis of a formal model for the truth or falsehood of some validation conjecture. Design steps have to be recorded and justified (all included in your one little "Step 4" arrow!) I would strongly recommend that you gain some experience of commercial development of safety critical systems before suggesting whole development methodologies. Better perhaps to offer some modelling and analysis techniques rather than a development methodology. - The specification-based testing strategy is fine in principle but it is rare to test code against very abstract specifications directly, because the level of abstraction of the implementation's input and output is so much more concrete than that of the specification. It requires a homomorphism to be set up in order to interpret concrete outputs at the specification level. There is an extensive literature on specification-based testing that should be explored. - In Section 2.1 you reveal the merit of X-machines in integrating data and functionality. This is indeed an important benefit, and you should make more of it in Section 1, justifying why you are interested in X-machines in the first place. - Page 6 Section 2.2, the formula describing the notation used - should you not have a lower case phi before "(sigma,m) = ."? - Page 7 If you do retain this section, can you include an intuitive explanation of what a state cover is and what a characterisation set is? - The conclusion at the end of Section 2 (page 8) that X-machines will provide a complete methodology for the development of a safety-critical system is plainly not justified by what has gone before. - There are just a few small flaws in the English, which could be addressed by getting some colleagues to proof read the next draft. +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++