Implement CENELEC Table A.1
ci/woodpecker/push/build Pipeline was successful
Details
ci/woodpecker/push/build Pipeline was successful
Details
This commit is contained in:
parent
9673359688
commit
a82f316997
|
@ -215,6 +215,10 @@ struct
|
|||
type docclass_inv_tab = (string -> {is_monitor:bool} -> Context.generic -> bool) Symtab.table
|
||||
val initial_docclass_inv_tab : docclass_inv_tab = Symtab.empty
|
||||
|
||||
type docclass_closing_inv_tab =
|
||||
(string -> {is_monitor:bool} -> Context.generic -> bool) Symtab.table
|
||||
val initial_docclass_closing_inv_tab : docclass_closing_inv_tab = Symtab.empty
|
||||
|
||||
type open_monitor_info = {accepted_cids : string list,
|
||||
rejected_cids : string list,
|
||||
automatas : RegExpInterface.automaton list
|
||||
|
@ -232,20 +236,22 @@ structure Data = Generic_Data
|
|||
docclass_tab : docclass_tab,
|
||||
ISA_transformer_tab : ISA_transformer_tab,
|
||||
monitor_tab : monitor_tab,
|
||||
docclass_inv_tab : docclass_inv_tab}
|
||||
docclass_inv_tab : docclass_inv_tab,
|
||||
docclass_closing_inv_tab : docclass_closing_inv_tab}
|
||||
val empty = {docobj_tab = initial_docobj_tab,
|
||||
docclass_tab = initial_docclass_tab,
|
||||
ISA_transformer_tab = initial_ISA_tab,
|
||||
monitor_tab = initial_monitor_tab,
|
||||
docclass_inv_tab = initial_docclass_inv_tab
|
||||
docclass_inv_tab = initial_docclass_inv_tab,
|
||||
docclass_closing_inv_tab = initial_docclass_closing_inv_tab
|
||||
}
|
||||
val extend = I
|
||||
fun merge( {docobj_tab=d1,docclass_tab = c1,
|
||||
ISA_transformer_tab = e1, monitor_tab=m1,
|
||||
docclass_inv_tab = n1},
|
||||
docclass_inv_tab = n1, docclass_closing_inv_tab = cn1},
|
||||
{docobj_tab=d2,docclass_tab = c2,
|
||||
ISA_transformer_tab = e2, monitor_tab=m2,
|
||||
docclass_inv_tab = n2}) =
|
||||
docclass_inv_tab = n2, docclass_closing_inv_tab = cn2}) =
|
||||
{docobj_tab=merge_docobj_tab (d1,d2),
|
||||
docclass_tab = merge_docclass_tab (c1,c2),
|
||||
(*
|
||||
|
@ -257,7 +263,9 @@ structure Data = Generic_Data
|
|||
ISA_transformer_tab = Symtab.merge (fn (_ , _) => true)(e1,e2),
|
||||
monitor_tab = override(m1,m2),
|
||||
(* PROVISORY ... ITS A REAL QUESTION HOW TO DO THIS!*)
|
||||
docclass_inv_tab = override(n1,n2)
|
||||
docclass_inv_tab = override(n1,n2),
|
||||
(* PROVISORY ... ITS A REAL QUESTION HOW TO DO THIS!*)
|
||||
docclass_closing_inv_tab = override(cn1,cn2)
|
||||
(* PROVISORY ... ITS A REAL QUESTION HOW TO DO THIS!*)
|
||||
}
|
||||
);
|
||||
|
@ -269,25 +277,35 @@ val get_data_global = Data.get o Context.Theory;
|
|||
val map_data_global = Context.theory_map o map_data;
|
||||
|
||||
|
||||
fun upd_docobj_tab f {docobj_tab,docclass_tab,ISA_transformer_tab, monitor_tab,docclass_inv_tab} =
|
||||
fun upd_docobj_tab f {docobj_tab,docclass_tab,ISA_transformer_tab,
|
||||
monitor_tab,docclass_inv_tab, docclass_closing_inv_tab} =
|
||||
{docobj_tab = f docobj_tab, docclass_tab=docclass_tab,
|
||||
ISA_transformer_tab=ISA_transformer_tab, monitor_tab=monitor_tab,
|
||||
docclass_inv_tab=docclass_inv_tab};
|
||||
fun upd_docclass_tab f {docobj_tab=x,docclass_tab = y,ISA_transformer_tab = z, monitor_tab, docclass_inv_tab} =
|
||||
docclass_inv_tab=docclass_inv_tab, docclass_closing_inv_tab=docclass_closing_inv_tab};
|
||||
fun upd_docclass_tab f {docobj_tab=x,docclass_tab = y,ISA_transformer_tab = z,
|
||||
monitor_tab, docclass_inv_tab, docclass_closing_inv_tab} =
|
||||
{docobj_tab=x,docclass_tab = f y,ISA_transformer_tab = z, monitor_tab=monitor_tab,
|
||||
docclass_inv_tab=docclass_inv_tab};
|
||||
fun upd_ISA_transformers f{docobj_tab=x,docclass_tab = y,ISA_transformer_tab = z, monitor_tab, docclass_inv_tab} =
|
||||
docclass_inv_tab=docclass_inv_tab, docclass_closing_inv_tab=docclass_closing_inv_tab};
|
||||
fun upd_ISA_transformers f {docobj_tab=x,docclass_tab = y,ISA_transformer_tab = z,
|
||||
monitor_tab, docclass_inv_tab, docclass_closing_inv_tab} =
|
||||
{docobj_tab=x,docclass_tab = y,ISA_transformer_tab = f z, monitor_tab=monitor_tab,
|
||||
docclass_inv_tab=docclass_inv_tab};
|
||||
fun upd_monitor_tabs f {docobj_tab,docclass_tab,ISA_transformer_tab, monitor_tab, docclass_inv_tab} =
|
||||
docclass_inv_tab=docclass_inv_tab, docclass_closing_inv_tab=docclass_closing_inv_tab};
|
||||
fun upd_monitor_tabs f {docobj_tab,docclass_tab,ISA_transformer_tab,
|
||||
monitor_tab, docclass_inv_tab, docclass_closing_inv_tab} =
|
||||
{docobj_tab = docobj_tab,docclass_tab = docclass_tab,
|
||||
ISA_transformer_tab = ISA_transformer_tab, monitor_tab = f monitor_tab,
|
||||
docclass_inv_tab=docclass_inv_tab};
|
||||
fun upd_docclass_inv_tab f {docobj_tab,docclass_tab,ISA_transformer_tab, monitor_tab, docclass_inv_tab} =
|
||||
docclass_inv_tab=docclass_inv_tab, docclass_closing_inv_tab=docclass_closing_inv_tab};
|
||||
fun upd_docclass_inv_tab f {docobj_tab,docclass_tab,ISA_transformer_tab,
|
||||
monitor_tab, docclass_inv_tab, docclass_closing_inv_tab} =
|
||||
{docobj_tab = docobj_tab,docclass_tab = docclass_tab,
|
||||
ISA_transformer_tab = ISA_transformer_tab, monitor_tab = monitor_tab,
|
||||
docclass_inv_tab = f docclass_inv_tab};
|
||||
docclass_inv_tab = f docclass_inv_tab, docclass_closing_inv_tab=docclass_closing_inv_tab};
|
||||
|
||||
fun upd_docclass_closing_inv_tab f {docobj_tab,docclass_tab,ISA_transformer_tab,
|
||||
monitor_tab, docclass_inv_tab, docclass_closing_inv_tab} =
|
||||
{docobj_tab = docobj_tab,docclass_tab = docclass_tab,
|
||||
ISA_transformer_tab = ISA_transformer_tab, monitor_tab = monitor_tab,
|
||||
docclass_inv_tab=docclass_inv_tab, docclass_closing_inv_tab= f docclass_closing_inv_tab};
|
||||
|
||||
fun get_accepted_cids ({accepted_cids, ... } : open_monitor_info) = accepted_cids
|
||||
fun get_automatas ({automatas, ... } : open_monitor_info) = automatas
|
||||
|
@ -413,6 +431,14 @@ fun update_class_invariant cid_long f thy =
|
|||
thy
|
||||
end
|
||||
|
||||
fun update_class_closing_invariant cid_long f thy =
|
||||
let val _ = if is_defined_cid_global' cid_long thy then ()
|
||||
else error("undefined class id : " ^cid_long)
|
||||
in map_data_global (upd_docclass_closing_inv_tab (Symtab.update (cid_long,
|
||||
(fn ctxt => ((writeln("Closing Invariant check of: " ^cid_long); f ctxt ))))))
|
||||
thy
|
||||
end
|
||||
|
||||
fun get_class_invariant cid_long thy =
|
||||
let val _ = if is_defined_cid_global' cid_long thy then ()
|
||||
else error("undefined class id : " ^cid_long)
|
||||
|
@ -422,6 +448,15 @@ fun get_class_invariant cid_long thy =
|
|||
| SOME f => f
|
||||
end
|
||||
|
||||
fun get_class_closing_invariant cid_long thy =
|
||||
let val _ = if is_defined_cid_global' cid_long thy then ()
|
||||
else error("undefined class id : " ^cid_long)
|
||||
val {docclass_closing_inv_tab, ...} = get_data_global thy
|
||||
in case Symtab.lookup docclass_closing_inv_tab cid_long of
|
||||
NONE => K(K(K true))
|
||||
| SOME f => f
|
||||
end
|
||||
|
||||
val SPY = Unsynchronized.ref(Bound 0)
|
||||
|
||||
fun check_regexps term =
|
||||
|
@ -1755,8 +1790,11 @@ fun close_monitor_command (args as (((oid:string,pos),cid_pos),
|
|||
val markup = docref_markup false oid id pos;
|
||||
val _ = Context_Position.report (Proof_Context.init_global thy) pos markup;
|
||||
val check_inv = (DOF_core.get_class_invariant cid_long thy oid) {is_monitor=true}
|
||||
o Context.Theory
|
||||
val check_closing_inv = (DOF_core.get_class_closing_invariant cid_long thy oid) {is_monitor=true}
|
||||
o Context.Theory
|
||||
in thy |> update_instance_command args
|
||||
in thy |> (fn thy => (check_closing_inv thy; thy))
|
||||
|> update_instance_command args
|
||||
|> (fn thy => (check_inv thy; thy))
|
||||
|> (fn thy => if Config.get_global thy DOF_core.invariants_checking = true
|
||||
then Value_Command.Docitem_Parser.check_invariants thy oid
|
||||
|
|
|
@ -281,18 +281,21 @@ chapter\<open>Software Management and Organisation\<close>
|
|||
text\<open>Representing chapter 5 in @{cite "bsi:50128:2014"}.\<close>
|
||||
|
||||
section\<open>Organization, Roles and Responsabilities\<close>
|
||||
text\<open>see also section \<^emph>\<open>Software management and organization\<close>.\<close>
|
||||
text\<open>See also section \<^emph>\<open>Software management and organization\<close>. and Annex B and C\<close>
|
||||
|
||||
datatype role = PM \<comment> \<open>Program Manager\<close>
|
||||
| RQM \<comment> \<open>Requirements Manager\<close>
|
||||
text\<open>REQ role in Table C.1 is assumed to be a typo and should be RQM.\<close>
|
||||
|
||||
datatype role = RQM \<comment> \<open>Requirements Manager\<close>
|
||||
| DES \<comment> \<open>Designer\<close>
|
||||
| IMP \<comment> \<open>Implementer\<close>
|
||||
| ASR \<comment> \<open>Assessor\<close>
|
||||
| INT \<comment> \<open>Integrator\<close>
|
||||
| TST \<comment> \<open>Tester\<close>
|
||||
| VER \<comment> \<open>Verifier\<close>
|
||||
| VnV \<comment> \<open>Verification and Validation\<close>
|
||||
| INT \<comment> \<open>Integrator\<close>
|
||||
| VAL \<comment> \<open>Validator\<close>
|
||||
| ASR \<comment> \<open>Assessor\<close>
|
||||
| PM \<comment> \<open>Program Manager\<close>
|
||||
| CM \<comment> \<open>Configuration Manager\<close>
|
||||
| No_Role_Defined \<comment> \<open>See Annex C footnote a\<close>
|
||||
|
||||
|
||||
|
||||
|
@ -303,20 +306,26 @@ datatype phase = SYSDEV_ext \<comment> \<open> System Development Phase (externa
|
|||
| SCDES \<comment> \<open>Software Component Design\<close>
|
||||
| CInT \<comment> \<open>Component Implementation and Testing\<close>
|
||||
| SI \<comment> \<open>Software Integration\<close>
|
||||
| SV \<comment> \<open>Software Validation\<close>
|
||||
| SV \<comment> \<open>Overall Software Testing/Final Validation\<close>
|
||||
| SCADA \<comment> \<open>Systems Configured by Application Data/Algorithms\<close>
|
||||
| SD \<comment> \<open>Software Deployment\<close>
|
||||
| SM \<comment> \<open>Software Maintenance\<close>
|
||||
| SA \<comment> \<open>Software Assessment\<close>
|
||||
|
||||
abbreviation software_planning :: "phase" where "software_planning \<equiv> SPl"
|
||||
abbreviation software_requirements :: "phase" where "software_requirements \<equiv> SR"
|
||||
abbreviation software_architecture_and_design :: "phase"
|
||||
where "software_architecture_and_design \<equiv> SADES"
|
||||
abbreviation software_component_design :: "phase" where "software_component_design \<equiv> SCDES"
|
||||
abbreviation component_implementation_and_testing :: "phase"
|
||||
where "component_implementation_and_testing \<equiv> CInT"
|
||||
where "component_implementation_and_testing \<equiv> CInT"
|
||||
abbreviation software_integration :: "phase" where "software_integration \<equiv> SI"
|
||||
abbreviation software_validation :: "phase" where "software_validation \<equiv> SV"
|
||||
abbreviation systems_configured_application_data_algorithm :: "phase"
|
||||
where "systems_configured_application_data_algorithm \<equiv> SCADA"
|
||||
abbreviation software_deployment :: "phase" where "software_deployment \<equiv> SD"
|
||||
abbreviation software_maintenance :: "phase" where "software_maintenance \<equiv> SM"
|
||||
abbreviation software_assessment :: "phase" where "software_assessment \<equiv> SM"
|
||||
|
||||
term "SR" (* meta-test *)
|
||||
|
||||
|
@ -327,8 +336,17 @@ datatype sil = SIL0 | SIL1 | SIL2 | SIL3 | SIL4
|
|||
|
||||
type_synonym safety_integration_level = sil
|
||||
|
||||
text\<open>Requirement levels specified Annex A: we use the term \<^emph>\<open>normative level\<close> to distinguish
|
||||
them from the requirements specified in the standard.\<close>
|
||||
|
||||
doc_class objectives =
|
||||
datatype normative_level =
|
||||
M \<comment> \<open>(Mandatory)\<close>
|
||||
| HR \<comment> \<open>Highly Recommended\<close>
|
||||
| R \<comment> \<open>Recommended\<close>
|
||||
| Any \<comment> \<open>No recommendation\<close>
|
||||
| NR \<comment> \<open>Not Recommended\<close>
|
||||
|
||||
doc_class objective =
|
||||
long_name :: "string option"
|
||||
is_concerned :: "role set"
|
||||
|
||||
|
@ -425,7 +443,7 @@ doc_class SIR = requirement +
|
|||
type_synonym safety_integrity_requirement = SIR
|
||||
|
||||
text\<open>The following class is a bit unclear about usage and seems to be in
|
||||
sfcual mismatch with @{typ objectives}: \<close>
|
||||
sfcual mismatch with @{typ objective}: \<close>
|
||||
doc_class SILA = requirement +
|
||||
is_concerned :: "role set" <= "UNIV"
|
||||
alloc :: "sil" <= "SIL0"
|
||||
|
@ -520,11 +538,14 @@ section\<open> Design and Test Documents \<close>
|
|||
|
||||
doc_class cenelec_document = text_element +
|
||||
phase :: "phase"
|
||||
level :: "int option" <= "Some(0)"
|
||||
sil :: "sil"
|
||||
level :: "int option" <= "Some(0)"
|
||||
nlvl :: "normative_level" \<comment> \<open>Annex A Table A.1\<close>
|
||||
written_by :: "role option" \<comment> \<open>Annex C Table C.1 \<close>
|
||||
fst_check :: "role option" \<comment> \<open>Annex C Table C.1\<close>
|
||||
snd_check :: "role option" \<comment> \<open>Annex C Table C.1\<close>
|
||||
is_concerned :: "role set" <= "UNIV"
|
||||
is_concerned :: "role set" <= "UNIV"
|
||||
accepts "\<lbrace>objective\<rbrace>\<^sup>+||\<lbrace>requirement\<rbrace>\<^sup>+"
|
||||
invariant must_be_chapter :: "text_element.level \<sigma> = Some(0)"
|
||||
invariant three_eyes_prcpl:: " written_by \<sigma> \<noteq> fst_check \<sigma>
|
||||
\<and> written_by \<sigma> \<noteq> snd_check \<sigma>"
|
||||
|
@ -536,7 +557,6 @@ doc_class external_specification =
|
|||
|
||||
doc_class SYSREQS = external_specification +
|
||||
phase :: "phase" <= "SYSDEV_ext"
|
||||
(*accepts "\<lbrace>objectives||requirement||cenelec_document\<rbrace>\<^sup>+ "*)
|
||||
type_synonym system_requirements_specification = SYSREQS
|
||||
|
||||
doc_class SYSSREQS = external_specification +
|
||||
|
@ -551,31 +571,69 @@ doc_class SYSS_pl = external_specification +
|
|||
phase :: "phase" <= "SYSDEV_ext"
|
||||
type_synonym system_safety_plan = SYSS_pl
|
||||
|
||||
(* SYS_VnV_pl exists in Figure 3 but not in Figure 4 *)
|
||||
(* SYS_VnV_pl exists in Figure 3 but not in Figure 4: surely a typo in Figure 4 *)
|
||||
doc_class SYS_VnV_pl = external_specification +
|
||||
phase :: "phase" <= "SYSDEV_ext"
|
||||
type_synonym system_VnV_plan = SYS_VnV_pl
|
||||
|
||||
doc_class SQAP = cenelec_document +
|
||||
phase :: "phase" <= "SPl"
|
||||
nlvl :: "normative_level" <= "HR"
|
||||
invariant force_nlvl_sqap :: "nlvl \<sigma> = HR"
|
||||
type_synonym software_quality_assurance_plan = SQAP
|
||||
|
||||
doc_class SQAVR = cenelec_document +
|
||||
phase :: "phase" <= "SPl"
|
||||
nlvl :: "normative_level" <= "HR"
|
||||
invariant force_nlvl_sqavr :: "nlvl \<sigma> = HR"
|
||||
type_synonym software_quality_assurance_verfication_report = SQAVR
|
||||
|
||||
doc_class SCMP = cenelec_document +
|
||||
phase :: "phase" <= "SPl"
|
||||
nlvl :: "normative_level" <= "HR"
|
||||
invariant force_nlvl_scmp :: "nlvl \<sigma> = HR"
|
||||
type_synonym software_configuration_management_plan = SCMP
|
||||
|
||||
doc_class SVP = cenelec_document +
|
||||
phase :: "phase" <= "SPl"
|
||||
nlvl :: "normative_level" <= "HR"
|
||||
invariant force_nlvl_svp :: "nlvl \<sigma> = HR"
|
||||
type_synonym software_verification_plan = SVP
|
||||
|
||||
doc_class SVAP = cenelec_document +
|
||||
phase :: "phase" <= "SPl"
|
||||
nlvl :: "normative_level" <= "HR"
|
||||
invariant force_nlvl_svap :: "nlvl \<sigma> = HR"
|
||||
type_synonym software_validation_plan = SVAP
|
||||
|
||||
doc_class SWRS = cenelec_document +
|
||||
phase :: "phase" <= "SR"
|
||||
type_synonym software_requirements_specification = SWRS
|
||||
phase :: "phase" <= "SR"
|
||||
nlvl :: "normative_level" <= "HR"
|
||||
invariant force_nlvl_swrs :: "nlvl \<sigma> = HR"
|
||||
type_synonym software_requirements_specification = SWRS
|
||||
|
||||
doc_class OSWTS = cenelec_document +
|
||||
phase :: "phase" <= "SR"
|
||||
nlvl :: "normative_level" <= "HR"
|
||||
invariant force_nlvl_oswts :: "nlvl \<sigma> = HR"
|
||||
type_synonym overall_software_test_specification = OSWTS
|
||||
|
||||
doc_class SWRVR = cenelec_document +
|
||||
phase :: "phase" <= "SR"
|
||||
type_synonym software_requirements_verification_report = SWRVR
|
||||
|
||||
|
||||
doc_class SWTS = cenelec_document +
|
||||
phase :: "phase" <= "SR"
|
||||
type_synonym software_test_specification = SWTS
|
||||
|
||||
phase :: "phase" <= "SR"
|
||||
nlvl :: "normative_level" <= "HR"
|
||||
invariant force_nlvl_swrvr :: "nlvl \<sigma> = HR"
|
||||
type_synonym software_requirements_verification_report = SWRVR
|
||||
|
||||
doc_class SWAS = cenelec_document +
|
||||
phase :: "phase" <= "SADES"
|
||||
nlvl :: "normative_level" <= "HR"
|
||||
invariant force_nlvl_swas :: "nlvl \<sigma> = HR"
|
||||
type_synonym software_architecture_specification = SWAS
|
||||
|
||||
doc_class SWDS = cenelec_document +
|
||||
phase :: "phase" <= "SADES"
|
||||
phase :: "phase" <= "SADES"
|
||||
nlvl :: "normative_level" <= "HR"
|
||||
invariant force_nlvl_swds :: "nlvl \<sigma> = HR"
|
||||
type_synonym software_design_specification = SWDS
|
||||
|
||||
doc_class SWIS_E =
|
||||
|
@ -591,74 +649,394 @@ doc_class SWIS_E =
|
|||
|
||||
doc_class SWIS = cenelec_document +
|
||||
phase :: "phase" <= "SADES"
|
||||
nlvl :: "normative_level" <= "HR"
|
||||
written_by :: "role option" <= "Some DES"
|
||||
fst_check :: "role option" <= "Some VER"
|
||||
snd_check :: "role option" <= "Some VAL"
|
||||
components :: "SWIS_E list"
|
||||
type_synonym software_interfaces_specification = SWIS
|
||||
invariant force_nlvl_swis :: "nlvl \<sigma> = HR"
|
||||
type_synonym software_interface_specifications = SWIS
|
||||
|
||||
doc_class SWITS = cenelec_document +
|
||||
phase :: "phase" <= "SADES"
|
||||
nlvl :: "normative_level" <= "HR"
|
||||
invariant force_nlvl_swits :: "nlvl \<sigma> = HR"
|
||||
type_synonym software_integration_test_specification = SWITS
|
||||
|
||||
doc_class SWHITS = cenelec_document +
|
||||
phase :: "phase" <= "SADES"
|
||||
nlvl :: "normative_level" <= "HR"
|
||||
invariant force_nlvl_swhits :: "nlvl \<sigma> = HR"
|
||||
type_synonym software_hardware_integration_test_specification = SWHITS
|
||||
|
||||
doc_class SWADVR = cenelec_document +
|
||||
phase :: "phase" <= "SADES"
|
||||
phase :: "phase" <= "SADES"
|
||||
nlvl :: "normative_level" <= "HR"
|
||||
invariant force_nlvl_swadvr :: "nlvl \<sigma> = HR"
|
||||
type_synonym software_architecture_and_design_verification_report = SWADVR
|
||||
|
||||
doc_class SWCDS = cenelec_document +
|
||||
phase :: "phase" <= "SCDES"
|
||||
phase :: "phase" <= "SCDES"
|
||||
invariant force_nlvl_swcds :: "if sil \<sigma> = SIL0 then nlvl \<sigma> = R else nlvl \<sigma> = HR"
|
||||
type_synonym software_component_design_specification = SWCDS
|
||||
|
||||
doc_class SWCTS = cenelec_document +
|
||||
phase :: "phase" <= "SCDES"
|
||||
phase :: "phase" <= "SCDES"
|
||||
invariant force_nlvl_swcts :: "if sil \<sigma> = SIL0 then nlvl \<sigma> = R else nlvl \<sigma> = HR"
|
||||
type_synonym software_component_test_specification = SWCTS
|
||||
|
||||
doc_class SWCDVR = cenelec_document +
|
||||
phase :: "phase" <= "SCDES"
|
||||
phase :: "phase" <= "SCDES"
|
||||
invariant force_nlvl_swcdvr :: "if sil \<sigma> = SIL0 then nlvl \<sigma> = R else nlvl \<sigma> = HR"
|
||||
type_synonym software_component_design_verification_report = SWCDVR
|
||||
|
||||
|
||||
doc_class SWSCD = cenelec_document +
|
||||
phase :: "phase" <= "CInT"
|
||||
phase :: "phase" <= "CInT"
|
||||
nlvl :: "normative_level" <= "HR"
|
||||
invariant force_nlvl_swscd :: "nlvl \<sigma> = HR"
|
||||
type_synonym software_source_code_and_documentation = SWSCD
|
||||
|
||||
doc_class SWCTR = cenelec_document +
|
||||
phase :: "phase" <= "CInT"
|
||||
phase :: "phase" <= "CInT"
|
||||
invariant force_nlvl_swctr :: "if sil \<sigma> = SIL0 then nlvl \<sigma> = R else nlvl \<sigma> = HR"
|
||||
type_synonym software_component_test_report = SWCTR
|
||||
|
||||
doc_class SWSCVR = cenelec_document +
|
||||
phase :: "phase" <= "CInT"
|
||||
phase :: "phase" <= "CInT"
|
||||
nlvl :: "normative_level" <= "HR"
|
||||
invariant force_nlvl_swscvr :: "nlvl \<sigma> = HR"
|
||||
type_synonym software_source_code_verification_report = SWSCVR
|
||||
|
||||
doc_class SWITR = cenelec_document +
|
||||
phase :: "phase" <= "SI"
|
||||
nlvl :: "normative_level" <= "HR"
|
||||
invariant force_nlvl_switr :: "nlvl \<sigma> = HR"
|
||||
type_synonym software_integration_test_report = SWITR
|
||||
|
||||
doc_class SWHAITR = cenelec_document +
|
||||
phase :: "phase" <= "SI"
|
||||
phase :: "phase" <= "SI"
|
||||
nlvl :: "normative_level" <= "HR"
|
||||
invariant force_nlvl_swhaitr :: "nlvl \<sigma> = HR"
|
||||
type_synonym software_hardware_integration_test_report = SWHAITR
|
||||
|
||||
doc_class SWIVR = cenelec_document +
|
||||
phase :: "phase" <= "SI"
|
||||
nlvl :: "normative_level" <= "HR"
|
||||
invariant force_nlvl_swivr :: "nlvl \<sigma> = HR"
|
||||
type_synonym software_integration_verification_report = SWIVR
|
||||
|
||||
doc_class SWTR_global = cenelec_document +
|
||||
phase :: "phase" <= "SV"
|
||||
type_synonym overall_software_test_report = SWTR_global
|
||||
doc_class OSWTR = cenelec_document +
|
||||
phase :: "phase" <= "SV"
|
||||
nlvl :: "normative_level" <= "HR"
|
||||
invariant force_nlvl_oswtr :: "nlvl \<sigma> = HR"
|
||||
type_synonym overall_software_test_report = OSWTR
|
||||
|
||||
doc_class SWVALR = cenelec_document +
|
||||
phase :: "phase" <= "SV"
|
||||
nlvl :: "normative_level" <= "HR"
|
||||
invariant force_nlvl_swvalr :: "nlvl \<sigma> = HR"
|
||||
type_synonym software_validation_report = SWVALR
|
||||
|
||||
doc_class SWDD = cenelec_document +
|
||||
phase :: "phase" <= "SD"
|
||||
type_synonym software_deployment_documents = SWDD
|
||||
doc_class TVALR = cenelec_document +
|
||||
phase :: "phase" <= "SV"
|
||||
invariant force_nlvl_tvalr :: "if sil \<sigma> = SIL0 then nlvl \<sigma> = R else nlvl \<sigma> = HR"
|
||||
type_synonym tools_validation_report = TVALR
|
||||
|
||||
doc_class SWMD = cenelec_document +
|
||||
phase :: "phase" <= "SM"
|
||||
type_synonym software_maintenance_documents = SWMD
|
||||
doc_class SWVRN = cenelec_document +
|
||||
phase :: "phase" <= "SV"
|
||||
nlvl :: "normative_level" <= "HR"
|
||||
invariant force_nlvl_swvrn :: "nlvl \<sigma> = HR"
|
||||
type_synonym software_validation_release_note = SWVRN
|
||||
|
||||
doc_class ARS = cenelec_document +
|
||||
phase :: "phase" <= "SCADA"
|
||||
nlvl :: "normative_level" <= "HR"
|
||||
invariant force_nlvl_ars :: "nlvl \<sigma> = HR"
|
||||
type_synonym application_requirements_specification = ARS
|
||||
|
||||
doc_class APP = cenelec_document +
|
||||
phase :: "phase" <= "SCADA"
|
||||
nlvl :: "normative_level" <= "HR"
|
||||
invariant force_nlvl_APP :: "nlvl \<sigma> = HR"
|
||||
type_synonym application_preparation_plan = APP
|
||||
|
||||
doc_class ATS = cenelec_document +
|
||||
phase :: "phase" <= "SCADA"
|
||||
nlvl :: "normative_level" <= "HR"
|
||||
invariant force_nlvl_ats :: "nlvl \<sigma> = HR"
|
||||
type_synonym application_test_specification = ATS
|
||||
|
||||
doc_class AAD = cenelec_document +
|
||||
phase :: "phase" <= "SCADA"
|
||||
nlvl :: "normative_level" <= "HR"
|
||||
invariant force_nlvl_aad :: "nlvl \<sigma> = HR"
|
||||
type_synonym application_architecture_design = AAD
|
||||
|
||||
doc_class APVR = cenelec_document +
|
||||
phase :: "phase" <= "SCADA"
|
||||
nlvl :: "normative_level" <= "HR"
|
||||
invariant force_nlvl_apvr :: "nlvl \<sigma> = HR"
|
||||
type_synonym application_preparation_verification_report = APVR
|
||||
|
||||
doc_class ATR = cenelec_document +
|
||||
phase :: "phase" <= "SCADA"
|
||||
nlvl :: "normative_level" <= "HR"
|
||||
invariant force_nlvl_atr :: "nlvl \<sigma> = HR"
|
||||
type_synonym application_test_report= ATR
|
||||
|
||||
doc_class SOCOADA = cenelec_document +
|
||||
phase :: "phase" <= "SCADA"
|
||||
nlvl :: "normative_level" <= "HR"
|
||||
invariant force_nlvl_socoada :: "nlvl \<sigma> = HR"
|
||||
type_synonym source_code_application_data_algorithms = SOCOADA
|
||||
|
||||
doc_class ADAVR = cenelec_document +
|
||||
phase :: "phase" <= "SCADA"
|
||||
nlvl :: "normative_level" <= "HR"
|
||||
invariant force_nlvl_adavr :: "nlvl \<sigma> = HR"
|
||||
type_synonym application_data_algorithms_verification_report= ADAVR
|
||||
|
||||
doc_class SWRDP = cenelec_document +
|
||||
phase :: "phase" <= "SD"
|
||||
invariant force_nlvl_swrdp :: "if sil \<sigma> = SIL0 then nlvl \<sigma> = R else nlvl \<sigma> = HR"
|
||||
type_synonym software_release_deployment_plan = SWRDP
|
||||
|
||||
doc_class SWDM = cenelec_document +
|
||||
phase :: "phase" <= "SD"
|
||||
invariant force_nlvl_swdm :: "if sil \<sigma> = SIL0 then nlvl \<sigma> = R else nlvl \<sigma> = HR"
|
||||
type_synonym software_deployment_manual = SWDM
|
||||
|
||||
doc_class SWDRN = cenelec_document +
|
||||
phase :: "phase" <= "SD"
|
||||
nlvl :: "normative_level" <= "HR"
|
||||
invariant force_nlvl_swdrn :: "nlvl \<sigma> = HR"
|
||||
type_synonym software_deployment_release_notes = SWDRN
|
||||
|
||||
doc_class SWDR = cenelec_document +
|
||||
phase :: "phase" <= "SD"
|
||||
invariant force_nlvl_swdr :: "if sil \<sigma> = SIL0 then nlvl \<sigma> = R else nlvl \<sigma> = HR"
|
||||
type_synonym software_deployment_records = SWDR
|
||||
|
||||
doc_class SWDVR = cenelec_document +
|
||||
phase :: "phase" <= "SD"
|
||||
invariant force_nlvl_swdvr :: "if sil \<sigma> = SIL0 then nlvl \<sigma> = R else nlvl \<sigma> = HR"
|
||||
type_synonym software_deployment_verification_report = SWDVR
|
||||
|
||||
doc_class SWMP = cenelec_document +
|
||||
phase :: "phase" <= "SM"
|
||||
invariant force_nlvl_swmp :: "if sil \<sigma> = SIL0 then nlvl \<sigma> = R else nlvl \<sigma> = HR"
|
||||
type_synonym software_maintenance_plan = SWMP
|
||||
|
||||
doc_class SWCR = cenelec_document +
|
||||
phase :: "phase" <= "SM"
|
||||
nlvl :: "normative_level" <= "HR"
|
||||
invariant force_nlvl_swcr :: "nlvl \<sigma> = HR"
|
||||
type_synonym software_change_records = SWCR
|
||||
|
||||
doc_class SWMR = cenelec_document +
|
||||
phase :: "phase" <= "SM"
|
||||
invariant force_nlvl_swmr :: "if sil \<sigma> = SIL0 then nlvl \<sigma> = R else nlvl \<sigma> = HR"
|
||||
type_synonym software_maintenance_records = SWMR
|
||||
|
||||
doc_class SWMVR = cenelec_document +
|
||||
phase :: "phase" <= "SM"
|
||||
invariant force_nlvl_swmvr :: "if sil \<sigma> = SIL0 then nlvl \<sigma> = R else nlvl \<sigma> = HR"
|
||||
type_synonym software_maintenance_verification_report = SWMVR
|
||||
|
||||
doc_class SWAP = cenelec_document +
|
||||
phase :: "phase" <= "SA"
|
||||
invariant force_nlvl_swap :: "if sil \<sigma> = SIL0 then nlvl \<sigma> = R else nlvl \<sigma> = HR"
|
||||
type_synonym software_assessment_plan = SWAP
|
||||
|
||||
doc_class SWAR = cenelec_document +
|
||||
phase :: "phase" <= "SA"
|
||||
invariant force_nlvl_swar :: "if sil \<sigma> = SIL0 then nlvl \<sigma> = R else nlvl \<sigma> = HR"
|
||||
type_synonym software_assessment_report = SWAR
|
||||
|
||||
text\<open>Table A.1: Lifecycle Issues and Documentation (5.3).
|
||||
The requirement levels of table A.1 is expressed with monitor classes:
|
||||
when closing the monitor, the normative level (requirement level in CENELEC lingua)
|
||||
of each CENELEC document instance is checked and warning/errors are triggered
|
||||
if they do not respect the SIL of the monitor class\<close>
|
||||
|
||||
doc_class monitor_SIL =
|
||||
sil :: sil
|
||||
|
||||
doc_class monitor_SIL0 = monitor_SIL +
|
||||
sil :: sil <= SIL0
|
||||
accepts "\<lbrakk>SQAP\<rbrakk> ~~ \<lbrakk>SQAVR\<rbrakk> ~~ \<lbrakk>SCMP\<rbrakk> ~~ \<lbrakk>SVP\<rbrakk> ~~ \<lbrakk>SVAP\<rbrakk>
|
||||
~~ \<lbrakk>SWRS\<rbrakk> ~~ \<lbrakk>OSWTS\<rbrakk> ~~ \<lbrakk>SWRVR\<rbrakk>
|
||||
~~ \<lbrakk>SWAS\<rbrakk> ~~ \<lbrakk>SWDS\<rbrakk> ~~ \<lbrakk>SWIS\<rbrakk> ~~ \<lbrakk>SWITS\<rbrakk> ~~ \<lbrakk>SWHITS\<rbrakk> ~~ \<lbrakk>SWADVR\<rbrakk>
|
||||
~~ \<lbrakk>SWCDS\<rbrakk> ~~ \<lbrakk>SWCTS\<rbrakk> ~~ \<lbrakk>SWCDVR\<rbrakk>
|
||||
~~ \<lbrakk>SWSCD\<rbrakk> ~~ \<lbrakk>SWCTR\<rbrakk> ~~ \<lbrakk>SWSCVR\<rbrakk>
|
||||
~~ \<lbrakk>SWITR\<rbrakk> ~~ \<lbrakk>SWHAITR\<rbrakk> ~~ \<lbrakk>SWIVR\<rbrakk>
|
||||
~~ \<lbrakk>OSWTR\<rbrakk> ~~ \<lbrakk>SWVALR\<rbrakk> ~~ \<lbrakk>TVALR\<rbrakk> ~~ \<lbrakk>SWVRN\<rbrakk>
|
||||
~~ \<lbrakk>ARS\<rbrakk> ~~ \<lbrakk>APP\<rbrakk> ~~ \<lbrakk>ATS\<rbrakk> ~~ \<lbrakk>AAD\<rbrakk> ~~ \<lbrakk>APVR\<rbrakk> ~~ \<lbrakk>ATR\<rbrakk> ~~ \<lbrakk>SOCOADA\<rbrakk> ~~ \<lbrakk>ADAVR\<rbrakk>
|
||||
~~ \<lbrakk>SWRDP\<rbrakk> ~~ \<lbrakk>SWDM\<rbrakk> ~~ \<lbrakk>SWDRN\<rbrakk> ~~ \<lbrakk>SWDR\<rbrakk> ~~ \<lbrakk>SWDVR\<rbrakk>
|
||||
~~ \<lbrakk>SWMP\<rbrakk> ~~ \<lbrakk>SWCR\<rbrakk> ~~ \<lbrakk>SWMR\<rbrakk> ~~ \<lbrakk>SWMVR\<rbrakk>
|
||||
~~ \<lbrakk>SWAP\<rbrakk> ~~ \<lbrakk>SWAR\<rbrakk>"
|
||||
invariant force_sil0 :: "sil \<sigma> = SIL0"
|
||||
|
||||
doc_class monitor_SIL1 = monitor_SIL +
|
||||
sil :: sil <= SIL1
|
||||
accepts "\<lbrakk>SQAP\<rbrakk> ~~ \<lbrakk>SQAVR\<rbrakk> ~~ \<lbrakk>SCMP\<rbrakk> ~~ \<lbrakk>SVP\<rbrakk> ~~ \<lbrakk>SVAP\<rbrakk>
|
||||
~~ \<lbrakk>SWRS\<rbrakk> ~~ \<lbrakk>OSWTS\<rbrakk> ~~ \<lbrakk>SWRVR\<rbrakk>
|
||||
~~ \<lbrakk>SWAS\<rbrakk> ~~ \<lbrakk>SWDS\<rbrakk> ~~ \<lbrakk>SWIS\<rbrakk> ~~ \<lbrakk>SWITS\<rbrakk> ~~ \<lbrakk>SWHITS\<rbrakk> ~~ \<lbrakk>SWADVR\<rbrakk>
|
||||
~~ \<lbrakk>SWCDS\<rbrakk> ~~ \<lbrakk>SWCTS\<rbrakk> ~~ \<lbrakk>SWCDVR\<rbrakk>
|
||||
~~ \<lbrakk>SWSCD\<rbrakk> ~~ \<lbrakk>SWCTR\<rbrakk> ~~ \<lbrakk>SWSCVR\<rbrakk>
|
||||
~~ \<lbrakk>SWITR\<rbrakk> ~~ \<lbrakk>SWHAITR\<rbrakk> ~~ \<lbrakk>SWIVR\<rbrakk>
|
||||
~~ \<lbrakk>OSWTR\<rbrakk> ~~ \<lbrakk>SWVALR\<rbrakk> ~~ \<lbrakk>TVALR\<rbrakk> ~~ \<lbrakk>SWVRN\<rbrakk>
|
||||
~~ \<lbrakk>ARS\<rbrakk> ~~ \<lbrakk>APP\<rbrakk> ~~ \<lbrakk>ATS\<rbrakk> ~~ \<lbrakk>AAD\<rbrakk> ~~ \<lbrakk>APVR\<rbrakk> ~~ \<lbrakk>ATR\<rbrakk> ~~ \<lbrakk>SOCOADA\<rbrakk> ~~ \<lbrakk>ADAVR\<rbrakk>
|
||||
~~ \<lbrakk>SWRDP\<rbrakk> ~~ \<lbrakk>SWDM\<rbrakk> ~~ \<lbrakk>SWDRN\<rbrakk> ~~ \<lbrakk>SWDR\<rbrakk> ~~ \<lbrakk>SWDVR\<rbrakk>
|
||||
~~ \<lbrakk>SWMP\<rbrakk> ~~ \<lbrakk>SWCR\<rbrakk> ~~ \<lbrakk>SWMR\<rbrakk> ~~ \<lbrakk>SWMVR\<rbrakk>
|
||||
~~ \<lbrakk>SWAP\<rbrakk> ~~ \<lbrakk>SWAR\<rbrakk>"
|
||||
invariant force_sil1 :: "sil \<sigma> = SIL1"
|
||||
|
||||
doc_class monitor_SIL2 = monitor_SIL +
|
||||
sil :: sil <= SIL2
|
||||
accepts "\<lbrakk>SQAP\<rbrakk> ~~ \<lbrakk>SQAVR\<rbrakk> ~~ \<lbrakk>SCMP\<rbrakk> ~~ \<lbrakk>SVP\<rbrakk> ~~ \<lbrakk>SVAP\<rbrakk>
|
||||
~~ \<lbrakk>SWRS\<rbrakk> ~~ \<lbrakk>OSWTS\<rbrakk> ~~ \<lbrakk>SWRVR\<rbrakk>
|
||||
~~ \<lbrakk>SWAS\<rbrakk> ~~ \<lbrakk>SWDS\<rbrakk> ~~ \<lbrakk>SWIS\<rbrakk> ~~ \<lbrakk>SWITS\<rbrakk> ~~ \<lbrakk>SWHITS\<rbrakk> ~~ \<lbrakk>SWADVR\<rbrakk>
|
||||
~~ \<lbrakk>SWCDS\<rbrakk> ~~ \<lbrakk>SWCTS\<rbrakk> ~~ \<lbrakk>SWCDVR\<rbrakk>
|
||||
~~ \<lbrakk>SWSCD\<rbrakk> ~~ \<lbrakk>SWCTR\<rbrakk> ~~ \<lbrakk>SWSCVR\<rbrakk>
|
||||
~~ \<lbrakk>SWITR\<rbrakk> ~~ \<lbrakk>SWHAITR\<rbrakk> ~~ \<lbrakk>SWIVR\<rbrakk>
|
||||
~~ \<lbrakk>OSWTR\<rbrakk> ~~ \<lbrakk>SWVALR\<rbrakk> ~~ \<lbrakk>TVALR\<rbrakk> ~~ \<lbrakk>SWVRN\<rbrakk>
|
||||
~~ \<lbrakk>ARS\<rbrakk> ~~ \<lbrakk>APP\<rbrakk> ~~ \<lbrakk>ATS\<rbrakk> ~~ \<lbrakk>AAD\<rbrakk> ~~ \<lbrakk>APVR\<rbrakk> ~~ \<lbrakk>ATR\<rbrakk> ~~ \<lbrakk>SOCOADA\<rbrakk> ~~ \<lbrakk>ADAVR\<rbrakk>
|
||||
~~ \<lbrakk>SWRDP\<rbrakk> ~~ \<lbrakk>SWDM\<rbrakk> ~~ \<lbrakk>SWDRN\<rbrakk> ~~ \<lbrakk>SWDR\<rbrakk> ~~ \<lbrakk>SWDVR\<rbrakk>
|
||||
~~ \<lbrakk>SWMP\<rbrakk> ~~ \<lbrakk>SWCR\<rbrakk> ~~ \<lbrakk>SWMR\<rbrakk> ~~ \<lbrakk>SWMVR\<rbrakk>
|
||||
~~ \<lbrakk>SWAP\<rbrakk> ~~ \<lbrakk>SWAR\<rbrakk>"
|
||||
invariant force_sil2 :: "sil \<sigma> = SIL2"
|
||||
|
||||
doc_class monitor_SIL3 = monitor_SIL +
|
||||
sil :: sil <= SIL3
|
||||
accepts "\<lbrakk>SQAP\<rbrakk> ~~ \<lbrakk>SQAVR\<rbrakk> ~~ \<lbrakk>SCMP\<rbrakk> ~~ \<lbrakk>SVP\<rbrakk> ~~ \<lbrakk>SVAP\<rbrakk>
|
||||
~~ \<lbrakk>SWRS\<rbrakk> ~~ \<lbrakk>OSWTS\<rbrakk> ~~ \<lbrakk>SWRVR\<rbrakk>
|
||||
~~ \<lbrakk>SWAS\<rbrakk> ~~ \<lbrakk>SWDS\<rbrakk> ~~ \<lbrakk>SWIS\<rbrakk> ~~ \<lbrakk>SWITS\<rbrakk> ~~ \<lbrakk>SWHITS\<rbrakk> ~~ \<lbrakk>SWADVR\<rbrakk>
|
||||
~~ \<lbrakk>SWCDS\<rbrakk> ~~ \<lbrakk>SWCTS\<rbrakk> ~~ \<lbrakk>SWCDVR\<rbrakk>
|
||||
~~ \<lbrakk>SWSCD\<rbrakk> ~~ \<lbrakk>SWCTR\<rbrakk> ~~ \<lbrakk>SWSCVR\<rbrakk>
|
||||
~~ \<lbrakk>SWITR\<rbrakk> ~~ \<lbrakk>SWHAITR\<rbrakk> ~~ \<lbrakk>SWIVR\<rbrakk>
|
||||
~~ \<lbrakk>OSWTR\<rbrakk> ~~ \<lbrakk>SWVALR\<rbrakk> ~~ \<lbrakk>TVALR\<rbrakk> ~~ \<lbrakk>SWVRN\<rbrakk>
|
||||
~~ \<lbrakk>ARS\<rbrakk> ~~ \<lbrakk>APP\<rbrakk> ~~ \<lbrakk>ATS\<rbrakk> ~~ \<lbrakk>AAD\<rbrakk> ~~ \<lbrakk>APVR\<rbrakk> ~~ \<lbrakk>ATR\<rbrakk> ~~ \<lbrakk>SOCOADA\<rbrakk> ~~ \<lbrakk>ADAVR\<rbrakk>
|
||||
~~ \<lbrakk>SWRDP\<rbrakk> ~~ \<lbrakk>SWDM\<rbrakk> ~~ \<lbrakk>SWDRN\<rbrakk> ~~ \<lbrakk>SWDR\<rbrakk> ~~ \<lbrakk>SWDVR\<rbrakk>
|
||||
~~ \<lbrakk>SWMP\<rbrakk> ~~ \<lbrakk>SWCR\<rbrakk> ~~ \<lbrakk>SWMR\<rbrakk> ~~ \<lbrakk>SWMVR\<rbrakk>
|
||||
~~ \<lbrakk>SWAP\<rbrakk> ~~ \<lbrakk>SWAR\<rbrakk>"
|
||||
invariant force_sil3 :: "sil \<sigma> = SIL3"
|
||||
|
||||
doc_class monitor_SIL4 = monitor_SIL +
|
||||
sil :: sil <= SIL4
|
||||
accepts "\<lbrakk>SQAP\<rbrakk> ~~ \<lbrakk>SQAVR\<rbrakk> ~~ \<lbrakk>SCMP\<rbrakk> ~~ \<lbrakk>SVP\<rbrakk> ~~ \<lbrakk>SVAP\<rbrakk>
|
||||
~~ \<lbrakk>SWRS\<rbrakk> ~~ \<lbrakk>OSWTS\<rbrakk> ~~ \<lbrakk>SWRVR\<rbrakk>
|
||||
~~ \<lbrakk>SWAS\<rbrakk> ~~ \<lbrakk>SWDS\<rbrakk> ~~ \<lbrakk>SWIS\<rbrakk> ~~ \<lbrakk>SWITS\<rbrakk> ~~ \<lbrakk>SWHITS\<rbrakk> ~~ \<lbrakk>SWADVR\<rbrakk>
|
||||
~~ \<lbrakk>SWCDS\<rbrakk> ~~ \<lbrakk>SWCTS\<rbrakk> ~~ \<lbrakk>SWCDVR\<rbrakk>
|
||||
~~ \<lbrakk>SWSCD\<rbrakk> ~~ \<lbrakk>SWCTR\<rbrakk> ~~ \<lbrakk>SWSCVR\<rbrakk>
|
||||
~~ \<lbrakk>SWITR\<rbrakk> ~~ \<lbrakk>SWHAITR\<rbrakk> ~~ \<lbrakk>SWIVR\<rbrakk>
|
||||
~~ \<lbrakk>OSWTR\<rbrakk> ~~ \<lbrakk>SWVALR\<rbrakk> ~~ \<lbrakk>TVALR\<rbrakk> ~~ \<lbrakk>SWVRN\<rbrakk>
|
||||
~~ \<lbrakk>ARS\<rbrakk> ~~ \<lbrakk>APP\<rbrakk> ~~ \<lbrakk>ATS\<rbrakk> ~~ \<lbrakk>AAD\<rbrakk> ~~ \<lbrakk>APVR\<rbrakk> ~~ \<lbrakk>ATR\<rbrakk> ~~ \<lbrakk>SOCOADA\<rbrakk> ~~ \<lbrakk>ADAVR\<rbrakk>
|
||||
~~ \<lbrakk>SWRDP\<rbrakk> ~~ \<lbrakk>SWDM\<rbrakk> ~~ \<lbrakk>SWDRN\<rbrakk> ~~ \<lbrakk>SWDR\<rbrakk> ~~ \<lbrakk>SWDVR\<rbrakk>
|
||||
~~ \<lbrakk>SWMP\<rbrakk> ~~ \<lbrakk>SWCR\<rbrakk> ~~ \<lbrakk>SWMR\<rbrakk> ~~ \<lbrakk>SWMVR\<rbrakk>
|
||||
~~ \<lbrakk>SWAP\<rbrakk> ~~ \<lbrakk>SWAR\<rbrakk>"
|
||||
invariant force_sil4 :: "sil \<sigma> = SIL4"
|
||||
|
||||
ML\<open>
|
||||
fun check_sil oid _ ctxt =
|
||||
let
|
||||
val ctxt' = Proof_Context.init_global(Context.theory_of ctxt)
|
||||
val monitor_record_value = #value (the (DOF_core.get_object_local oid ctxt'))
|
||||
val Const _ $ _ $ monitor_sil $ _ = monitor_record_value
|
||||
val traces = AttributeAccess.compute_trace_ML ctxt oid \<^here> \<^here>
|
||||
fun check_sil'' [] = true
|
||||
| check_sil'' (x::xs) =
|
||||
let
|
||||
val (_, doc_oid) = x
|
||||
val doc_record_value = #value (the (DOF_core.get_object_local doc_oid ctxt'))
|
||||
val Const _ $ _ $ _ $ _ $ _ $ cenelec_document_ext = doc_record_value
|
||||
val Const _ $ _ $ _ $ doc_sil $ _ $ _ $ _ $ _ $ _ $ _ = cenelec_document_ext
|
||||
in
|
||||
if doc_sil <> monitor_sil
|
||||
then error(doc_oid
|
||||
^ " cenelec document SIL must be: "
|
||||
^ Syntax.string_of_term ctxt' monitor_sil)
|
||||
else check_sil'' xs end
|
||||
in check_sil'' traces end
|
||||
\<close>
|
||||
|
||||
setup\<open>DOF_core.update_class_invariant "CENELEC_50128.monitor_SIL0" check_sil\<close>
|
||||
|
||||
text\<open>
|
||||
A more generic example of check_sil which can be generalized:
|
||||
it is decoupled from the CENELEC current implementation
|
||||
but is much less efficient regarding time computation by relying on Isabelle evaluation mechanism.\<close>
|
||||
ML\<open>
|
||||
fun check_sil_slow oid _ ctxt =
|
||||
let
|
||||
val ctxt' = Proof_Context.init_global(Context.theory_of ctxt)
|
||||
val monitor_record_value = #value (the (DOF_core.get_object_local oid ctxt'))
|
||||
val monitor_cid = #cid (the (DOF_core.get_object_local oid ctxt'))
|
||||
val monitor_sil_typ = (Syntax.read_typ ctxt' monitor_cid) --> @{typ "sil"}
|
||||
val monitor_sil = Value_Command.value ctxt'
|
||||
(Const("CENELEC_50128.monitor_SIL.sil", monitor_sil_typ) $ monitor_record_value)
|
||||
val traces = AttributeAccess.compute_trace_ML ctxt oid \<^here> \<^here>
|
||||
fun check_sil' [] = true
|
||||
| check_sil' (x::xs) =
|
||||
let
|
||||
val (doc_cid, doc_oid) = x
|
||||
val doc_record_value = #value (the (DOF_core.get_object_local doc_oid ctxt'))
|
||||
val doc_sil_typ = (Syntax.read_typ ctxt' doc_cid) --> @{typ "sil"}
|
||||
val doc_sil = Value_Command.value ctxt'
|
||||
(Const ("CENELEC_50128.cenelec_document.sil", doc_sil_typ) $ doc_record_value)
|
||||
in
|
||||
if doc_sil <> monitor_sil
|
||||
then error(doc_oid
|
||||
^ " cenelec document SIL must be: "
|
||||
^ Syntax.string_of_term ctxt' monitor_sil)
|
||||
else check_sil' xs end
|
||||
in check_sil' traces end
|
||||
\<close>
|
||||
|
||||
(*setup\<open>DOF_core.update_class_invariant "CENELEC_50128.monitor_SIL0" check_sil_slow\<close>*)
|
||||
|
||||
ML\<open>
|
||||
fun check_required_documents oid _ ctxt =
|
||||
let
|
||||
val ctxt' = Proof_Context.init_global(Context.theory_of ctxt)
|
||||
val {monitor_tab,...} = DOF_core.get_data ctxt'
|
||||
val {accepted_cids, ...} = the (Symtab.lookup monitor_tab oid)
|
||||
val traces = AttributeAccess.compute_trace_ML ctxt oid \<^here> \<^here>
|
||||
fun check_required_documents' [] = true
|
||||
| check_required_documents' (cid::cids) =
|
||||
if exists (fn (doc_cid, _) => equal cid doc_cid) traces
|
||||
then check_required_documents' cids
|
||||
else
|
||||
let
|
||||
val ctxt' = Proof_Context.init_global(Context.theory_of ctxt)
|
||||
val monitor_record_value = #value (the (DOF_core.get_object_local oid ctxt'))
|
||||
val Const _ $ _ $ monitor_sil $ _ = monitor_record_value
|
||||
in error ("A " ^ cid ^ " cenelec document is required with "
|
||||
^ Syntax.string_of_term ctxt' monitor_sil)
|
||||
end
|
||||
in check_required_documents' accepted_cids end
|
||||
\<close>
|
||||
|
||||
setup\<open>DOF_core.update_class_closing_invariant "CENELEC_50128.monitor_SIL0" check_required_documents\<close>
|
||||
|
||||
(* Test pattern matching for the records of the current CENELEC implementation classes,
|
||||
and used by checking functions.
|
||||
If the test failed, then it meams hat the CENELCEC implementation has changed
|
||||
(the class defintions have been updated) and the checking functions must be updated.
|
||||
*)
|
||||
text*[MonitorPatternMatchingTest::monitor_SIL0]\<open>\<close>
|
||||
text*[CenelecClassPatternMatchingTest::SQAP, sil = "SIL0"]\<open>\<close>
|
||||
ML\<open>
|
||||
val thy = @{theory}
|
||||
val monitor_record_value =
|
||||
#value (the (DOF_core.get_object_global "MonitorPatternMatchingTest" thy))
|
||||
val Const _ $ _ $ monitor_sil $ _ = monitor_record_value
|
||||
val doc_record_value = #value (the (DOF_core.get_object_global
|
||||
"CenelecClassPatternMatchingTest" thy))
|
||||
val Const _ $ _ $ _ $ _ $ _ $ cenelec_document_ext = doc_record_value
|
||||
val Const _ $ _ $ _ $ doc_sil $ _ $ _ $ _ $ _ $ _ $ _ = cenelec_document_ext
|
||||
\<close>
|
||||
|
||||
|
||||
section\<open> Software Assurance \<close>
|
||||
\<comment> \<open>MORE TO COME\<close>
|
||||
|
||||
|
@ -671,7 +1049,7 @@ specification to the extent achievable by the selected test coverage.
|
|||
|
||||
text\<open>Outputs:
|
||||
\<^enum> @{typ overall_software_test_report}
|
||||
\<^enum> @{typ software_test_specification} Overall Software Test Specification
|
||||
\<^enum> @{typ overall_software_test_specification} Overall Software Test Specification
|
||||
\<^enum> Overall Software Test Report
|
||||
\<^enum> Software Integration Test Specification
|
||||
\<^enum> Software Integration Test Report
|
||||
|
@ -794,7 +1172,7 @@ doc_class global_documentation_structure = text_element +
|
|||
SYSSREQS ~~ \<comment> \<open>system_safety_requirements_specification\<close>
|
||||
SYSAD ~~ \<comment> \<open>system_architecture description\<close>
|
||||
SYSS_pl ~~ \<comment> \<open>system safety plan\<close>
|
||||
(SWRS || SWTS) " \<comment> \<open>software requirements specification OR
|
||||
(SWRS || OSWTS) " \<comment> \<open>software requirements specification OR
|
||||
overall software test specification\<close>
|
||||
(* MORE TO COME : *)
|
||||
|
||||
|
|
|
@ -0,0 +1,68 @@
|
|||
theory
|
||||
Cenelec_Test
|
||||
imports
|
||||
"Isabelle_DOF.CENELEC_50128"
|
||||
begin
|
||||
|
||||
declare[[strict_monitor_checking = true]]
|
||||
declare[[invariants_checking = true]]
|
||||
declare[[invariants_checking_with_tactics = true]]
|
||||
|
||||
print_doc_items
|
||||
print_doc_classes
|
||||
|
||||
open_monitor*[SIL0Test::monitor_SIL0]
|
||||
|
||||
text*[sqap_intance::SQAP, sil="SIL0", written_by="Some RQM", fst_check="Some VER", snd_check="Some VAL"]\<open>\<close>
|
||||
text*[sqavr_intance::SQAVR, sil= "SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
|
||||
text*[scmp_intance::SCMP, sil="SIL0", written_by="Some CM", fst_check="Some VER", snd_check="Some VAL"]\<open>\<close>
|
||||
text*[svp_intance::SVP, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
|
||||
text*[svap_intance::SVAP, sil="SIL0", written_by="Some VAL", fst_check="Some VER", snd_check="None"]\<open>\<close>
|
||||
text*[swrs_intance::SWRS, sil="SIL0", written_by="Some RQM", fst_check="Some VER", snd_check="Some VAL"]\<open>\<close>
|
||||
text*[oswts_intance::OSWTS, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
|
||||
text*[swrvr_intance::SWRVR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
|
||||
text*[swas_intance::SWAS, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
|
||||
text*[swds_intance::SWDS, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
|
||||
text*[swis_intance::SWIS, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
|
||||
text*[swits_intance::SWITS, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
|
||||
text*[swhits_intance::SWHITS, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
|
||||
text*[swadvr_intance::SWADVR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
|
||||
text*[swcds_intance::SWCDS, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
|
||||
text*[swcts_intance::SWCTS, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
|
||||
text*[swcdvr_intance::SWCDVR, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
|
||||
text*[swscd_intance::SWSCD, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
|
||||
text*[swctr_intance::SWCTR, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
|
||||
text*[swscvr_intance::SWSCVR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
|
||||
text*[switr_intance::SWITR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
|
||||
text*[swhaitr_intance::SWHAITR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
|
||||
text*[swivr_intance::SWIVR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
|
||||
text*[oswtr_intance::OSWTR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
|
||||
text*[swvalr_intance::SWVALR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
|
||||
text*[tvalr_intance::TVALR, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
|
||||
text*[swvrn_intance::SWVRN, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
|
||||
text*[ars_intance::ARS, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
|
||||
text*[app_intance::APP, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
|
||||
text*[ats_intance::ATS, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
|
||||
text*[aad_intance::AAD, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
|
||||
text*[apvr_intance::APVR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
|
||||
text*[atr_intance::ATR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
|
||||
text*[socoada_intance::SOCOADA, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
|
||||
text*[adavr_intance::ADAVR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
|
||||
text*[swrdp_intance::SWRDP, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
|
||||
text*[swdm_intance::SWDM, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
|
||||
text*[swdrn_intance::SWDRN, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
|
||||
text*[swdr_intance::SWDR, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
|
||||
text*[swdvr_intance::SWDVR, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
|
||||
text*[swmp_intance::SWMP, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
|
||||
text*[swcr_intance::SWCR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
|
||||
text*[swmr_intance::SWMR, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
|
||||
text*[swmvr_intance::SWMVR, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
|
||||
text*[swap_intance::SWAP, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
|
||||
text*[swar_intance::SWAR, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
|
||||
|
||||
close_monitor*[SIL0Test]
|
||||
|
||||
declare[[strict_monitor_checking = true]]
|
||||
declare[[invariants_checking = true]]
|
||||
declare[[invariants_checking_with_tactics = true]]
|
||||
|
Loading…
Reference in New Issue