diff --git a/src/ontologies/CENELEC_50128/CENELEC_50128.thy b/src/ontologies/CENELEC_50128/CENELEC_50128.thy index a603332..50f3630 100644 --- a/src/ontologies/CENELEC_50128/CENELEC_50128.thy +++ b/src/ontologies/CENELEC_50128/CENELEC_50128.thy @@ -272,34 +272,36 @@ NOTE Verification is mostly based on document reviews (design, implementation, t Definition*[verifier, short_name="''verifier''"] \entity that is responsible for one or more verification activities\ +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\.\ -datatype role = PM (* Program Manager *) - | RQM (* Requirements Manager *) - | DES (* Designer *) - | IMP (* Implementer *) - | ASR (* Assessor *) - | INT (* Integrator *) - | TST (* Tester *) - | VER (* Verifier *) - | VnV (* Verification and Validation *) - | VAL (* Validator *) +datatype role = PM \ \Program Manager\ + | RQM \ \Requirements Manager\ + | DES \ \Designer\ + | IMP \ \Implementer\ + | ASR \ \Assessor\ + | INT \ \Integrator\ + | TST \ \Tester\ + | VER \ \Verifier\ + | VnV \ \Verification and Validation\ + | VAL \ \Validator\ -datatype phase = SYSDEV_ext (* System Development Phase (external) *) - | SPl (* Software Planning *) - | SR (* Software Requirement *) - | SA (* Software Architecture *) - | SDES (* Software Design *) - | SCDES (* Software Component Design *) - | CInT (* Component Implementation and Testing *) - | SI (* Software Integration *) - | SV (* Software Validation *) - | SD (* Software Deployment *) - | SM (* Software Maintenance *) +datatype phase = SYSDEV_ext \ \ System Development Phase (external)\ + | SPl \ \Software Planning\ + | SR \ \Software Requirement\ + | SA \ \Software Architecture\ + | SDES \ \Software Design\ + | SCDES \ \Software Component Design\ + | CInT \ \Component Implementation and Testing\ + | SI \ \Software Integration\ + | SV \ \Software Validation\ + | SD \ \Software Deployment\ + | SM \ \Software Maintenance\ abbreviation software_requirement :: "phase" where "software_requirement \ SR" abbreviation software_architecture :: "phase" where "software_architecture \ SA" @@ -429,6 +431,21 @@ doc_class TC = requirement + is_concerned :: "role set" <= "UNIV" type_synonym timing_constraint = TC + +section\Personal Competence\ + +text\pp. 20 MORE TO COME\ + +section\Lifecycle Issues and Documentation\ + +text\Figure 3 in Chapter 5: Illustrative Development Lifecycle 1\ + +text\Global Overview\ + +figure*[fig3::figure, relative_width="100", + src="''examples/CENELEC_50128/mini_odo/document/figures/CENELEC-Fig.3-docStructure.png''"] +\Illustrative Development Lifecycle 1\ + section\Software Assurance related Entities and Concepts\ @@ -494,121 +511,145 @@ doc_class judgement = section\ Design and Test Documents \ -doc_class cenelec_text = text_element + +doc_class cenelec_document = text_element + phase :: "phase" + level :: "int option" <= "Some(0)" + written_by :: role \ \Annex C Table C.1 \ + fst_check :: role \ \Annex C Table C.1\ + snd_check :: role \ \Annex C Table C.1\ is_concerned :: "role set" <= "UNIV" + invariant must_be_chapter :: "text_element.level \ = Some(0)" + invariant three_eyes_prcpl:: " written_by \ \ fst_check \ + \ written_by \ \ snd_check \" +text\see Fig.3.\ - -doc_class SYSREQS = cenelec_text + +doc_class SYSREQS = cenelec_document + phase :: "phase" <= "SYSDEV_ext" - accepts "\objectives||requirement||cenelec_text\\<^sup>+ " + accepts "\objectives||requirement||cenelec_document\\<^sup>+ " type_synonym system_requirements_specification = SYSREQS -doc_class SYSSREQS = cenelec_text + +doc_class SYSSREQS = cenelec_document + phase :: "phase" <= "SYSDEV_ext" type_synonym system_safety_requirements_specification = SYSSREQS -doc_class SYSAD = cenelec_text + +doc_class SYSAD = cenelec_document + phase :: "phase" <= "SYSDEV_ext" type_synonym system_architecture_description = SYSAD -doc_class SYSS_pl = cenelec_text + +doc_class SYSS_pl = cenelec_document + phase :: "phase" <= "SPl" type_synonym system_safety_plan = SYSS_pl -doc_class SYS_VnV_pl = cenelec_text + +doc_class SYS_VnV_pl = cenelec_document + phase :: "phase" <= "SPl" type_synonym system_VnV_plan = SYS_VnV_pl -doc_class SWRS = cenelec_text + +doc_class SWRS = cenelec_document + phase :: "phase" <= "SD" type_synonym software_requirements_specification = SWRS -doc_class SWRVR = cenelec_text + +doc_class SWRVR = cenelec_document + phase :: "phase" <= "SD" type_synonym software_requirements_verification_report = SWRVR -doc_class SWTS = cenelec_text + +doc_class SWTS = cenelec_document + phase :: "phase" <= "SD" type_synonym software_test_specification = SWTS -doc_class SWAS = cenelec_text + + +doc_class SWAS = cenelec_document + phase :: "phase" <= "SD" type_synonym software_architecture_specification = SWAS -doc_class SWDS = cenelec_text + +doc_class SWDS = cenelec_document + phase :: "phase" <= "SD" type_synonym software_design_specification = SWDS -doc_class SWIS = cenelec_text + - phase :: "phase" <= "SD" +doc_class SWIS_E = + \ \input - output of an operation; alternatives could be channels or public global variables ...\ + op_name :: "string" + op_args_ty :: "(string \ typ) list \ typ" + raises_exn :: "(string \ typ) list" \ \exn name and value\ + pre_cond :: "(string \ thm) list" <= "[]" \ \labels and predicates\ + post_cond :: "(string \ thm) list" <= "[]" \ \labels and predicates\ + boundary_pre_cond :: "thm list" <= "[]" + type_synonym software_interface_specification_element = SWIS_E + + +doc_class SWIS = cenelec_document + + phase :: "phase" <= "SCDES" + written_by :: "role" <= "DES" + fst_check :: "role" <= "VER" + snd_check :: "role" <= "VAL" + components :: "SWIS_E list" type_synonym software_interface_specification = SWIS -doc_class SWITS = cenelec_text + +doc_class SWITS = cenelec_document + phase :: "phase" <= "SD" type_synonym software_integration_test_specification = SWITS -doc_class SWHITS = cenelec_text + +doc_class SWHITS = cenelec_document + phase :: "phase" <= "SD" type_synonym software_hardware_integration_test_specification = SWHITS -doc_class SWADVR = cenelec_text + +doc_class SWADVR = cenelec_document + phase :: "phase" <= "SD" type_synonym software_architecture_and_design_verification_report = SWADVR -doc_class SWCDS = cenelec_text + +doc_class SWCDS = cenelec_document + phase :: "phase" <= "SD" type_synonym software_component_design_specification = SWCDS -doc_class SWCTS = cenelec_text + +doc_class SWCTS = cenelec_document + phase :: "phase" <= "SD" type_synonym software_component_test_specification = SWCTS -doc_class SWCDVR = cenelec_text + +doc_class SWCDVR = cenelec_document + phase :: "phase" <= "SD" type_synonym software_component_design_verification_report = SWCDVR -doc_class SWSCD = cenelec_text + +doc_class SWSCD = cenelec_document + phase :: "phase" <= "SD" type_synonym software_source_code_and_documentation = SWSCD -doc_class SWCTR = cenelec_text + +doc_class SWCTR = cenelec_document + phase :: "phase" <= "SD" type_synonym software_component_test_report = SWCTR -doc_class SWSCVR = cenelec_text + +doc_class SWSCVR = cenelec_document + phase :: "phase" <= "SD" type_synonym software_source_code_verification_report = SWSCVR -doc_class SWHAITR = cenelec_text + +doc_class SWHAITR = cenelec_document + phase :: "phase" <= "SD" type_synonym software_hardware_integration_test_report = SWHAITR -doc_class SWIVR = cenelec_text + +doc_class SWIVR = cenelec_document + phase :: "phase" <= "SD" type_synonym software_integration_verification_report = SWIVR -doc_class SWTR_global = cenelec_text + +doc_class SWTR_global = cenelec_document + phase :: "phase" <= "SD" type_synonym overall_software_test_report = SWTR_global -doc_class SWVALR = cenelec_text + +doc_class SWVALR = cenelec_document + phase :: "phase" <= "SD" type_synonym software_validation_report = SWVALR -doc_class SWDD = cenelec_text + +doc_class SWDD = cenelec_document + phase :: "phase" <= "SD" type_synonym software_deployment_documents = SWDD -doc_class SWMD = cenelec_text + +doc_class SWMD = cenelec_document + phase :: "phase" <= "SD" type_synonym software_maintenance_documents = SWMD section\ Software Assurance \ +\ \MORE TO COME\ subsection\ Software Testing \ text\Objective: @@ -725,20 +766,26 @@ doc_class test_requirement = test_item + doc_class test_adm_role = test_item + name :: string -doc_class test_documentation = +doc_class test_documentation = (* OUTDATED ? *) no :: "nat" accepts "test_specification ~~ \test_case~~test_result\\<^sup>+ ~~ \test_environment||test_tool\\<^sup>+ ~~ \test_requirement\ ~~ test_adm_role" - accepts "test_specification ~~ - \test_case~~test_result\\<^sup>+ ~~ - \test_environment||test_tool\\<^sup>+ ~~ - \test_requirement \ ~~ - test_adm_role" +section\Global Documentation Structure\ + +doc_class global_documentation_structure = text_element + + level :: "int option" <= "Some(-1::int)" \ \document must be a chapter\ + accepts "SYSREQS ~~ \ \system_requirements_specification\ + SYSSREQS ~~ \ \system_safety_requirements_specification\ + SYSAD ~~ \ \system_architecture description\ + SYSS_pl ~~ \ \system safety plan\ + (SWRS || SWTS) " \ \software requirements specification OR + overall software test specification\ +(* MORE TO COME : *) section\ META : Testing and Validation \ @@ -771,4 +818,4 @@ ML Syntax.read_typ @{context} "hypothesis" handle _ => dummyT; Proof_Context.init_global; \ -end +end \ No newline at end of file