PAPER NUMBER: 21
PAPER TITLE: A Framework for Modeling and Analysis of Rea-time System Operating System
AUTHORS: J. Kim and J. Choi

Score values              0 (reject), 1(weak reject), 2 (neutral), 3 (weak accept), and 4 (accept). 
--------(Review 1)----------------------------------------------------------------------------------------------------------
Appropriateness: 4
Originality: 3
Technical strength: 3
Presentation: 2
-------------------------------------------------------------------------------------------------------------------
Overall: 3

Comments to the authors: 
The paper contains many grammatical errors and typos. Only some are listed below. 
The authors should proofread the article carefully.

The title: `... Real-time System Operating System' --> `... Real-time Operating System'
Page 4, line -3: ` ... verification. [1] ...' `... verification [1]. ...'
Page 4, line -2: I-LOGOX --> I-LOGIX
page 7, line -1: `by model checking' --> `by model checking.'
pages 7 and 8, The texts in Figures 5 and 6 are not readable. 
page 8, line 7: `We simulateit ...' --> `We simulate it ...'
page 8, line -2: `we saw see ...'  ?
page 9, line 3: `in Fig. 7 ...' --> `In Fig. 7 ...'
page 9, line 17: `This methods ...' --> `This method ...'



Score values              0 (reject), 1(weak reject), 2 (neutral), 3 (weak accept), and 4 (accept). 
------------(Review 2)------------------------------------------------------------------------------------------------------
Appropriateness: 4
Originality: 2
Technical strength: 2
Presentation: 2
-------------------------------------------------------------------------------------------------------------------
Overall: 2

Comments to the authors: 


This work presents a framework for modeling and analyzing earlist
deadline first algorithm in Startcharts. From the content of the
paper, the authors seem to emphasize more on modeling than analysis. 
As the authors noted in section 2, there are not many works on
analysis of dynamic priority scheduling algorithms. Modeling earlist
deadline first algorithm may be an interesting topic itself. 
Additionally, how to exploit the abort mechanism in Startcharts to
model interrupt may be of interest. Unfortunately, the figures in the
paper (Figure 5 and 6) are obscure. I cannot see how the algorithm is
modeled from the authors' description. I would suggest the authors to
remove some of the introductory contents (such as statecharts for car
pedals or mutual exclusion) and enlarge the more interesting figures 5
and 6. I also would suggest the authors to present the anaylsis
results differently. I would rather see the trace of counterexample
found by the model checker than a window with a list of passed
properties. 

Here are the typos I found:

pp 4, paragraph 3: "Event is the event enabling...." It would be
better to use italics on "Event," similarly for "condition" and
"action."

pp 4, paragraph 4: "We can the check whether the system meets its ..."
"the" should be removed. In the same paragraph, "... variance of
variables are the important factor for verification." Should it be
"factors"?

pp 6, item 1: "In other words, there exits the minimum..." I think it
should be "exists"

pp 7, paragraph 2: "... that task isn't in the running state because
the task never any time." The sentence "the task never any time" does
not parse.

pp 8, paragraph 2: "We simulateit ..." Add a space.

pp8, paragraph 3: "In this verification, we saw see a ..." There is
one verb too many. 


Score values              0 (reject), 1(weak reject), 2 (neutral), 3 (weak accept), and 4 (accept).
 -----------(Review 3)-------------------------------------------------------------------------------------------------------
 Appropriateness: 4
 Originality: 2
 Technical strength: 2
 Presentation:  1
 -------------------------------------------------------------------------------------------------------------------
 Overall:  2

 Comments to the authors:

This paper presents a case study of using model-checker Statechart/mate to analyzing
programmable logic controller for a nuclear plant. The subject itself is interesting since
safety-critical appllications are a natural area for formal methods to show their strength.
However,  the presentation of this paper is far below the standard for publishable work:
1. There is at  least one grammar problem within every 5 lines,
2. There is no essential explanation on the system PLC and its design/modeling. Note that
     the PLC is the case-study performed by the authors in the paper and therefore, should be
     the key part of the paper. Because of this,  I have no way to understand the results
     presented in section 6
3. Not enough related work