From c9beb99b7a3c06b9b4ef204a0e5864470ac15d2d Mon Sep 17 00:00:00 2001 From: Burkhart Wolff Date: Tue, 19 Apr 2022 14:02:37 +0200 Subject: [PATCH] Elements in the intro - enlarging the scope to engineering - addig recfs. --- .../2021-ITP-PMTI/document/root.bib | 133 ++++++++++++++++++ .../scholarly_paper/2021-ITP-PMTI/paper.thy | 21 ++- .../CENELEC_50128/CENELEC_50128.thy | 6 +- 3 files changed, 152 insertions(+), 8 deletions(-) diff --git a/examples/scholarly_paper/2021-ITP-PMTI/document/root.bib b/examples/scholarly_paper/2021-ITP-PMTI/document/root.bib index a3c981a..d02e1c7 100644 --- a/examples/scholarly_paper/2021-ITP-PMTI/document/root.bib +++ b/examples/scholarly_paper/2021-ITP-PMTI/document/root.bib @@ -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 diff --git a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy index cf64aef..b10f396 100644 --- a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy +++ b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy @@ -117,14 +117,25 @@ text*[abs::abstract, \ -section*[introheader::introduction] - \ Introduction \ +section*[introheader::introduction] \ Introduction \ + text*[introtext::introduction]\ The linking of \<^emph>\formal\ and \<^emph>\informal\ 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 \iswff\<^sub>p\<^sub>r\<^sub>e\ is bound to a f is executed during the evaluation phase of these invariants and that checks: \<^item> Any \cond\ 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>\-0.3cm\ @{cartouche [display,indent=10,margin=70] \pre_ (a\<^sub>1::\\<^sub>1) ... (a\<^sub>n::\\<^sub>n) \ ,\} \<^vs>\-0.3cm\ @@ -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. \ text\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>\\<^url>\https://www.isa-afp.org/entries/Physical_Quantities.html\\, it is possible to express that the result of some calculation is of type \32 unsigned [m\<^sup>\s\<^sup>-\<^sup>2]\, so a 32-bit natural representing an acceleration in the SI-system. diff --git a/src/ontologies/CENELEC_50128/CENELEC_50128.thy b/src/ontologies/CENELEC_50128/CENELEC_50128.thy index badccb9..f907f81 100755 --- a/src/ontologies/CENELEC_50128/CENELEC_50128.thy +++ b/src/ontologies/CENELEC_50128/CENELEC_50128.thy @@ -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