forked from Isabelle_DOF/Isabelle_DOF
parent
9757268b55
commit
a69b1ec2ff
|
|
@ -1,14 +1,14 @@
|
|||
chapter \<open>An Outline of a CENELEC Ontology\<close>
|
||||
|
||||
text{* NOTE: An Ontology-Model of a certification standard such as CENELEC or
|
||||
Common Criteria identifies:
|
||||
text\<open> NOTE: An Ontology-Model of a certification standard such as CENELEC or Common Criteria
|
||||
identifies:
|
||||
- notions (conceptual \emph{categories}) having \emph{instances}
|
||||
(similar to classes and objects),
|
||||
- their subtype relation (eg., a "SRAC" is an "assumption"),
|
||||
- their syntactical structure
|
||||
(for the moment: defined by regular expressions describing the
|
||||
order of category instances in the overall document as a regular language)
|
||||
*}
|
||||
\<close>
|
||||
|
||||
(*<<*)
|
||||
theory CENELEC_50126
|
||||
|
|
@ -17,9 +17,9 @@ begin
|
|||
(*>>*)
|
||||
|
||||
|
||||
text{* Excerpt of the BE EN 50128:2011 *}
|
||||
text\<open> Excerpt of the BE EN 50128:2011 \<close>
|
||||
|
||||
section {* Requirements-Analysis related Categories *}
|
||||
section\<open> Requirements-Analysis related Categories \<close>
|
||||
|
||||
doc_class requirement =
|
||||
long_name :: "string option"
|
||||
|
|
@ -30,7 +30,7 @@ doc_class requirement_analysis =
|
|||
accepts "\<lbrace>requirement\<rbrace>\<^sup>+"
|
||||
|
||||
|
||||
text{*The category @{emph \<open>hypothesis\<close>} is used for assumptions from the
|
||||
text\<open>The category @{emph \<open>hypothesis\<close>} is used for assumptions from the
|
||||
foundational mathematical or physical domain, so for example:
|
||||
\<^item> the Mordell-Lang conjecture holds,
|
||||
\<^item> euklidian geometry is assumed, or
|
||||
|
|
@ -38,7 +38,7 @@ text{*The category @{emph \<open>hypothesis\<close>} is used for assumptions fro
|
|||
Their acceptance is inherently outside the scope of the model
|
||||
and can only established inside certification process by
|
||||
authority argument.
|
||||
*}
|
||||
\<close>
|
||||
|
||||
datatype hyp_type = physical | mathematical | computational | other
|
||||
|
||||
|
|
@ -48,39 +48,35 @@ typ "CENELEC_50126.requirement"
|
|||
doc_class hypothesis = requirement +
|
||||
hyp_type :: hyp_type <= physical (* default *)
|
||||
|
||||
text{* The following sub-class of security related hypothesis might comprise, for example:
|
||||
text\<open> The following sub-class of security related hypothesis might comprise, for example:
|
||||
\<^item> @{term "P \<noteq> NP"},
|
||||
\<^item> or the computational hardness of certain functions
|
||||
relevant for cryptography (like prime-factorization).
|
||||
*}
|
||||
relevant for cryptography (like prime-factorization).\<close>
|
||||
|
||||
doc_class security_hyp = hypothesis +
|
||||
hyp_type :: hyp_type <= physical (* default *)
|
||||
|
||||
|
||||
text{*The category @{emph \<open>assumption\<close>} is used for domain-specific assumptions.
|
||||
It has formal, semi-formal and informal sub-categories. They have to be
|
||||
tracked and discharged by appropriate validation procedures within a
|
||||
certification process, by it by test or proof. *}
|
||||
text\<open>The category \<^emph>\<open>assumption\<close> is used for domain-specific assumptions. It has formal, semi-formal
|
||||
and informal sub-categories. They have to be tracked and discharged by appropriate
|
||||
validation procedures within a certification process, by it by test or proof. \<close>
|
||||
|
||||
datatype ass_kind = informal | semiformal | formal
|
||||
|
||||
doc_class assumption = requirement +
|
||||
assumption_kind :: ass_kind <= informal
|
||||
|
||||
text{*The category @{emph \<open>exported constraint\<close>} (or @{emph \<open>ec\<close>} for short)
|
||||
is used for formal assumptions, that arise during the analysis,
|
||||
design or implementation and have to be tracked till the final
|
||||
evaluation target, and discharged by appropriate validation procedures
|
||||
within the certification process, by it by test or proof. *}
|
||||
text\<open> The category \<^emph>\<open>exported constraint\<close> (or \<^emph>\<open>ec\<close> for short) is used for formal assumptions, that
|
||||
arise during the analysis, design or implementation and have to be tracked till the final
|
||||
evaluation target, and discharged by appropriate validation procedures within the certification
|
||||
process, by it by test or proof. \<close>
|
||||
|
||||
doc_class ec = assumption +
|
||||
assumption_kind :: ass_kind <= (*default *) formal
|
||||
|
||||
text{*The category @{emph \<open>safety related application condition\<close>} (or @{emph \<open>srac\<close>}
|
||||
for short) is used for @{typ ec}'s that establish safety properties
|
||||
of the evaluation target. Their track-ability throughout the certification
|
||||
is therefore particularly critical. *}
|
||||
text\<open> The category \<^emph>\<open>safety related application condition\<close> (or \<^emph>\<open>srac\<close> for short) is used for
|
||||
@{typ ec}'s that establish safety properties of the evaluation target. Their track-ability
|
||||
throughout the certification is therefore particularly critical. \<close>
|
||||
|
||||
doc_class srac = ec +
|
||||
assumption_kind :: ass_kind <= (*default *) formal
|
||||
|
|
@ -95,7 +91,7 @@ doc_class security = ec +
|
|||
assumption_kind :: ass_kind <= (*default *) formal
|
||||
|
||||
|
||||
section {* Design related Categories *}
|
||||
section\<open> Design related Categories \<close>
|
||||
|
||||
doc_class design_item =
|
||||
description :: string
|
||||
|
|
@ -106,7 +102,7 @@ doc_class interface = design_item +
|
|||
kind :: design_kind
|
||||
|
||||
|
||||
section {* Requirements-Analysis related Categories *}
|
||||
section\<open> Requirements-Analysis related Categories \<close>
|
||||
|
||||
doc_class test_item =
|
||||
nn :: "string option"
|
||||
|
|
@ -161,10 +157,9 @@ doc_class test_documentation =
|
|||
|
||||
|
||||
|
||||
section{* Testing and Validation *}
|
||||
section\<open> Testing and Validation \<close>
|
||||
|
||||
|
||||
ML{*
|
||||
ML\<open>
|
||||
DOF_core.name2doc_class_name @{theory} "requirement";
|
||||
DOF_core.name2doc_class_name @{theory} "srac";
|
||||
DOF_core.is_defined_cid_global "srac" @{theory};
|
||||
|
|
@ -178,26 +173,25 @@ DOF_core.is_subclass @{context} "CENELEC_50126.ec" "CENELEC_50126.test_require
|
|||
val {docobj_tab={maxano, tab=ref_tab},docclass_tab=class_tab,...} = DOF_core.get_data @{context};
|
||||
Symtab.dest ref_tab;
|
||||
Symtab.dest class_tab;
|
||||
*}
|
||||
\<close>
|
||||
|
||||
|
||||
ML{*
|
||||
ML\<open>
|
||||
"XXXXXXXXXXXXXXXXX";
|
||||
|
||||
DOF_core.get_attributes_local "srac" @{context};
|
||||
|
||||
@{term assumption_kind}
|
||||
*}
|
||||
\<close>
|
||||
|
||||
|
||||
ML{*
|
||||
ML\<open>
|
||||
DOF_core.name2doc_class_name @{theory} "requirement";
|
||||
Syntax.parse_typ @{context} "requirement";
|
||||
val Type(t,_) = Syntax.parse_typ @{context} "requirement" handle ERROR _ => dummyT;
|
||||
Syntax.read_typ @{context} "hypothesis" handle _ => dummyT;
|
||||
Proof_Context.init_global;
|
||||
*}
|
||||
|
||||
\<close>
|
||||
|
||||
end
|
||||
|
||||
Loading…
Reference in New Issue