++++++++++++++++++ FME2001: - Review reports for paper 18 +++++++++++++++++++++ - 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: 18 CATEGORY: 2 TITLE: Exploring Timing Properties Using VDM++ AUTHOR(S): Paul Mukherjee Fabien Bousquet Jérôme Delabre Stephen Paynter Peter Gorm Larsen -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The paper describes the use of VDM++ and its tools to model and explore the timing behaviour of specifications. 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 subject matter would rate a higher interest, but the technical quality is not very good. 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 extension to VDM++ is new, but the general ideas of simulating time are not. 6. How WORTHWILE is the goal of the authors? Comment: The idea is useful. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: Reasonably well. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: What is described seems sound, but the whole does not hang together well. 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: Seems applicable. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: The specifications on grey background are almost unreadable. Further comments below. 11. Were there any formatting or mechanical problems with this paper?: No Are the figures and length acceptable?: Figures mostly useless; paper is longer than it needs to be (see below). Are the references correct?: Yes 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: Time is added to VDM statements as an additional attribute. Statements may be grouped together and the group given a duration. Two orthogonal issues seem confused here: the possibility of grouping statements for giving timing information, and different sources of that information. The claim is that timing can be tested prior to implementation, yet the so-called default times for individual statements are based on assembly code instructions. If you know the assembly code corresponding to VDM++ statements it is difficult to see what more is to be done to implement them. The semantics presented in section 3.3 is very simple, and suggests that threads have no conditional or looping constructs. This turns out not to be true in the later example, so one is left confused. If threads are just sequences interleavable by scheduling, then surely the total number of switches, for n statements distributed across k threads, is between k-1 and n-1 inclusive. The number of switches will depend on the scheduling policy. The total execution time is just the sum of the statement times plus the number of switches multiplied by the switching overhead. The explanation of this obvious fact is both tortuous (with several pages devoted to the conceptually simple but tedious details of how to construct the set of all possible traces) and confusing because the example changes half way through (and the fact is never stated as a conclusion). Allocating timings for compound statements as zero for all but the last does not change the theory in any substantial way, and hardly merits another page and a half of explanation. It does raise the interesting question of what to do about the times of intermediate events, which will presumably be wrongly reported, but this is not addressed. Apart from the fact that there is a tool that can generate traces, from which statistics and graphics can be extracted, it is difficult to see what this has intrinsically to do with VDM++ or formal methods. What normally distinguishes formal methods from programming languages is a logic, the basis for an ability to reason. For example, if add is a method that adds one to an instance variable, then one might expect in such a logic to be able to reason that add(1) ; add(1) is equivalent to add(2) (perhaps under some exclusion condition if there are concurrent threads). If timings are added to statements this may no longer be true. This problem is not addressed. The extension to multiprocessors may in principle be possible, but it surely warrants more discussion than this single remark. +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++ PAPER NUMBER: 18 CATEGORY: 2 TITLE: Exploring Timing Properties Using VDM++ AUTHOR(S): Paul Mukherjee Fabien Bousquet Jérôme Delabre Stephen Paynter Peter Gorm Larsen -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The paper proposes extensions to the VDMTools environment in order to take into account timing information in the design and validation of systems. 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 authors improve one of the most popular formal methods environment in order to cover timing properties. Validating timing properties of critical systems is definitely an important challenge for both the industrial and academic research communities. 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 authors propose a nice extension to the IFAD tools. These tools allow the validation of specifications based on simulation/testing. This paper adds the possibility to also validate some timing properties based on simulation/testing. 6. How WORTHWILE is the goal of the authors? Comment: The goal is very worthwile! Personally, I feel it is of great help in the design of an architecture for a critical system, because it allows to evaluate the performance of the proposed design. I know several industrials who would be very happy to try such a system. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: The goal is explained correctly. But the technical parts, in particular a first specification of the timing semantics is very badly explained: the specification is not commented enough and some non-obvious design choices are not commented at all. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: I did not find errors, but I must confess that I did not completely understand the specifications. Some parts of the specifications are poorly commented and I am not able to figure out if they model the correct reality. For example, on page 7, the specification of "FromThread" checks for the inclusion of two sets, but personnally I would have also checked that the elements appeared in the right sequence. Unfortunately, since this point is not commented I can't figure out whether this is a conscious modeling choice or an incomplete specification. 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 to a case study is a definite argument for the applicability of the work. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: This is my major problem with this paper. The paper tries to cover too much material (presentation of the work, presentation of a restricted semantics, presentation of a case study), as a result many sections seems to be unnecessary for the paper. In particular, the formal sections 3.3 and most of 4.2 are not really needed to understand the paper (but I can tell you that the reader spends too much time trying to understand these... and then you understand that you can't understand as already said under 8.) The two formal sections should be more commented. The typical participant to FME is not necessarily fluent in VDM++. And even if you are fluent in VDM/VDM++, there are several design/modeling choices that are not commented and cannot be understood. I recommend that you skip section 3.3 which does not contribute to the paper and use the available space to detail/comment the case study. (I think that such poorly commented formal specifications are a counter-example of formal specs because they tend to enforce the idea that formal specifications are unreadable) 11. Were there any formatting or mechanical problems with this paper?: Are the figures and length acceptable?: Are the references correct?: OK 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: My first reaction to this paper (when I read the introduction) was: "VDM was not designed for reactive systems, moreover, timing constraints are an independent concept with respect to specification which is supposed to favour implementation freedom". The rest of your paper is quite convincing that these additional features make sense, but you might find it interesting to discuss this independence topic. Another topic that does not receive so much interest in your paper is that the (timing) behaviour of a system is also linked to the timing behaviour of its environment. How do you describe this timing behaviour? page 5. Section 3.3 semantics. Here are some examples of badly commented specifications: a) "a timed statement consists of a statement and its duration" Here you should justify why you don't use a map between statements and durations. Your specification suggests that the same statement may have different durations? Please explain if this is the right interpretation and why this makes sense? b) The definition of "Interleave" is very complex, not only because it uses "FromThread" which is badly explained, but also because of this combinatorial arrangement. I spend some time trying to understand it and finally decided there is probably some subtle semantic point I don't get. Section 3.4 is supposed to illustrate 3.3, but the example given here is definitely too simple to illustrate all the aspects of 3.3. Actually the example is useful to understand the next sections, but not 3.3 which seems to be unnecessary for this paper.(just say you have a formal semantics, the reader will trust you) Section 3.5 is too short. Please take some time to explain it in detail. For example, I did not understand that the duration statement may apply to a sequence of instructions (as shown later in the paper). In section 3.5, you say that the environment can be modeled using "duration(0)" statement. You are right, but how do you also make sure that the switching cost corresponding to these parallel execution is also 0? In your case study (page 14) I don't understand how the timer "wakes" the FlareController. Also, I did not understand some elements of the notation such as the square brackets in [Sensor`MissileType] and the "sync" statement in "StepAlgorithm" page 18. You give three interesting timing properties. These are expressed in English. It might be interesting to use some real-time temporal logic as a language to express those properties (in order for the VDMTools environment to check these at test/simulation time). +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++ PAPER NUMBER: 18 CATEGORY: 2 TITLE: Exploring Timing Properties Using VDM++ AUTHOR(S): Paul Mukherjee Fabien Bousquet Jerome Delabre Stephen Paynter Peter Gorm Larsen -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The existing formal notation VDM++ with its toolset are adapted to enable exploration (note: not formal specification or proof) of timing properties of a formal model of a deterministic closed system. 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 paper is interesting in that it describes an easily accessible formal way to model a certain class of real-time systems, and suggests how this class can be extended to other processing models. Its goal falls within the theme of increasing software productivity. However no really new theoretical concepts are introduced, and the analysis demonstrated here would also be possible with non-formal tools that are available. 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: 3-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: Mainly the availability of tool support to explore timing properties of a formal model. Note that tool support to do similar exploration of a non-formal model is already available and can offer more powerful exploration than the current paper (see below). However, in some application areas the use of a formal model may be prescribed and the paper describes a promising first step towards further analysis. 6. How WORTHWILE is the goal of the authors? Comment: The goal of being able to analyse timing properties early in the development process is very worthwile; this is a real problem. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: Well enough. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: For the most part. I've found two possible errors: - the definition of the predicate FromThread (pages 6-7); first of all in the text above "trace event" should probably be replaced by "trace element", and secondly I don't think this predicate would be able to distinguish between 2 different threads that both execute all the statements from the trace element (possibly in a different order). As far as I read the paper there is nothing to stop two different threads from executing the same statements? - the example interleaving on page 8 (table 1) does not correspond to the interleaving used in the rest of the text (and the figure) 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: There are a couple of missed opportunities in this paper. 1. Where this method would add value to existing non-formal timing exploration tools is that the duration expression seems to allow you to specify timing properties of implicitly specified operations. However this is not mentioned anywhere in the paper, which makes me wonder whether it is supported by the tool set at all. 2. How do you specify the timing requirements (e.g. those just before section 4.1) in terms of the timed events, and how do you extend the toolset to automatically check that the timing requirements are satisfied in a given run? Also, to at least partially remove the limits of dealing with a closed system (which has no random external inputs), how to generate a large number of runs with random external behaviour? I'm thinking here of what SPIN can do for non-timed specification; although I don't think that a SPIN-like full state space analysis (in order to generate proofs that the timing properties hold rather than just that they don't) to be possible for this timed case. 3. The set of timed events that can be analysed is rather limited (request for operation, start of operation, end of operation). It would be a very interesting extension to introduce timed events that capture when a specific proposition over all instance variables in the system becomes true or false (admittedly this becomes a bit hazy when you allow implicit specification). 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?: I cannot check these because I don't have access to a library. 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: None. +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++