pierre.derathe
/
Isabelle_DOF
Archived
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Merge branch 'ICFEM-2022' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF into ICFEM-2022

This commit is contained in:
Burkhart Wolff 2022-04-19 14:03:57 +02:00
parent c9beb99b7a aa6d11f73c
commit ee3428d384
2 changed files with 70 additions and 28 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -36,6 +36,40 @@
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{MendilASMP21,
author = {Isma{\"{\i}}l Mendil and
Yamine A{\"{\i}}t-Ameur and
Neeraj Kumar Singh and
Dominique M{\'{e}}ry and
Philippe A. Palanque},
title = {Standard Conformance-by-Construction with Event-B},
booktitle = {Formal Methods for Industrial Critical Systems - 26th International
Conference, {FMICS}, Paris, France},
series = {LNCS},
volume = {12863},
pages = {126--146},
publisher = {Springer},
year = {2021},
doi = {10.1007/978-3-030-85248-1\_8}
}
@inproceedings{FotsoFLM18,
author = {Steve Jeffrey Tueno Fotso and
Marc Frappier and
R{\'{e}}gine Laleau and
Amel Mammar},
title = {Modeling the Hybrid {ERTMS/ETCS} Level 3 Standard Using a Formal Requirements
Engineering Approach},
booktitle = {Abstract State Machines, Alloy, B, TLA, VDM, and {Z} - 6th International
Conference, {ABZ}, Southampton, UK},
series = {LLNCS},
volume = {10817},
pages = {262--276},
publisher = {Springer},
year = {2018},
doi = {10.1007/978-3-319-91271-4\_18}
}
@MISC{atl,
title = {ATL - A model transformation technology},
note={\url{https://www.eclipse.org/atl/}},

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

@ -1262,33 +1262,7 @@ Therefore it is possible to impose that certain values refer to physical dimensi
measured in a concrete metrological system.
\<close>
section*[concl::conclusion]\<open>Conclusion\<close>
text\<open>We presented \<^dof>, an ontology framework
deeply integrating continuous-check\slash continuous-build functionality into
the formal development process in \<^hol>. The novel feature of term-contexts in \<^dof>,
which permits term-antiquotations elaborated in the parsing process, paves the
way for the abstract specification of meta-data constraints as well the possibility
of advanced search in the meta-data of document elements. Thus it profits and
extends Isabelle's document-centric view on formal development.
Many ontological languages such as OWL as well as the meta-modeling technology
available for UML/OCL provide concepts for semantic rules and constraints, but
leave the validation checking usually to external tools (if implementing them at all).
This limits their practical usefulness drastically. Our approach treats invariants as
first-class citizens, and turns them into an object of formal study in, for example,
ontological mappings. Such a technology exists, to our knowledge, for the first time.
Our experiments with adaptations of existing ontologies from engineering and mathematics
show that \<^dof>'s ODL has sufficient expressive power to cover all aspects
of languages such as OWL (with perhaps the exception of multiple inheritance on classes).
However, these ontologies have been developed specifically \<^emph>\<open>in\<close> OWL and target
its specific support, the Protégé editor @{cite "protege"}. We argue that \<^dof> might ask
for a re-engineering of these ontologies: less deep hierarchies, rather deeper structure
in meta-data and stronger invariants.
\<close>
subsection*[rw::related_work]\<open>Related Work\<close>
section*[rw::related_work]\<open>Related Work\<close>
text\<open>There are a number of approaches to use ontologies for structuring the link between
information and knowledge, and to make it amenable to
@ -1315,6 +1289,14 @@ Some are targeting mathematical libraries:
and the more general ScienceWISE \<^footnote>\<open>\<^url>\<open>http://sciencewise.info/ontology/\<close>.\<close>
that allows users to introduce their own category concepts.
Regarding using formal methods to formalise standards, Event-B method was used by
Fotso et al. @{cite "FotsoFLM18"} to propose a specification of the hybrid ERTMS/ETCS level 3 standard,
in which requirements are specified using SysML/KAOS goal diagrams that are translated into
Event-B, and domain-specific properties are specified by ontologies.
In another case, Mendil et al. @{cite "MendilASMP21"} proposes an Event-B framework for formalising standard
conformance through formal modelling of standards as ontologies.
The proposed approach was exemplified on ARINC 661 standard and weather radar system application.
Our approach emphasizes type-safeness, expressive power and ``depth'' of meta-data,
which is adapted to the specific needs of ITP systems and theory developments.
@ -1333,7 +1315,33 @@ Some are targeting mathematical libraries:
% exist approaches based on strong type systems
\<close>
subsection*[fw::related_work]\<open>Future Work\<close>
section*[concl::conclusion]\<open>Conclusion\<close>
text\<open>We presented \<^dof>, an ontology framework
deeply integrating continuous-check\slash continuous-build functionality into
the formal development process in \<^hol>. The novel feature of term-contexts in \<^dof>,
which permits term-antiquotations elaborated in the parsing process, paves the
way for the abstract specification of meta-data constraints as well the possibility
of advanced search in the meta-data of document elements. Thus it profits and
extends Isabelle's document-centric view on formal development.
Many ontological languages such as OWL as well as the meta-modeling technology
available for UML/OCL provide concepts for semantic rules and constraints, but
leave the validation checking usually to external tools (if implementing them at all).
This limits their practical usefulness drastically. Our approach treats invariants as
first-class citizens, and turns them into an object of formal study in, for example,
ontological mappings. Such a technology exists, to our knowledge, for the first time.
Our experiments with adaptations of existing ontologies from engineering and mathematics
show that \<^dof>'s ODL has sufficient expressive power to cover all aspects
of languages such as OWL (with perhaps the exception of multiple inheritance on classes).
However, these ontologies have been developed specifically \<^emph>\<open>in\<close> OWL and target
its specific support, the Protégé editor @{cite "protege"}. We argue that \<^dof> might ask
for a re-engineering of these ontologies: less deep hierarchies, rather deeper structure
in meta-data and stronger invariants.
\<close>
(*subsection*[fw::related_work]\<open>Future Work\<close>*)
text\<open> We plan to complement \<^dof> with incremental LaTeX generation and a previewing facility
that will further increase the usability of our framework for the ontology-conform editing
of formal content, be it in the engineering or the mathematics domain