Slight restructuring.
Ontology instances in one site, separated from the Isa_DOF core.
This commit is contained in:
parent
4c9e7c74a1
commit
497c79349b
|
@ -1,5 +1,5 @@
|
||||||
theory Example
|
theory Example
|
||||||
imports "../../CENELEC_50126"
|
imports "../../ontologies/CENELEC_50126"
|
||||||
keywords "Term" :: diag
|
keywords "Term" :: diag
|
||||||
begin
|
begin
|
||||||
|
|
||||||
|
|
|
@ -0,0 +1,216 @@
|
||||||
|
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:
|
||||||
|
- 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)
|
||||||
|
*}
|
||||||
|
|
||||||
|
theory CENELEC_50126
|
||||||
|
imports "../Isa_DOF"
|
||||||
|
begin
|
||||||
|
|
||||||
|
text{* Excerpt of the BE EN 50128:2011 *}
|
||||||
|
|
||||||
|
section {* Requirements-Analysis related Categories *}
|
||||||
|
|
||||||
|
doc_class requirement =
|
||||||
|
long_name :: "string option"
|
||||||
|
|
||||||
|
|
||||||
|
doc_class requirement_analysis =
|
||||||
|
no :: "nat"
|
||||||
|
where "requirement_item +"
|
||||||
|
|
||||||
|
|
||||||
|
text{*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
|
||||||
|
\<^item> Newtonian (non-relativistic) physics is assumed,
|
||||||
|
\<^item> @{term "P \<noteq> NP"},
|
||||||
|
\<^item> or the computational hardness of certain functions
|
||||||
|
relevant for cryptography (like prime-factorization).
|
||||||
|
Their acceptance is inherently outside the scope of the model
|
||||||
|
and can only established inside certification process by
|
||||||
|
authority argument.
|
||||||
|
*}
|
||||||
|
|
||||||
|
datatype hyp_type = physical | mathematical | computational | other
|
||||||
|
|
||||||
|
|
||||||
|
typ "CENELEC_50126.requirement"
|
||||||
|
|
||||||
|
|
||||||
|
doc_class hypothesis = requirement +
|
||||||
|
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. *}
|
||||||
|
|
||||||
|
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. *}
|
||||||
|
|
||||||
|
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. *}
|
||||||
|
|
||||||
|
doc_class srac = ec +
|
||||||
|
assumption_kind :: ass_kind <= (*default *) formal
|
||||||
|
|
||||||
|
section {* Design related Categories *}
|
||||||
|
|
||||||
|
doc_class design_item =
|
||||||
|
description :: string
|
||||||
|
|
||||||
|
datatype design_kind = unit | module | protocol
|
||||||
|
|
||||||
|
doc_class interface = design_item +
|
||||||
|
kind :: design_kind
|
||||||
|
|
||||||
|
|
||||||
|
section {* Requirements-Analysis related Categories *}
|
||||||
|
|
||||||
|
doc_class test_item =
|
||||||
|
nn :: "string option"
|
||||||
|
|
||||||
|
text{* subcategories are : *}
|
||||||
|
|
||||||
|
datatype test_kind = blackbox | whitebox | greybox | fuzz | pertubation
|
||||||
|
|
||||||
|
datatype test_coverage_criterion =
|
||||||
|
allpathk nat nat (* depth, test_coverage_degree *)
|
||||||
|
| mcdc nat (* depth, test_coverage_degree *)
|
||||||
|
| exhaustive
|
||||||
|
| dnf_E_d string nat (* equivalence class testing *)
|
||||||
|
| other string
|
||||||
|
|
||||||
|
doc_class test_specification = test_item +
|
||||||
|
short_goal :: string
|
||||||
|
|
||||||
|
doc_class test_case = test_item +
|
||||||
|
kind :: test_kind
|
||||||
|
descr :: string
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
doc_class test_result = test_item +
|
||||||
|
verdict :: bool
|
||||||
|
remarks :: string
|
||||||
|
covvrit :: test_coverage_criterion
|
||||||
|
|
||||||
|
datatype test_environment_kind = hardware_in_the_loop ("hil")
|
||||||
|
| simulated_hardware_in_the_loop ("shil")
|
||||||
|
|
||||||
|
doc_class test_environment = test_item +
|
||||||
|
descr :: string
|
||||||
|
kind :: test_environment_kind <= shil
|
||||||
|
|
||||||
|
doc_class test_tool = test_item +
|
||||||
|
descr :: string
|
||||||
|
|
||||||
|
doc_class test_requirement = test_item +
|
||||||
|
descr :: string
|
||||||
|
|
||||||
|
doc_class test_adm_role = test_item +
|
||||||
|
name :: string
|
||||||
|
|
||||||
|
doc_class test_documentation =
|
||||||
|
no :: "nat"
|
||||||
|
where "(test_specification.((test_case.test_result)+.(test_environment|test_tool))+.
|
||||||
|
[test_requirement].test_adm_role"
|
||||||
|
where "(test_specification.((test_case.test_result)+.(test_environment|test_tool))+.
|
||||||
|
[test_requirement].test_adm_role"
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
section{* Example *}
|
||||||
|
|
||||||
|
text*[ass122::srac] {* The overall sampling frequence of the odometer
|
||||||
|
subsystem is therefore 14 khz, which includes sampling, computing and
|
||||||
|
result communication times... *}
|
||||||
|
|
||||||
|
text*[t10::test_result] {* This is a meta-test. This could be an ML-command
|
||||||
|
that governs the external test-execution via, eg., a makefile or specific calls
|
||||||
|
to a test-environment or test-engine *}
|
||||||
|
|
||||||
|
|
||||||
|
text \<open> As established by @{docref \<open>t10\<close>}, the
|
||||||
|
assumption @{docref \<open>ass122\<close>} is validated. \<close>
|
||||||
|
|
||||||
|
|
||||||
|
section{* Provisory Setup *}
|
||||||
|
|
||||||
|
(* Hack: This should be generated automatically: *)
|
||||||
|
ML{*
|
||||||
|
val _ = Theory.setup
|
||||||
|
((DocAttrParser.control_antiquotation @{binding srac}
|
||||||
|
(DOF_core.name2doc_class_name @{theory} "srac")
|
||||||
|
{strict_checking=true}
|
||||||
|
"\\autoref{" "}" ) #>
|
||||||
|
(DocAttrParser.control_antiquotation @{binding ec}
|
||||||
|
(DOF_core.name2doc_class_name @{theory} "ec")
|
||||||
|
{strict_checking=true}
|
||||||
|
"\\autoref{" "}")#>
|
||||||
|
(DocAttrParser.control_antiquotation @{binding test_specification}
|
||||||
|
(DOF_core.name2doc_class_name @{theory} "test_specification")
|
||||||
|
{strict_checking=true}
|
||||||
|
"\\label{" "}"))
|
||||||
|
|
||||||
|
*}
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
section{* Testing and Validation *}
|
||||||
|
|
||||||
|
|
||||||
|
ML{*
|
||||||
|
DOF_core.name2doc_class_name @{theory} "requirement";
|
||||||
|
DOF_core.name2doc_class_name @{theory} "srac";
|
||||||
|
DOF_core.is_defined_cid_global "srac" @{theory};
|
||||||
|
DOF_core.is_defined_cid_global "ec" @{theory};
|
||||||
|
|
||||||
|
DOF_core.is_subclass @{context} "CENELEC_50126.srac" "CENELEC_50126.ec";
|
||||||
|
DOF_core.is_subclass @{context} "CENELEC_50126.ec" "CENELEC_50126.srac";
|
||||||
|
|
||||||
|
val ({maxano, tab},tab2) = DOF_core.get_data @{context};
|
||||||
|
Symtab.dest tab;
|
||||||
|
Symtab.dest tab2;
|
||||||
|
|
||||||
|
|
||||||
|
*}
|
||||||
|
|
||||||
|
|
||||||
|
ML{*
|
||||||
|
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;
|
||||||
|
*}
|
||||||
|
|
||||||
|
|
||||||
|
end
|
||||||
|
|
|
@ -0,0 +1,92 @@
|
||||||
|
theory LNCS_onto
|
||||||
|
imports Isa_DOF
|
||||||
|
begin
|
||||||
|
|
||||||
|
doc_class title =
|
||||||
|
short_title :: "string option" -- None
|
||||||
|
|
||||||
|
doc_class subtitle =
|
||||||
|
abbrev :: "string option" -- None
|
||||||
|
|
||||||
|
doc_class author =
|
||||||
|
affiliation :: "string"
|
||||||
|
|
||||||
|
doc_class abstract =
|
||||||
|
keywds :: "string list" -- None
|
||||||
|
|
||||||
|
doc_class introduction =
|
||||||
|
main_author :: "author option" -- None
|
||||||
|
|
||||||
|
doc_class tech_section =
|
||||||
|
main_author :: "author option" -- None
|
||||||
|
|
||||||
|
doc_class example_section =
|
||||||
|
main_author :: "author option" -- None
|
||||||
|
|
||||||
|
|
||||||
|
doc_class conclusion =
|
||||||
|
main_author :: "author option" -- None
|
||||||
|
|
||||||
|
doc_class bibliography =
|
||||||
|
style :: "string option" -- "''LNCS''"
|
||||||
|
|
||||||
|
text{* Besides subtyping, there is another relation between
|
||||||
|
doc_classes: a class can be a \emph{monitor} to other ones,
|
||||||
|
which is expressed by occurrence in the where clause.
|
||||||
|
While sub-classing refers to data-inheritance of attributes,
|
||||||
|
a monitor captures structural constraints -- the order --
|
||||||
|
in which instances of monitored classes may occur.
|
||||||
|
|
||||||
|
The control of monitors is done by the commands:
|
||||||
|
-- monitor <doc-class>
|
||||||
|
-- close_monitor <doc-class>
|
||||||
|
where the automaton of the monitor class is expected
|
||||||
|
to be in a final state.
|
||||||
|
|
||||||
|
Monitors can be nested.
|
||||||
|
|
||||||
|
Classes neither directly or via inheritance indirectly
|
||||||
|
mentioned in the monitor are \emph{independent} from
|
||||||
|
a monitor and may occur freely.
|
||||||
|
*}
|
||||||
|
|
||||||
|
|
||||||
|
doc_class article =
|
||||||
|
T :: "title option" -- None
|
||||||
|
ST :: "subtitle option" -- None
|
||||||
|
AS :: "author list"
|
||||||
|
ABS :: "abstract option"
|
||||||
|
INTRO :: "introduction option"
|
||||||
|
TS :: "tech_section list"
|
||||||
|
EXS :: "example_section list"
|
||||||
|
CON :: "conclusion"
|
||||||
|
where "(title .
|
||||||
|
[subtitle] .
|
||||||
|
(author)+ .
|
||||||
|
abstract .
|
||||||
|
introduction .
|
||||||
|
(tech_section)+ .
|
||||||
|
conclusion .
|
||||||
|
bibliography)"
|
||||||
|
|
||||||
|
-- \<open>other idea: capture the essence of a monitor class as trace.
|
||||||
|
trace would be `predefined id` like `main` in C.
|
||||||
|
\<close>
|
||||||
|
|
||||||
|
doc_class article' =
|
||||||
|
trace :: "(title + subtitle + author+ abstract +
|
||||||
|
introduction + tech_section + example_section +
|
||||||
|
conclusion + bibliography) list"
|
||||||
|
where "(title .
|
||||||
|
[subtitle] .
|
||||||
|
(author)+ .
|
||||||
|
abstract .
|
||||||
|
introduction .
|
||||||
|
(tech_section | example_section)+ .
|
||||||
|
conclusion .
|
||||||
|
bibliography)"
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
end
|
||||||
|
|
Loading…
Reference in New Issue