-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathdoc.html
222 lines (184 loc) · 10.8 KB
/
doc.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
<!DOCTYPE html><html lang="en">
<head>
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
<title>Modelling Software-based Systems</title>
<!--Generated on Wed Sep 18 15:35:19 2024 by LaTeXML (version 0.8.8) http://dlmf.nist.gov/LaTeXML/.-->
<!--Document created on September 18, 2024.-->
<link rel="stylesheet" href="LaTeXML.css" type="text/css">
<link rel="stylesheet" href="ltx-article.css" type="text/css">
<link rel="stylesheet" href="ltx-listings.css" type="text/css">
<link rel="stylesheet" href="ltx-ulem.css" type="text/css">
<meta name="viewport" content="width=device-width, initial-scale=1, shrink-to-fit=no">
</head>
<body>
<div class="ltx_page_main">
<div class="ltx_page_content">
<article class="ltx_document ltx_authors_1line">
<div id="p1" class="ltx_para">
<span class="ltx_ERROR undefined">\includeversion</span>
<p class="ltx_p"><span class="ltx_text" style="background-color:#00FFFF;">check
<span class="ltx_ERROR undefined">\excludeversion</span>comm
</span></p>
</div>
<h1 class="ltx_title ltx_title_document" style="background-color:#00FFFF;">Modelling Software-based Systems</h1>
<div class="ltx_authors">
<span class="ltx_creator ltx_role_author">
<span class="ltx_personname"><span class="ltx_text" style="background-color:#00FFFF;">Dominique Méry</span>
<br class="ltx_break"><span class="ltx_text" style="background-color:#00FFFF;">LORIA & Telecom Nancy</span>
<br class="ltx_break"><span class="ltx_text" style="background-color:#00FFFF;">Université de Lorraine</span>
<br class="ltx_break"><span class="ltx_ref ltx_nolink ltx_url ltx_font_typewriter ltx_ref_self" style="background-color:#00FFFF;">[email protected]</span>
</span></span>
</div>
<div class="ltx_dates">(<span class="ltx_text" style="background-color:#00FFFF;">September 18, 2024</span>)</div>
<div class="ltx_abstract">
<h6 class="ltx_title ltx_title_abstract">Abstract</h6>
<p class="ltx_p" style="background-color:#00FFFF;">The Event-B method is based on a modelling
language used to describe state-based models and safety
properties of those state-based models. The originality of Event-B
lies in its ability to
enable incremental and proof-based modelling of <span class="ltx_text ltx_font_italic">reactive
systems</span>. The Event-B language contains both set notations and a
first-order predicate calculus; it offers the possibility of defining
models of reactive systems called machines and contexts and includes
the refinement relationship that allows us to follow an incremental
development methodology.</p>
</div>
<div id="p2" class="ltx_para">
<p class="ltx_p"><span class="ltx_text" style="background-color:#00FFFF;">This site contains resources relating to the use of the Event-B
language and the Rodin platform to verify contracts for a small
sequential programming language. We give the Rodin models and a
description of these models in the form of a text <span class="ltx_text ltx_LaTeX_logo" style="letter-spacing:-0.2em; margin-right:0.1em;">L<span class="ltx_text" style="position:relative; bottom:0.4ex;font-variant:small-caps;;">a</span>T<span class="ltx_text" style="position:relative; bottom:-0.2ex;font-variant:small-caps;font-size:120%;">e</span>X</span>.</span></p>
</div>
<section id="S1" class="ltx_section" style="background-color:#00FFFF;">
<h2 class="ltx_title ltx_title_section">
<span class="ltx_tag ltx_tag_section">1 </span>Documentation</h2>
<div id="S1.p1" class="ltx_para">
<ul id="S1.I1" class="ltx_itemize">
<li id="S1.I1.i1" class="ltx_item" style="list-style-type:none;">
<span class="ltx_tag ltx_tag_item">•</span>
<div id="S1.I1.i1.p1" class="ltx_para">
<p class="ltx_p"><cite class="ltx_cite ltx_citemacro_cite">[<a href="#bib.bib1" title="The event-b modelling method: concepts and case studies" class="ltx_ref">2</a>]</cite></p>
</div>
</li>
</ul>
</div>
</section>
<section id="S2" class="ltx_section" style="background-color:#00FFFF;">
<h2 class="ltx_title ltx_title_section">
<span class="ltx_tag ltx_tag_section">2 </span>Course MCFSI at Telecom Nancy</h2>
<div id="S2.p1" class="ltx_para">
<ul id="S2.I1" class="ltx_itemize">
<li id="S2.I1.i1" class="ltx_item" style="list-style-type:none;">
<span class="ltx_tag ltx_tag_item">•</span>
<div id="S2.I1.i1.p1" class="ltx_para">
<p class="ltx_p">Lectures Notes <span class="ltx_text ltx_font_italic">The Modelling Language</span> at the
<a href="http://mery54.github.io/teaching/mosos/lecturesnotes/main-Poly1.pdf" title="" class="ltx_ref ltx_href">following
link</a>.</p>
</div>
</li>
<li id="S2.I1.i2" class="ltx_item" style="list-style-type:none;">
<span class="ltx_tag ltx_tag_item">•</span>
<div id="S2.I1.i2.p1" class="ltx_para">
<p class="ltx_p">Slides of the course</p>
<ul id="S2.I1.i2.I1" class="ltx_itemize">
<li id="S2.I1.i2.I1.i1" class="ltx_item" style="list-style-type:none;">
<span class="ltx_tag ltx_tag_item"><span class="ltx_text ltx_font_bold">–</span></span>
<div id="S2.I1.i2.I1.i1.p1" class="ltx_para">
<p class="ltx_p">Lecture 1
<a href="http://mery54.github.io/teaching/mosos/lecturesnotes/mcfsi-lect1.pdf" title="" class="ltx_ref ltx_href">The
Modelling Language Event-B</a>.</p>
</div>
</li>
<li id="S2.I1.i2.I1.i2" class="ltx_item" style="list-style-type:none;">
<span class="ltx_tag ltx_tag_item"><span class="ltx_text ltx_font_bold">–</span></span>
<div id="S2.I1.i2.I1.i2.p1" class="ltx_para">
<p class="ltx_p">Lecture 2
<a href="http://mery54.github.io/teaching/mosos/lecturesnotes/mcfsi-po.pdf" title="" class="ltx_ref ltx_href">Proof
Obligations</a>.</p>
</div>
</li>
<li id="S2.I1.i2.I1.i3" class="ltx_item" style="list-style-type:none;">
<span class="ltx_tag ltx_tag_item"><span class="ltx_text ltx_font_bold">–</span></span>
<div id="S2.I1.i2.I1.i3.p1" class="ltx_para">
<p class="ltx_p">Lecture 3
<a href="http://mery54.github.io/teaching/mosos/lecturesnotes/mcfsi-lect2.pdf" title="" class="ltx_ref ltx_href">Correctness by Construction with the
Modelling Language Event-B using the Refinement</a>.</p>
</div>
</li>
<li id="S2.I1.i2.I1.i4" class="ltx_item" style="list-style-type:none;">
<span class="ltx_tag ltx_tag_item"><span class="ltx_text ltx_font_bold">–</span></span>
<div id="S2.I1.i2.I1.i4.p1" class="ltx_para">
<p class="ltx_p">Lecture 4
<a href="http://mery54.github.io/teaching/mosos/lecturesnotes/mcfsi-lect3.pdf" title="" class="ltx_ref ltx_href">Access
Control </a></p>
</div>
</li>
</ul>
</div>
</li>
<li id="S2.I1.i3" class="ltx_item" style="list-style-type:none;">
<span class="ltx_tag ltx_tag_item">•</span>
<div id="S2.I1.i3.p1" class="ltx_para">
<p class="ltx_p">Tutorials</p>
<ul id="S2.I1.i3.I1" class="ltx_itemize">
<li id="S2.I1.i3.I1.i1" class="ltx_item" style="list-style-type:none;">
<span class="ltx_tag ltx_tag_item"><span class="ltx_text ltx_font_bold">–</span></span>
<div id="S2.I1.i3.I1.i1.p1" class="ltx_para">
<p class="ltx_p">Tutorial 1
<a href="http://mery54.github.io/teaching/mosos/lecturesnotes/tutorial1.pdf" title="" class="ltx_ref ltx_href">Using
the Event-B modelling language</a>.</p>
</div>
</li>
</ul>
</div>
</li>
<li id="S2.I1.i4" class="ltx_item" style="list-style-type:none;">
<span class="ltx_tag ltx_tag_item">•</span>
<div id="S2.I1.i4.p1" class="ltx_para">
<p class="ltx_p">The Event-B models are at the <a href="http://mery54.github.io/teaching/models/" title="" class="ltx_ref ltx_href">link for <span class="ltx_text ltx_font_sansserif">Event-B</span> </a>.</p>
</div>
</li>
</ul>
</div>
</section>
<section id="S3" class="ltx_section" style="background-color:#00FFFF;">
<h2 class="ltx_title ltx_title_section">
<span class="ltx_tag ltx_tag_section">3 </span>Course Modelling and verifying software-based systems</h2>
</section>
<section id="bib" class="ltx_bibliography" style="background-color:#00FFFF;">
<h2 class="ltx_title ltx_title_bibliography">References</h2>
<ul id="bib.L1" class="ltx_biblist">
<li id="bib.bib5" class="ltx_bibitem ltx_bib_book">
<span class="ltx_tag ltx_bib_key ltx_role_refnum ltx_tag_bibitem">[1]</span>
<span class="ltx_bibblock"><span class="ltx_text ltx_bib_editor">D. Bjørner and M. C. Henson (Eds.)</span><span class="ltx_text ltx_bib_year"> (2007)</span>
</span>
<span class="ltx_bibblock"><span class="ltx_text ltx_bib_title">Logics of specification languages</span>.
</span>
<span class="ltx_bibblock"><span class="ltx_text ltx_bib_series">EATCS Textbook in Computer Science</span>, <span class="ltx_text ltx_bib_publisher">Springer</span>.
</span>
<span class="ltx_bibblock ltx_bib_cited">Cited by: <a href="#bib.bib1" title="The event-b modelling method: concepts and case studies" class="ltx_ref">2</a>.
</span>
</li>
<li id="bib.bib1" class="ltx_bibitem ltx_bib_inbook">
<span class="ltx_tag ltx_bib_key ltx_role_refnum ltx_tag_bibitem">[2]</span>
<span class="ltx_bibblock"><span class="ltx_text ltx_bib_author">D. Cansell and D. Méry</span><span class="ltx_text ltx_bib_year"> (2007)</span>
</span>
<span class="ltx_bibblock"><span class="ltx_text ltx_bib_title">The event-b modelling method: concepts and case studies</span>.
</span>
<span class="ltx_bibblock"><span class="ltx_text ltx_bib_pages"> pp. 33–140</span>.
</span>
<span class="ltx_bibblock">Note: <span class="ltx_text ltx_bib_note">See <cite class="ltx_cite ltx_citemacro_cite">[<a href="#bib.bib5" title="Logics of specification languages" class="ltx_ref">1</a>]</cite>.</span>
</span>
<span class="ltx_bibblock ltx_bib_cited">Cited by: <a href="#S1.I1.i1.p1" title="In 1 Documentation ‣ Modelling Software-based Systems" class="ltx_ref"><span class="ltx_text ltx_ref_tag">1st item</span></a>.
</span>
</li>
</ul>
</section>
</article>
</div>
<footer class="ltx_page_footer">
<div class="ltx_page_logo">Generated on Wed Sep 18 15:35:19 2024 by <a href="http://dlmf.nist.gov/LaTeXML/" class="ltx_LaTeXML_logo"><span style="letter-spacing:-0.2em; margin-right:0.1em;">L<span class="ltx_font_smallcaps" style="position:relative; bottom:2.2pt;">a</span>T<span class="ltx_font_smallcaps" style="font-size:120%;position:relative; bottom:-0.2ex;">e</span></span><span style="font-size:90%; position:relative; bottom:-0.2ex;">XML</span><img src="data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAAAsAAAAOCAYAAAD5YeaVAAAAAXNSR0IArs4c6QAAAAZiS0dEAP8A/wD/oL2nkwAAAAlwSFlzAAALEwAACxMBAJqcGAAAAAd0SU1FB9wKExQZLWTEaOUAAAAddEVYdENvbW1lbnQAQ3JlYXRlZCB3aXRoIFRoZSBHSU1Q72QlbgAAAdpJREFUKM9tkL+L2nAARz9fPZNCKFapUn8kyI0e4iRHSR1Kb8ng0lJw6FYHFwv2LwhOpcWxTjeUunYqOmqd6hEoRDhtDWdA8ApRYsSUCDHNt5ul13vz4w0vWCgUnnEc975arX6ORqN3VqtVZbfbTQC4uEHANM3jSqXymFI6yWazP2KxWAXAL9zCUa1Wy2tXVxheKA9YNoR8Pt+aTqe4FVVVvz05O6MBhqUIBGk8Hn8HAOVy+T+XLJfLS4ZhTiRJgqIoVBRFIoric47jPnmeB1mW/9rr9ZpSSn3Lsmir1fJZlqWlUonKsvwWwD8ymc/nXwVBeLjf7xEKhdBut9Hr9WgmkyGEkJwsy5eHG5vN5g0AKIoCAEgkEkin0wQAfN9/cXPdheu6P33fBwB4ngcAcByHJpPJl+fn54mD3Gg0NrquXxeLRQAAwzAYj8cwTZPwPH9/sVg8PXweDAauqqr2cDjEer1GJBLBZDJBs9mE4zjwfZ85lAGg2+06hmGgXq+j3+/DsixYlgVN03a9Xu8jgCNCyIegIAgx13Vfd7vdu+FweG8YRkjXdWy329+dTgeSJD3ieZ7RNO0VAXAPwDEAO5VKndi2fWrb9jWl9Esul6PZbDY9Go1OZ7PZ9z/lyuD3OozU2wAAAABJRU5ErkJggg==" alt="Mascot Sammy"></a>
</div></footer>
</div>
</body>
</html>