Коллеги,
Поздравляю всех с принятием нашей статьи на VES-2013. Все отзывы
оказались внезапно позитивными.
Надо до 3 июня отправить поправленную версию, я думаю, что завтра я
исправлю мелкие замечания, упомянутые в рецензиях и пришлю всем
исправленный вариант.
Также в письме сказано, что один из авторов должен зарегистрироваться:
http://cav2013.forsyte.at/registration/
Как я понял, нас интересуют One-day workshops. Ранняя регистрация
заканчивается довольно скоро, 21 мая.
Также нам надо до 27 мая подготовить статью на Eucass, это уже скоро,
так что я в выходные постараюсь набросать статью, отформатированную по
нужному шаблону, на основе статьи на WinterSim.
Даниил
-------- Исходное сообщение --------
Тема: VES-2013 notification for paper 5
Дата: Fri, 17 May 2013 13:25:11 +0200
От: VES-2013 <ves2013(a)easychair.org>
Кому: Daniil Zorin <juan(a)lvk.cs.msu.su>
Dear Daniil,
We are glad to inform you that your paper
An experience on using simulation environment DYANA augmented with UPPAAL for verification of embedded systems defined by UML statecharts
was accepted for VES 2013.
Please note the following important information:
* The workshop proceedings will be distributed with CAV proceedings on USB sticks. The final version is due on May 31, 2013. Please take into account the comments and suggestions by the reviewers in the final version.
The final version should be in the pdf format.
* At least one author of each accepted paper must register and present the paper at the conference.
We are looking forward to seeing you in St. Petersburg!
VES 2013 organizers.
----------------------- REVIEW 1 ---------------------
PAPER: 5
TITLE: An experience on using simulation environment DYANA augmented with UPPAAL for verification of embedded systems defined by UML statecharts
AUTHORS: Daniil Zorin, Vladislav Podymov, Dmitry Volkanov, Vladimir Zakharov, Alevtina Glonina and Igor Konnov
OVERALL EVALUATION: 3 (strong accept)
----------- REVIEW -----------
The paper presents a tool for verification of real-time embedded systems. Authors integrated their simulation tool DYANA with UPPAAL. Also they used DYANA to measure execution time of scheduled tasks. Developed tool used to verify an onboard car controller and an onboard flight controller.
The research will be interesting for majority of VES participants.
There are some minor remarks that should be considered before publication:
1) The counterexample (p.6) found by the verifier as violation of the liveness property seems to be a Zenon execution. It’s unclear why it can’t be excluded by a fairness condition.
2) The description of the onboard flight controller is overloaded by details. It becomes impossible to reconstruct the idea of system behavior without all statecharts. Might be a one controller scenario will give much more understanding of the system.
3) Requirements (p.11) have not common syntax and unclear semantics, e.g. concerning the formula A[]!cr2 || !cr3 usually [] has higher priority than ||. Other formulae are stated as liveness properties but they do not contain temporal operators explicitly.
4) Abbreviation RTES is not explained.
5) There are no WCETs for any examples.
----------------------- REVIEW 2 ---------------------
PAPER: 5
TITLE: An experience on using simulation environment DYANA augmented with UPPAAL for verification of embedded systems defined by UML statecharts
AUTHORS: Daniil Zorin, Vladislav Podymov, Dmitry Volkanov, Vladimir Zakharov, Alevtina Glonina and Igor Konnov
OVERALL EVALUATION: 2 (accept)
----------- REVIEW -----------
The paper presents DYANA analyser which was originally intended for simulation of distributed real-time systems.
Then DYANA was extended for the verification on the early stages of development and the paper describes the architecture of the approach and briefly describes its components.
The paper gives several case studies. The first one is onboard car controller.
I guessed that the described intersection in section 3.1 is a circular motion.
If so, I didn't understand how a car can move to the left and what is the meaning of the rule:
"If a car is moving to the left, then it should give way to cars moving from the opposite lane to the left or straight ahead"
The second one is onboard flight controller. For this case study I didn't understand whether the violations found?
The paper is well written and should be accepted.
Errata
page 3. par. 3.
Metamoc working -> Metamoc is working
page 3. par. 3. missing dot at the end
verification tool [8] -> verification tool [8].
page 4. par. 4
until some a transition -> until some transition
----------------------- REVIEW 3 ---------------------
PAPER: 5
TITLE: An experience on using simulation environment DYANA augmented with UPPAAL for verification of embedded systems defined by UML statecharts
AUTHORS: Daniil Zorin, Vladislav Podymov, Dmitry Volkanov, Vladimir Zakharov, Alevtina Glonina and Igor Konnov
OVERALL EVALUATION: 2 (accept)
----------- REVIEW -----------
The paper is an experience report on verification of some embedded systems by the tools developed by the authors with the use of some open-source tools.
The paper is very well written. English is good. I enjoyed reading the paper, especially because I'm not an expert in this area and it was kind of a tutorial for me. Such quality is quite enough for accepting for a workshop.
The paper clearly states what is the contribution of the authors. Figure 1 shows the structure of the system with colors denoting reusing of open source tools, modified by authors and newly developed ones.
Two large examples of verified systems are presented in rather detail. Although I didn't follow all of the details, I enjoyed the overall impression of the case study.
The bibliography and discussion of related work looks fairly complete, although I can't judge for sure, being not an expert in this area.
Unfortunately the paper lacks discussion of computer resources used for verification of this samples. I recommend authors to add such data in the final version.
MINOR NOTES
Page 1: "In this project for the first time a Model Driven Approach has been studied and implemented." - It is not clear: "for the first time" by authors with this system or in the history?
Page 3: "Metamoc working in cooperation with UPPAAL verification tool" - replace "working" -> "works" and add period at the end.
Page 3: "If a NTA" -> "If an NTA"
Page 4: "time does not passes until" -> "time does not pass until"
Page 5: "at the crossing simultaneously is assumed." - "is assumed" is extra
Page 6: "a car appears at the crossing, and then it continuously slows down, but doesn't stop. With such strategy it will never pass the crossing." - I don't understand the conclusion. (However, this is unimportant. Just for curiosity.)
Page 13: "Creation object le using cross-compiliator" -> "...cross-compiler"
Page 14. Reference [7]: "imulation" -> "Simulation"
