-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathUsingtheEventBmodellinglanguageforteachingverificationtechniques.html
38 lines (36 loc) · 3.37 KB
/
UsingtheEventBmodellinglanguageforteachingverificationtechniques.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
<!DOCTYPE html>
<html lang='en-US' xml:lang='en-US'>
<head><title>Using the Event-B modelling language for teaching verification techniques
</title>
<meta charset='utf-8' />
<meta content='TeX4ht (https://tug.org/tex4ht/)' name='generator' />
<meta content='width=device-width,initial-scale=1' name='viewport' />
<link href='web.css' rel='stylesheet' type='text/css' />
<meta content='web.tex' name='src' />
</head><body>
<!-- l. 143 --><div class='crosslinks'><p class='noindent'>[<a href='CourseDISCONTModellingModellingSystems.html'>next</a>] [<a href='CourseMVSIforfrenchstudentsinfrench.html'>prev</a>] [<a href='CourseMVSIforfrenchstudentsinfrench.html#tailCourseMVSIforfrenchstudentsinfrench.html'>prev-tail</a>] [<a href='#tailUsingtheEventBmodellinglanguageforteachingverificationtechniques.html'>tail</a>] [<a href='web.html#UsingtheEventBmodellinglanguageforteachingverificationtechniques.html'>up</a>] </p></div>
<h3 class='sectionHead' id='using-the-eventb-modelling-language-for-teaching-verification-techniques-'><span class='titlemark'>5 </span> <a id='x6-50005'></a>Using the Event-B modelling language for teaching verification techniques
</h3>
<!-- l. 145 --><p class='noindent'>Verification of program properties such as partial correctness (PC) or absence of errors at
runtime (RTE) applies induction principles using algorithmic techniques for checking
statements in a logical framework such as classical logic or temporal logic. Alan Turing
was undoubtedly the first to annotate programs, namely Turing machines, and to apply
an induction principle to transition systems. Our work is placed in this perspective of
verifying safety properties of sequential or distributed programs, with the aim of
presenting them as simply as possible to student classes in the context of a posteriori
verification. We report on an in vivo experiment using the Event-B language
and associated tools as an assembly and disassembly platform for correcting
programs in a programming language. We revisit the properties of partial correctness
and the absence of run-time errors in the context of this experiment, which
precedes the use of Event-B as a method of correct design by construction. We have
adopted a contract-based approach to programming, which we are implementing
with Event-B. A few examples are given to illustrate this pedagogical approach.
This step is part of a process of learning both the underlying techniques and
other tools such as Frama-c, Dafny and Why3 …, which are based on the same
ideas.
</p><!-- l. 160 --><p class='indent'>Please visit the link <a href='https://mery54.github.io/fmt'>FMT</a>.
</p>
<!-- l. 164 --><div class='crosslinks'><p class='noindent'>[<a href='CourseDISCONTModellingModellingSystems.html'>next</a>] [<a href='CourseMVSIforfrenchstudentsinfrench.html'>prev</a>] [<a href='CourseMVSIforfrenchstudentsinfrench.html#tailCourseMVSIforfrenchstudentsinfrench.html'>prev-tail</a>] [<a href='UsingtheEventBmodellinglanguageforteachingverificationtechniques.html'>front</a>] [<a href='web.html#UsingtheEventBmodellinglanguageforteachingverificationtechniques.html'>up</a>] </p></div>
<!-- l. 164 --><p class='indent'><a id='tailUsingtheEventBmodellinglanguageforteachingverificationtechniques.html'></a></p>
</body>
</html>