Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

Elements in the intro 

- enlarging the scope to engineering
- addig recfs.
This commit is contained in:
Burkhart Wolff 2022-04-19 14:02:37 +02:00
parent 6e928f5af6
commit c9beb99b7a
3 changed files with 152 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

133
examples/scholarly_paper/2021-ITP-PMTI/document/root.bib
View File

@ -425,6 +425,139 @@ isbn="978-3-540-48509-4"
year = {2006}
}
@article{Security_Protocol_Refinement-AFP,
author = {Christoph Sprenger and Ivano Somaini},
title = {Developing Security Protocols by Refinement},
journal = {Archive of Formal Proofs},
month = may,
year = 2017,
note = {\url{http://isa-afp.org/entries/Security_Protocol_Refinement.html},
Formal proof development},
ISSN = {2150-914x},
}
@article{Splay_Tree-AFP,
author = {Tobias Nipkow},
title = {Splay Tree},
journal = {Archive of Formal Proofs},
month = aug,
year = 2014,
note = {\url{http://isa-afp.org/entries/Splay_Tree.html},
Formal proof development},
ISSN = {2150-914x},
}
@article{CakeML-AFP,
author = {Lars Hupel and Yu Zhang},
title = {CakeML},
journal = {Archive of Formal Proofs},
month = mar,
year = 2018,
note = {\url{http://isa-afp.org/entries/CakeML.html},
Formal proof development},
ISSN = {2150-914x},
}
@Article{ brucker.ea:featherweight:2014,
author = {Achim D. Brucker and Fr{\'e}d{\'e}ric Tuong and Burkhart Wolff},
title = {{Featherweight} {OCL}: A Proposal for a Machine-Checked Formal Semantics for {OCL} 2.5},
journal = {Archive of Formal Proofs},
month = jan,
year = 2014,
note = {\url{http://www.isa-afp.org/entries/Featherweight_OCL.shtml}, Formal proof development},
issn = {2150-914x},
public = {yes},
classification= {formal},
categories = {holocl},
pdf = {http://www.brucker.ch/bibliography/download/2014/brucker.ea-featherweight-2014.pdf},
filelabel = {Outline},
file = {http://www.brucker.ch/bibliography/download/2014/brucker.ea-featherweight-outline-2014.pdf},
areas = {formal methods, software},
url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-featherweight-2014}
}
@Article{ brucker.ea:afp-core-dom:2018,
author = {Achim D. Brucker and Michael Herzberg},
title = {The {Core} {DOM}},
journal = {Archive of Formal Proofs},
month = dec,
year = 2018,
date = {2018-12-26},
note = {\url{http://www.isa-afp.org/entries/Core_DOM.html}, Formal proof development},
issn = {2150-914x},
abstract = {In this AFP entry, we formalize the core of the Document Object Model (DOM). At its core, the DOM
defines a tree-like data structure for representing documents in general and HTML documents in
particular. It is the heart of any modern web browser. Formalizing the key concepts of the DOM is a
prerequisite for the formal reasoning over client-side JavaScript programs and for the analysis of
security concepts in modern web browsers. We present a formalization of the core DOM, with focus on
the node-tree and the operations defined on node-trees, in Isabelle/HOL. We use the formalization to
verify the functional correctness of the most important functions defined in the DOM standard.
Moreover, our formalization is 1) extensible, i.e., can be extended without the need of re-proving
already proven properties and 2) executable, i.e., we can generate executable code from our
specification.},
public = {yes},
classification= {formal},
categories = {websecurity},
pdf = {http://www.brucker.ch/bibliography/download/2018/brucker.ea-afp-core-dom-2018.pdf},
filelabel = {Outline},
file = {http://www.brucker.ch/bibliography/download/2018/brucker.ea-afp-core-dom-outline-2018.pdf},
areas = {formal methods, security, software engineering},
url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-afp-core-dom-2018}
}
@article{SPARCv8-AFP,
author = {Zhe Hou and David Sanan and Alwen Tiu and Yang Liu},
title = {A formal model for the SPARCv8 ISA and a proof of non-interference for the LEON3 processor},
journal = {Archive of Formal Proofs},
month = oct,
year = 2016,
note = {\url{http://isa-afp.org/entries/SPARCv8.html},
Formal proof development},
ISSN = {2150-914x},
}
@Article{ verbeek.ea:formal:2014,
author = {Freek Verbeek and Sergey Tverdyshev and Oto Havle and
Holger Blasum and Bruno Langenstein and Werner Stephan and
Yakoub Nemouchi and Abderrahmane Feliachi and Burkhart
Wolff and Julien Schmaltz},
title = {Formal Specification of a Generic Separation Kernel},
journal = {Archive of Formal Proofs},
month = jul,
year = 2014,
note = {\url{http://isa-afp.org/entries/CISC-Kernel.html}, Formal
proof development},
issn = {2150-914x}
}
@Article{ brucker.ea:upf-firewall:2017,
author = {Achim D. Brucker and Lukas Br{\"u}gger and Burkhart Wolff},
title = {Formal Network Models and Their Application to Firewall Policies},
journal = {Archive of Formal Proofs},
month = jan,
year = 2017,
date = {2017-01-08},
note = {\url{http://www.isa-afp.org/entries/UPF_Firewall.shtml}, Formal proof development},
issn = {2150-914x},
public = {yes},
classification= {formal},
categories = {holtestgen},
pdf = {http://www.brucker.ch/bibliography/download/2017/brucker.ea-upf-firewall-2017.pdf},
filelabel = {Outline},
file = {http://www.brucker.ch/bibliography/download/2017/brucker.ea-upf-firewall-outline-2017.pdf},
areas = {formal methods, security},
url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-upf-firewall-2017}
}
@Article{ klein.ea:comprehensive:2014,
author = {Gerwin Klein and June Andronick and Kevin Elphinstone and
Toby C. Murray and Thomas Sewell and Rafal Kolanski and
Gernot Heiser},
title = {Comprehensive formal verification of an {OS} microkernel},
journal = {{ACM} Trans. Comput. Syst.},
year = 2014,
volume = 32,
number = 1,
pages = {2:1--2:70},
doi = {10.1145/2560537}
}
@InProceedings{10.1007/978-3-540-76298-0_52,
author="Auer, S{\"o}ren
and Bizer, Christian

21
examples/scholarly_paper/2021-ITP-PMTI/paper.thy
View File

@ -117,14 +117,25 @@ text*[abs::abstract,
\<close>
section*[introheader::introduction]
\<open> Introduction \<close>
section*[introheader::introduction] \<open> Introduction \<close>
text*[introtext::introduction]\<open>
The linking of \<^emph>\<open>formal\<close> and \<^emph>\<open>informal\<close> information is perhaps the most pervasive challenge
in the digitization of knowledge and its propagation. Unsurprisingly, this problem reappears
in the libraries with formalized mathematics and engineering such as the Isabelle Archive of
Formal Proofs @{cite "AFP-ref22"}, which passed the impressive numbers of 650 articles,
written by 420 authors at the beginning of 2022. Still, while the problem of logical consistency
written by 420 authors at the beginning of 2022. Together with the AFP, there is also a growing
body on articles concerned with formal software engineering such as standardized language
definitions (e.g., @{cite "CakeML-AFP" and "brucker.ea:featherweight:2014"}),
data-structures
(e.g., @{cite "brucker.ea:afp-core-dom:2018" and "Splay_Tree-AFP"}), hardware- models
(e.g., @{cite "SPARCv8-AFP"}),
security-related specifications
(e.g., @{cite "brucker.ea:upf-firewall:2017" and "Security_Protocol_Refinement-AFP"}),
or operating systems (e. g., @{cite "verbeek.ea:formal:2014" and "klein.ea:comprehensive:2014"}).
Still, while the problem of logical consistency
even under system-changes and pervasive theory evolution is technically solved via continuous
proof-checking, the problem of knowledge retrieval and of linking semi-formal explanations to
definitions and proofs remains largely open.
@ -1235,7 +1246,7 @@ where the constants \<open>iswff\<^sub>p\<^sub>r\<^sub>e\<close> is bound to a f
is executed during the evaluation phase of these invariants and that checks:
\<^item> Any \<open>cond\<close> is indeed a valid definition in the global logical context
(taking HOL-libraries but also the concrete certification target model into account).
\<^item> Any such definition has the syntactic form:
\<^item> Any such HOL definition has the syntactic form:
\<^vs>\<open>-0.3cm\<close>
@{cartouche [display,indent=10,margin=70] \<open>pre_<op_name> (a\<^sub>1::\<tau>\<^sub>1) ... (a\<^sub>n::\<tau>\<^sub>n) \<equiv> <predicate>,\<close>}
\<^vs>\<open>-0.3cm\<close>
@ -1243,7 +1254,7 @@ is executed during the evaluation phase of these invariants and that checks:
\<^item> The case for the post-condition is treated analogously. \<close>
text\<open>Note that this technique can also be applied to impose specific syntactic constraints on
HOL types. For example, via the SI-package available in the Isabelle AFP
types. For example, via the SI-package available in the Isabelle AFP
\<^footnote>\<open>\<^url>\<open>https://www.isa-afp.org/entries/Physical_Quantities.html\<close>\<close>, it is possible to express
that the result of some calculation is of type
\<open>32 unsigned [m\<^sup>\<cdot>s\<^sup>-\<^sup>2]\<close>, so a 32-bit natural representing an acceleration in the SI-system.

6
src/ontologies/CENELEC_50128/CENELEC_50128.thy
View File

@ -580,9 +580,9 @@ doc_class SWIS_E =
doc_class SWIS = cenelec_document +
phase :: "phase" <= "SCDES"
written_by :: "role" <= "DES"
fst_check :: "role" <= "VER"
snd_check :: "role" <= "VAL"
written_by :: "role" <= "DES"
fst_check :: "role" <= "VER"
snd_check :: "role" <= "VAL"
components :: "SWIS_E list"
type_synonym software_interface_specification = SWIS