Academic Journal
Author manuscript, published in 'Rodin User and Developer Workshop (2009)' A Rodin plugin for quantitative timed models ∗
| العنوان: | Author manuscript, published in 'Rodin User and Developer Workshop (2009)' A Rodin plugin for quantitative timed models ∗ |
|---|---|
| المؤلفون: | Joris Rehm, Loria Nancy Université |
| المساهمون: | The Pennsylvania State University CiteSeerX Archives |
| المصدر: | http://hal.inria.fr/docs/00/43/12/46/PDF/time_plugin.pdf. |
| سنة النشر: | 2009 |
| المجموعة: | CiteSeerX |
| الوصف: | We propose to develop a Rodin1 plug-in that experiments a systematic use of a refinement pattern. The goal of this pattern is to help in modeling of timed system in Event-B. By timed system we mean system with quantitative temporal constraints and properties. The user (of the plug-in) will see and modify an Event-B machine augmented with a new operator S. This unary operator over an event name e gives the delay elapsed since the latest triggering of the event e. By using this operator in the invariant, the user will be able to write and prove temporal properties over the events. By using this operator in the guard of an event f, the user will be able to specify temporal constraints over the duration S(e) (which becomes here the delay between the event e and f). For the possible constraints, we plan to consider lower time bounds (l ≤ S(e) in guard of f) and upper time bound (S(e) ≤ u in guard of f). The upper time bound is a bound within the event f must obligatory occurs, it is not just a possibility. In this text, the usages of the operator S is called the annotations, it is an extension of the syntaxe of the B models. The annotations can only appear in invariant or guards. Our pattern is an Event-B model that encodes the behaviour of the operator S (we call this model the pattern model). The annotations given by the user define how to refine the pattern model and how to obtain the behaviour of S needed for a particular augmented model. The goal of our plug-in is to generate a normal Event-B model that is the studied (augmented) model where the annotations are replaced with the superposition of the refined pattern model. To explain briefly what is the idea of the pattern, we show below an augmented model (on the left) and the generated result (on the right). This small model define a light that can be on (lo = TRUE) or off (lo = FALSE); the light can be switch on by a button (the event on) and goes automaticaly off (event off) after a delay between c − d and c + d. You can see the temporal annotations in the ... |
| نوع الوثيقة: | text |
| وصف الملف: | application/pdf |
| اللغة: | English |
| Relation: | http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.230.2129; http://hal.inria.fr/docs/00/43/12/46/PDF/time_plugin.pdf |
| الاتاحة: | http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.230.2129 http://hal.inria.fr/docs/00/43/12/46/PDF/time_plugin.pdf |
| Rights: | Metadata may be used without restrictions as long as the oai identifier remains attached to it. |
| رقم الانضمام: | edsbas.3CA88D9C |
| قاعدة البيانات: | BASE |
| الوصف غير متاح. |