PAPER NUMBER: 17 PAPER TITLE: Regular Expressions for Run-Time Verification Languages AUTHORS: Sammapun and Sokolsky Score values 0 (reject), 1(weak reject), 2 (neutral), 3 (weak accept), and 4 (accept). ----------(Review 1)-------------------------------------------------------------------------------------------------------- Appropriateness: 4 Originality: 1 Technical strength: 2 Presentation: 3 ------------------------------------------------------------------------------------------------------------------- Overall: 2 Comments to the authors: The paper presents a suggested extension of their specification language in the MaC system. This language is based on a temporal logic for safety properties. The paper presents an extension with regular expressions. The rationale is to specify certain complex event patterns in a more convenient way. My impression is that the extension has not been implemented nor evaluated empirically. The extension is motivated by some examples. The semantics of the regular expressions is motivated and defined in a quite readable way. I think that the contribution is interesting. However, I also think that it is still preliminary work, and that the authors should consider and discuss some possible objections to their approach, including: - The chosen semantics is based on some design decisions, which seem not to be so evident. This makes the semantics different from the use of Regular Expressions in other languages (UNIX regexp, ForSpec, ...). The authors should motivate the differences to these languages. - The semantics of Regular Expressions is quite "non-declarative", using a quite "procedural" interpretation of the REgular Expressions. One must in fact think of them as finite automata. Then, why not directly use finite automata. The examples in the paper are all simple. The authors should check that the semantics for complex examples matches some intuition. Score values 0 (reject), 1(weak reject), 2 (neutral), 3 (weak accept), and 4 (accept). --------(Review 2)---------------------------------------------------------------------------------------------------------- Appropriateness: 4 Originality: 2 Technical strength: 3 Presentation: 3 ------------------------------------------------------------------------------------------------------------------- Overall: 3 Comments to the authors: The authors propose an extension to their previous work MEDL (meta event definition language) for analyzing real-time systems by adding regular expressions over events to allow succinct specifications for design requirements. The paper is an ongoing piece of work and no implementation is presented at the current time. Researchers in experimental formal methods may find the paper somewhat interesting, since it addresses the issue of introducing appropriate mechanisms into an existing specification language to make the language expressive and less error-prone (to users). However, the originality of the regular expression idea in this paper is weak -- people in model-checking have already known the idea and are well studied for decades. One other comment is why the authors do not choose timed automata as the underlying solver since you have timing requirements in MEDL (see section 5). More comments: p5 line 3: such --> such as p5 line -15: RE wxyz =; should be: RE wxyz = ? Maybe I am wrong. p6 line -12: kleene --> Kleene p7 line 3: what is your time domain? discrete or dense? p8 line 3 and line 4: your L(\epsilon) and L(a) do not return a set ! p8 lines 7,8,9: you need explainations in English p9 line 1 of section 5: a automaton --> an automaton Score values 0 (reject), 1(weak reject), 2 (neutral), 3 (weak accept), and 4 (accept). --------(Review 3)---------------------------------------------------------------------------------------------------------- Appropriateness: 4 Originality: 4 Technical strength: 3 Presentation: 4 ------------------------------------------------------------------------------------------------------------------- Overall: 4 Comments to the authors: