diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index e4a0492..57346ed 100644 --- a/src/DOF/Isa_DOF.thy +++ b/src/DOF/Isa_DOF.thy @@ -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 diff --git a/src/ontologies/CENELEC_50128/CENELEC_50128.thy b/src/ontologies/CENELEC_50128/CENELEC_50128.thy index dd1d3b1..b4a90c8 100644 --- a/src/ontologies/CENELEC_50128/CENELEC_50128.thy +++ b/src/ontologies/CENELEC_50128/CENELEC_50128.thy @@ -281,18 +281,21 @@ chapter\Software Management and Organisation\ text\Representing chapter 5 in @{cite "bsi:50128:2014"}.\ section\Organization, Roles and Responsabilities\ -text\see also section \<^emph>\Software management and organization\.\ +text\See also section \<^emph>\Software management and organization\. and Annex B and C\ -datatype role = PM \ \Program Manager\ - | RQM \ \Requirements Manager\ +text\REQ role in Table C.1 is assumed to be a typo and should be RQM.\ + +datatype role = RQM \ \Requirements Manager\ | DES \ \Designer\ | IMP \ \Implementer\ - | ASR \ \Assessor\ - | INT \ \Integrator\ | TST \ \Tester\ | VER \ \Verifier\ - | VnV \ \Verification and Validation\ + | INT \ \Integrator\ | VAL \ \Validator\ + | ASR \ \Assessor\ + | PM \ \Program Manager\ + | CM \ \Configuration Manager\ + | No_Role_Defined \ \See Annex C footnote a\ @@ -303,20 +306,26 @@ datatype phase = SYSDEV_ext \ \ System Development Phase (externa | SCDES \ \Software Component Design\ | CInT \ \Component Implementation and Testing\ | SI \ \Software Integration\ - | SV \ \Software Validation\ + | SV \ \Overall Software Testing/Final Validation\ + | SCADA \ \Systems Configured by Application Data/Algorithms\ | SD \ \Software Deployment\ | SM \ \Software Maintenance\ + | SA \ \Software Assessment\ +abbreviation software_planning :: "phase" where "software_planning \ SPl" abbreviation software_requirements :: "phase" where "software_requirements \ SR" abbreviation software_architecture_and_design :: "phase" where "software_architecture_and_design \ SADES" abbreviation software_component_design :: "phase" where "software_component_design \ SCDES" abbreviation component_implementation_and_testing :: "phase" - where "component_implementation_and_testing \ CInT" + where "component_implementation_and_testing \ CInT" abbreviation software_integration :: "phase" where "software_integration \ SI" abbreviation software_validation :: "phase" where "software_validation \ SV" +abbreviation systems_configured_application_data_algorithm :: "phase" + where "systems_configured_application_data_algorithm \ SCADA" abbreviation software_deployment :: "phase" where "software_deployment \ SD" abbreviation software_maintenance :: "phase" where "software_maintenance \ SM" +abbreviation software_assessment :: "phase" where "software_assessment \ SM" term "SR" (* meta-test *) @@ -327,8 +336,17 @@ datatype sil = SIL0 | SIL1 | SIL2 | SIL3 | SIL4 type_synonym safety_integration_level = sil +text\Requirement levels specified Annex A: we use the term \<^emph>\normative level\ to distinguish +them from the requirements specified in the standard.\ -doc_class objectives = +datatype normative_level = + M \ \(Mandatory)\ + | HR \ \Highly Recommended\ + | R \ \Recommended\ + | Any \ \No recommendation\ + | NR \ \Not Recommended\ + +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\The following class is a bit unclear about usage and seems to be in -sfcual mismatch with @{typ objectives}: \ +sfcual mismatch with @{typ objective}: \ doc_class SILA = requirement + is_concerned :: "role set" <= "UNIV" alloc :: "sil" <= "SIL0" @@ -520,11 +538,14 @@ section\ Design and Test Documents \ doc_class cenelec_document = text_element + phase :: "phase" - level :: "int option" <= "Some(0)" + sil :: "sil" + level :: "int option" <= "Some(0)" + nlvl :: "normative_level" \ \Annex A Table A.1\ written_by :: "role option" \ \Annex C Table C.1 \ fst_check :: "role option" \ \Annex C Table C.1\ snd_check :: "role option" \ \Annex C Table C.1\ - is_concerned :: "role set" <= "UNIV" + is_concerned :: "role set" <= "UNIV" + accepts "\objective\\<^sup>+||\requirement\\<^sup>+" invariant must_be_chapter :: "text_element.level \ = Some(0)" invariant three_eyes_prcpl:: " written_by \ \ fst_check \ \ written_by \ \ snd_check \" @@ -536,7 +557,6 @@ doc_class external_specification = doc_class SYSREQS = external_specification + phase :: "phase" <= "SYSDEV_ext" - (*accepts "\objectives||requirement||cenelec_document\\<^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 \ = 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 \ = 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 \ = 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 \ = HR" +type_synonym software_verification_plan = SVP + +doc_class SVAP = cenelec_document + + phase :: "phase" <= "SPl" + nlvl :: "normative_level" <= "HR" + invariant force_nlvl_svap :: "nlvl \ = 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 \ = HR" +type_synonym software_requirements_specification = SWRS + +doc_class OSWTS = cenelec_document + + phase :: "phase" <= "SR" + nlvl :: "normative_level" <= "HR" + invariant force_nlvl_oswts :: "nlvl \ = 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 \ = 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 \ = 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 \ = 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 \ = HR" + type_synonym software_interface_specifications = SWIS doc_class SWITS = cenelec_document + phase :: "phase" <= "SADES" + nlvl :: "normative_level" <= "HR" + invariant force_nlvl_swits :: "nlvl \ = 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 \ = 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 \ = 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 \ = SIL0 then nlvl \ = R else nlvl \ = 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 \ = SIL0 then nlvl \ = R else nlvl \ = 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 \ = SIL0 then nlvl \ = R else nlvl \ = 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 \ = 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 \ = SIL0 then nlvl \ = R else nlvl \ = 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 \ = 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 \ = 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 \ = 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 \ = 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 \ = 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 \ = 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 \ = SIL0 then nlvl \ = R else nlvl \ = 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 \ = 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 \ = HR" + type_synonym application_requirements_specification = ARS + +doc_class APP = cenelec_document + + phase :: "phase" <= "SCADA" + nlvl :: "normative_level" <= "HR" + invariant force_nlvl_APP :: "nlvl \ = HR" + type_synonym application_preparation_plan = APP + +doc_class ATS = cenelec_document + + phase :: "phase" <= "SCADA" + nlvl :: "normative_level" <= "HR" + invariant force_nlvl_ats :: "nlvl \ = HR" + type_synonym application_test_specification = ATS + +doc_class AAD = cenelec_document + + phase :: "phase" <= "SCADA" + nlvl :: "normative_level" <= "HR" + invariant force_nlvl_aad :: "nlvl \ = HR" + type_synonym application_architecture_design = AAD + +doc_class APVR = cenelec_document + + phase :: "phase" <= "SCADA" + nlvl :: "normative_level" <= "HR" + invariant force_nlvl_apvr :: "nlvl \ = 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 \ = HR" + type_synonym application_test_report= ATR + +doc_class SOCOADA = cenelec_document + + phase :: "phase" <= "SCADA" + nlvl :: "normative_level" <= "HR" + invariant force_nlvl_socoada :: "nlvl \ = 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 \ = HR" + type_synonym application_data_algorithms_verification_report= ADAVR + +doc_class SWRDP = cenelec_document + + phase :: "phase" <= "SD" + invariant force_nlvl_swrdp :: "if sil \ = SIL0 then nlvl \ = R else nlvl \ = HR" + type_synonym software_release_deployment_plan = SWRDP + +doc_class SWDM = cenelec_document + + phase :: "phase" <= "SD" + invariant force_nlvl_swdm :: "if sil \ = SIL0 then nlvl \ = R else nlvl \ = HR" + type_synonym software_deployment_manual = SWDM + +doc_class SWDRN = cenelec_document + + phase :: "phase" <= "SD" + nlvl :: "normative_level" <= "HR" + invariant force_nlvl_swdrn :: "nlvl \ = HR" + type_synonym software_deployment_release_notes = SWDRN + +doc_class SWDR = cenelec_document + + phase :: "phase" <= "SD" + invariant force_nlvl_swdr :: "if sil \ = SIL0 then nlvl \ = R else nlvl \ = HR" + type_synonym software_deployment_records = SWDR + +doc_class SWDVR = cenelec_document + + phase :: "phase" <= "SD" + invariant force_nlvl_swdvr :: "if sil \ = SIL0 then nlvl \ = R else nlvl \ = HR" + type_synonym software_deployment_verification_report = SWDVR + +doc_class SWMP = cenelec_document + + phase :: "phase" <= "SM" + invariant force_nlvl_swmp :: "if sil \ = SIL0 then nlvl \ = R else nlvl \ = HR" + type_synonym software_maintenance_plan = SWMP + +doc_class SWCR = cenelec_document + + phase :: "phase" <= "SM" + nlvl :: "normative_level" <= "HR" + invariant force_nlvl_swcr :: "nlvl \ = HR" + type_synonym software_change_records = SWCR + +doc_class SWMR = cenelec_document + + phase :: "phase" <= "SM" + invariant force_nlvl_swmr :: "if sil \ = SIL0 then nlvl \ = R else nlvl \ = HR" +type_synonym software_maintenance_records = SWMR + +doc_class SWMVR = cenelec_document + + phase :: "phase" <= "SM" + invariant force_nlvl_swmvr :: "if sil \ = SIL0 then nlvl \ = R else nlvl \ = HR" + type_synonym software_maintenance_verification_report = SWMVR + +doc_class SWAP = cenelec_document + + phase :: "phase" <= "SA" + invariant force_nlvl_swap :: "if sil \ = SIL0 then nlvl \ = R else nlvl \ = HR" + type_synonym software_assessment_plan = SWAP + +doc_class SWAR = cenelec_document + + phase :: "phase" <= "SA" + invariant force_nlvl_swar :: "if sil \ = SIL0 then nlvl \ = R else nlvl \ = HR" + type_synonym software_assessment_report = SWAR + +text\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\ + +doc_class monitor_SIL = + sil :: sil + +doc_class monitor_SIL0 = monitor_SIL + + sil :: sil <= SIL0 + accepts "\SQAP\ ~~ \SQAVR\ ~~ \SCMP\ ~~ \SVP\ ~~ \SVAP\ + ~~ \SWRS\ ~~ \OSWTS\ ~~ \SWRVR\ + ~~ \SWAS\ ~~ \SWDS\ ~~ \SWIS\ ~~ \SWITS\ ~~ \SWHITS\ ~~ \SWADVR\ + ~~ \SWCDS\ ~~ \SWCTS\ ~~ \SWCDVR\ + ~~ \SWSCD\ ~~ \SWCTR\ ~~ \SWSCVR\ + ~~ \SWITR\ ~~ \SWHAITR\ ~~ \SWIVR\ + ~~ \OSWTR\ ~~ \SWVALR\ ~~ \TVALR\ ~~ \SWVRN\ + ~~ \ARS\ ~~ \APP\ ~~ \ATS\ ~~ \AAD\ ~~ \APVR\ ~~ \ATR\ ~~ \SOCOADA\ ~~ \ADAVR\ + ~~ \SWRDP\ ~~ \SWDM\ ~~ \SWDRN\ ~~ \SWDR\ ~~ \SWDVR\ + ~~ \SWMP\ ~~ \SWCR\ ~~ \SWMR\ ~~ \SWMVR\ + ~~ \SWAP\ ~~ \SWAR\" + invariant force_sil0 :: "sil \ = SIL0" + +doc_class monitor_SIL1 = monitor_SIL + + sil :: sil <= SIL1 + accepts "\SQAP\ ~~ \SQAVR\ ~~ \SCMP\ ~~ \SVP\ ~~ \SVAP\ + ~~ \SWRS\ ~~ \OSWTS\ ~~ \SWRVR\ + ~~ \SWAS\ ~~ \SWDS\ ~~ \SWIS\ ~~ \SWITS\ ~~ \SWHITS\ ~~ \SWADVR\ + ~~ \SWCDS\ ~~ \SWCTS\ ~~ \SWCDVR\ + ~~ \SWSCD\ ~~ \SWCTR\ ~~ \SWSCVR\ + ~~ \SWITR\ ~~ \SWHAITR\ ~~ \SWIVR\ + ~~ \OSWTR\ ~~ \SWVALR\ ~~ \TVALR\ ~~ \SWVRN\ + ~~ \ARS\ ~~ \APP\ ~~ \ATS\ ~~ \AAD\ ~~ \APVR\ ~~ \ATR\ ~~ \SOCOADA\ ~~ \ADAVR\ + ~~ \SWRDP\ ~~ \SWDM\ ~~ \SWDRN\ ~~ \SWDR\ ~~ \SWDVR\ + ~~ \SWMP\ ~~ \SWCR\ ~~ \SWMR\ ~~ \SWMVR\ + ~~ \SWAP\ ~~ \SWAR\" + invariant force_sil1 :: "sil \ = SIL1" + +doc_class monitor_SIL2 = monitor_SIL + + sil :: sil <= SIL2 + accepts "\SQAP\ ~~ \SQAVR\ ~~ \SCMP\ ~~ \SVP\ ~~ \SVAP\ + ~~ \SWRS\ ~~ \OSWTS\ ~~ \SWRVR\ + ~~ \SWAS\ ~~ \SWDS\ ~~ \SWIS\ ~~ \SWITS\ ~~ \SWHITS\ ~~ \SWADVR\ + ~~ \SWCDS\ ~~ \SWCTS\ ~~ \SWCDVR\ + ~~ \SWSCD\ ~~ \SWCTR\ ~~ \SWSCVR\ + ~~ \SWITR\ ~~ \SWHAITR\ ~~ \SWIVR\ + ~~ \OSWTR\ ~~ \SWVALR\ ~~ \TVALR\ ~~ \SWVRN\ + ~~ \ARS\ ~~ \APP\ ~~ \ATS\ ~~ \AAD\ ~~ \APVR\ ~~ \ATR\ ~~ \SOCOADA\ ~~ \ADAVR\ + ~~ \SWRDP\ ~~ \SWDM\ ~~ \SWDRN\ ~~ \SWDR\ ~~ \SWDVR\ + ~~ \SWMP\ ~~ \SWCR\ ~~ \SWMR\ ~~ \SWMVR\ + ~~ \SWAP\ ~~ \SWAR\" + invariant force_sil2 :: "sil \ = SIL2" + +doc_class monitor_SIL3 = monitor_SIL + + sil :: sil <= SIL3 + accepts "\SQAP\ ~~ \SQAVR\ ~~ \SCMP\ ~~ \SVP\ ~~ \SVAP\ + ~~ \SWRS\ ~~ \OSWTS\ ~~ \SWRVR\ + ~~ \SWAS\ ~~ \SWDS\ ~~ \SWIS\ ~~ \SWITS\ ~~ \SWHITS\ ~~ \SWADVR\ + ~~ \SWCDS\ ~~ \SWCTS\ ~~ \SWCDVR\ + ~~ \SWSCD\ ~~ \SWCTR\ ~~ \SWSCVR\ + ~~ \SWITR\ ~~ \SWHAITR\ ~~ \SWIVR\ + ~~ \OSWTR\ ~~ \SWVALR\ ~~ \TVALR\ ~~ \SWVRN\ + ~~ \ARS\ ~~ \APP\ ~~ \ATS\ ~~ \AAD\ ~~ \APVR\ ~~ \ATR\ ~~ \SOCOADA\ ~~ \ADAVR\ + ~~ \SWRDP\ ~~ \SWDM\ ~~ \SWDRN\ ~~ \SWDR\ ~~ \SWDVR\ + ~~ \SWMP\ ~~ \SWCR\ ~~ \SWMR\ ~~ \SWMVR\ + ~~ \SWAP\ ~~ \SWAR\" + invariant force_sil3 :: "sil \ = SIL3" + +doc_class monitor_SIL4 = monitor_SIL + + sil :: sil <= SIL4 + accepts "\SQAP\ ~~ \SQAVR\ ~~ \SCMP\ ~~ \SVP\ ~~ \SVAP\ + ~~ \SWRS\ ~~ \OSWTS\ ~~ \SWRVR\ + ~~ \SWAS\ ~~ \SWDS\ ~~ \SWIS\ ~~ \SWITS\ ~~ \SWHITS\ ~~ \SWADVR\ + ~~ \SWCDS\ ~~ \SWCTS\ ~~ \SWCDVR\ + ~~ \SWSCD\ ~~ \SWCTR\ ~~ \SWSCVR\ + ~~ \SWITR\ ~~ \SWHAITR\ ~~ \SWIVR\ + ~~ \OSWTR\ ~~ \SWVALR\ ~~ \TVALR\ ~~ \SWVRN\ + ~~ \ARS\ ~~ \APP\ ~~ \ATS\ ~~ \AAD\ ~~ \APVR\ ~~ \ATR\ ~~ \SOCOADA\ ~~ \ADAVR\ + ~~ \SWRDP\ ~~ \SWDM\ ~~ \SWDRN\ ~~ \SWDR\ ~~ \SWDVR\ + ~~ \SWMP\ ~~ \SWCR\ ~~ \SWMR\ ~~ \SWMVR\ + ~~ \SWAP\ ~~ \SWAR\" + invariant force_sil4 :: "sil \ = SIL4" + +ML\ +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 +\ + +setup\DOF_core.update_class_invariant "CENELEC_50128.monitor_SIL0" check_sil\ + +text\ +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.\ +ML\ +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 +\ + +(*setup\DOF_core.update_class_invariant "CENELEC_50128.monitor_SIL0" check_sil_slow\*) + +ML\ +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 +\ + +setup\DOF_core.update_class_closing_invariant "CENELEC_50128.monitor_SIL0" check_required_documents\ + +(* 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]\\ +text*[CenelecClassPatternMatchingTest::SQAP, sil = "SIL0"]\\ +ML\ +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 +\ - section\ Software Assurance \ \ \MORE TO COME\ @@ -671,7 +1049,7 @@ specification to the extent achievable by the selected test coverage. text\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 ~~ \ \system_safety_requirements_specification\ SYSAD ~~ \ \system_architecture description\ SYSS_pl ~~ \ \system safety plan\ - (SWRS || SWTS) " \ \software requirements specification OR + (SWRS || OSWTS) " \ \software requirements specification OR overall software test specification\ (* MORE TO COME : *) diff --git a/src/tests/Cenelec_Test.thy b/src/tests/Cenelec_Test.thy new file mode 100644 index 0000000..4b1473a --- /dev/null +++ b/src/tests/Cenelec_Test.thy @@ -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"]\\ +text*[sqavr_intance::SQAVR, sil= "SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[scmp_intance::SCMP, sil="SIL0", written_by="Some CM", fst_check="Some VER", snd_check="Some VAL"]\\ +text*[svp_intance::SVP, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[svap_intance::SVAP, sil="SIL0", written_by="Some VAL", fst_check="Some VER", snd_check="None"]\\ +text*[swrs_intance::SWRS, sil="SIL0", written_by="Some RQM", fst_check="Some VER", snd_check="Some VAL"]\\ +text*[oswts_intance::OSWTS, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swrvr_intance::SWRVR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swas_intance::SWAS, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swds_intance::SWDS, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swis_intance::SWIS, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swits_intance::SWITS, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swhits_intance::SWHITS, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swadvr_intance::SWADVR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swcds_intance::SWCDS, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swcts_intance::SWCTS, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swcdvr_intance::SWCDVR, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swscd_intance::SWSCD, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swctr_intance::SWCTR, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swscvr_intance::SWSCVR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[switr_intance::SWITR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swhaitr_intance::SWHAITR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swivr_intance::SWIVR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[oswtr_intance::OSWTR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swvalr_intance::SWVALR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[tvalr_intance::TVALR, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swvrn_intance::SWVRN, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[ars_intance::ARS, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[app_intance::APP, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[ats_intance::ATS, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[aad_intance::AAD, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[apvr_intance::APVR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[atr_intance::ATR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[socoada_intance::SOCOADA, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[adavr_intance::ADAVR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swrdp_intance::SWRDP, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swdm_intance::SWDM, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swdrn_intance::SWDRN, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swdr_intance::SWDR, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swdvr_intance::SWDVR, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swmp_intance::SWMP, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swcr_intance::SWCR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swmr_intance::SWMR, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swmvr_intance::SWMVR, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swap_intance::SWAP, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swar_intance::SWAR, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ + +close_monitor*[SIL0Test] + +declare[[strict_monitor_checking = true]] +declare[[invariants_checking = true]] +declare[[invariants_checking_with_tactics = true]] +