diff --git a/Isa_COL.thy b/Isa_COL.thy index 12a81fe..460d055 100644 --- a/Isa_COL.thy +++ b/Isa_COL.thy @@ -13,6 +13,9 @@ begin section\ Library of Standard Text Ontology \ + + + datatype placement = pl_h | pl_t | pl_b | pl_ht | pl_hb @@ -45,6 +48,19 @@ doc_class figure_group = (* dito the future monitor: table - block *) +text\ The attribute @{term "level"} in the subsequent enables doc-notation support section* etc. +we follow LaTeX terminology on levels +\<^enum> part = Some -1 +\<^enum> chapter = Some 0 +\<^enum> section = Some 1 +\<^enum> subsection = Some 2 +\<^enum> subsubsection = Some 3 +\<^enum> ... + +for scholarly paper: invariant level > 0 \ + +doc_class text_element = + level :: "int option" <= "None" section\Some attempt to model standardized links to Standard Isabelle Formal Content\ @@ -64,7 +80,7 @@ doc_class formal_content = doc_class concept = tag :: "string" <= "''''" - properties :: "thm list" + properties :: "thm list" <= "[]" section\Tests\ diff --git a/ontologies/CENELEC_50128.thy b/ontologies/CENELEC_50128.thy index 0b2b846..1768ad4 100644 --- a/ontologies/CENELEC_50128.thy +++ b/ontologies/CENELEC_50128.thy @@ -28,7 +28,7 @@ Safety assessment is focused on but not limited to the safety properties of a sy Definition*[assessor::concept, tag="''assessor''"] \entity that carries out an assessment\ -Definition*[cots::concept, tag="''commercial off-the-shelf (COTS) software''"] +Definition*[COTS::concept, tag="''commercial off-the-shelf software''"] \software defined by market-driven need, commercially available and whose fitness for purpose has been demonstrated by a broad spectrum of commercial users\ @@ -44,7 +44,7 @@ criteria: (e. g. subsystems) which have an independent version \ -Definition*[cmgr::concept, tag="''configuration manager''"] +Definition*[CMGR::concept, tag="''configuration manager''"] \entity that is responsible for implementing and carrying out the processes for the configuration management of documents, software and related tools including \<^emph>\change management\\ @@ -71,7 +71,7 @@ from the intended performance or behaviour (cf @{concept \error\})\ Definition*[failure::concept] \unacceptable difference between required and observed performance\ -Definition*[ft::concept, tag="''fault tolerance''"] +Definition*[FT::concept, tag="''fault tolerance''"] \built-in capability of a system to provide continued correct provision of service as specified, in the presence of a limited number of hardware or software faults\ @@ -79,7 +79,7 @@ Definition*[firmware::concept] \software stored in read-only memory or in semi-permanent storage such as flash memory, in a way that is functionally independent of applicative software\ -Definition*[gen_soft::concept,tag="''generic software''"] +Definition*[GS::concept,tag="''generic software''"] \software which can be used for a variety of installations purely by the provision of application-specific data and/or algorithms\ @@ -231,6 +231,8 @@ NOTE Verification is mostly based on document reviews (design, implementation, t Definition*[verifier::concept] \entity that is responsible for one or more verification activities\ +section\Organization, Roles and Responsabilities\ +text\see also section \<^emph>\Software management and organization\.\ datatype role = PM (* Program Manager *) | RQM (* Requirements Manager *) @@ -240,18 +242,22 @@ datatype role = PM (* Program Manager *) | Ne (* Integrator *) | TST (* Tester *) | VER (* Verifier *) + | VnV (* Verification and Validation *) | VAL (* Validator *) -datatype phase = 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" @@ -264,16 +270,209 @@ abbreviation software_validation :: "phase" where "software_validation \ SD" abbreviation software_maintenance :: "phase" where "software_maintenance \ SM" -term "SR" +term "SR" (* meta-test *) + + +section\Objectives, Conformance and Software Integrity Levels\ + +datatype sil = SIL0 | SIL1 | SIL2 | SIL3 | SIL4 + +type_synonym saftety_integraytion_level = sil doc_class objectives = long_name :: "string option" is_concerned :: "role set" +doc_class FnI = objectives + + is_concerned :: "role set" <= "UNIV" + +type_synonym functions_and_interfaces = FnI + +doc_class AC = objectives + + is_concerned :: "role set" <= "UNIV" + +type_synonym application_conditions = AC + +doc_class CoAS = objectives + + is_concerned :: "role set" <= "UNIV" + +type_synonym configuration_or_architecture_of_system = CoAS + +doc_class HtbC = objectives + + is_concerned :: "role set" <= "UNIV" + +type_synonym hazard_to_be_controlled = HtbC + +doc_class SIR = objectives + + is_concerned :: "role set" <= "UNIV" + +type_synonym safety_integrity_requirement = SIR + +text\The following class is a bit unclear about usage and seems to be in +conceptual mismatch with @{typ objectives}: \ +doc_class SILA = objectives + + is_concerned :: "role set" <= "UNIV" + alloc :: "sil" <= "SIL0" + +type_synonym allocation_of_SIL = SILA + +doc_class TC = objectives + + is_concerned :: "role set" <= "UNIV" + +type_synonym timing_constraint = TC + + +section\ Design and Test Documents \ + +doc_class cenelec_text = text_element + + phase :: "phase" + is_concerned :: "role set" <= "UNIV" + + + +doc_class SYSREQS = cenelec_text + + phase :: "phase" <= "SYSDEV_ext" + type_synonym system_requirements_specification = SYSREQS + +doc_class SYSSREQS = cenelec_text + + phase :: "phase" <= "SYSDEV_ext" + type_synonym system_safety_requirements_specification = SYSSREQS + +doc_class SYSS_pl = cenelec_text + + phase :: "phase" <= "SPl" + type_synonym system_safety_plan = SYSS_pl + +doc_class SYS_VnV = cenelec_text + + phase :: "phase" <= "SPl" + type_synonym system_VnV_plan = SYS_VnV + +doc_class SORS = cenelec_text + + phase :: "phase" <= "SD" + type_synonym software_requirements_specification = SORS + +doc_class SOTS = cenelec_text + + phase :: "phase" <= "SD" + type_synonym software_test_specification = SOTS + +doc_class SOAS = cenelec_text + + phase :: "phase" <= "SD" + type_synonym software_architecture_specification = SOAS + +doc_class SODS = cenelec_text + + phase :: "phase" <= "SD" + type_synonym software_design_specification = SODS + +doc_class SOIS = cenelec_text + + phase :: "phase" <= "SD" + type_synonym software_interface_specification = SOIS + +doc_class SOHITS = cenelec_text + + phase :: "phase" <= "SD" + type_synonym software_hardware_integration_test_specification = SOHITS + +doc_class SOCDS = cenelec_text + + phase :: "phase" <= "SD" + type_synonym software_component_design_specification = SOCDS + +doc_class SOCTS = cenelec_text + + phase :: "phase" <= "SD" + type_synonym software_component_test_specification = SOCTS + +doc_class SOSCD = cenelec_text + + phase :: "phase" <= "SD" + type_synonym software_source_code_and_documentation = SOSCD + +doc_class SOCTR = cenelec_text + + phase :: "phase" <= "SD" + type_synonym software_component_test_report = SOCTR + +doc_class SOHAITR = cenelec_text + + phase :: "phase" <= "SD" + type_synonym software_hardware_integration_test_report = SOHAITR + +doc_class SOTR_global = cenelec_text + + phase :: "phase" <= "SD" + type_synonym overall_software_test_report = SOTR_global + +doc_class SODD = cenelec_text + + phase :: "phase" <= "SD" + type_synonym software_deployment_documents = SODD + +doc_class SOMD = cenelec_text + + phase :: "phase" <= "SD" + type_synonym software_maintenance_documents = SOMD + + +section\ Software Assurance \ + +subsection\ Software Testing \ +text\Objective: +The objective of software testing, as performed by the Tester and/or Integrator, +is to ascertain the behaviour or performance of software against the corresponding test +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> Overall Software Test Report +\<^enum> Software Integration Test Specification +\<^enum> Software Integration Test Report +\<^enum> Software/Hardware Integration Test Specification +\<^enum> Software/Hardware Integration Test Report +\<^enum> Software Component Test Specification +\<^enum> Software Component Test Report +\ + +subsection\ Software Verification \ +text\Objective: +The objective of software verification is to examine and arrive at a judgement based on evidence +that output items (process, documentation, software or application) of a specific development +phase fulfil the requirements and plans with respect to completeness, correctness and consistency. +These activities are managed by the @{concept \verifier\}. +\ + +text\Outputs: +\<^enum> Software Verification Plan +\<^enum> Software Verification Report(s) +\<^enum> Software Quality Assurance Verification Report +\ + +subsection\ Software Validation \ +text\Objective: +\<^enum>The objective of software validation is to demonstrate that the processes and their outputs are +such that the software is of the defined software safety integrity level, fulfils the software +requirements and is fit for its intended application. This activity is performed by the Validator. +\<^enum>The main validation activities are to demonstrate by analysis and/or testing that all the software +requirements are specified, implemented, tested and fulfilled as required by the applicable SIL, +and to evaluate the safety criticality of all anomalies and non-conformities based on the results +of reviews, analyses and tests. +\ +text\Output documents: +\<^enum> Software Validation Plan +\<^enum> Software Validation Report +\<^enum> Software Validation Verification Report +\ + +subsection\ Software Assessment \ (* other word for : formal evaluation. *) +text\Objective: +\<^enum>To evaluate that the lifecycle processes and their outputs are such that the software is of the +defined software safety integrity levels 1-4 andis fit for its intended application. +\<^enum> For SIL 0 software, requirements of this standard shall be fulfilled but where a certificate stating +compliance with EN ISO 9001 is available, no assessment will be required. +\ + +subsection\ Software Quality Assurance \ +text\Objectives: To identify, monitor and control all those activities, both technical and +managerial, which are necessary to ensure that the software achieves the quality required. +This is necessary to provide the required qualitative defence against systematic faults and +to ensure that an audit trail can be established to allow +verification and validation activities to be undertaken effectively.\ +(* So : pretty much META *) section\ Requirements-Analysis related Categories \ -doc_class requirement = +doc_class requirement = text_element + long_name :: "string option" is_concerned :: "role set" @@ -405,7 +604,7 @@ doc_class test_documentation = section\ Testing and Validation \ -text\Test : @{concept \cots\}\ +text\Test : @{concept \COTS\}\ ML\ diff --git a/ontologies/scholarly_paper.thy b/ontologies/scholarly_paper.thy index 8e2738b..eb125e0 100644 --- a/ontologies/scholarly_paper.thy +++ b/ontologies/scholarly_paper.thy @@ -22,18 +22,18 @@ doc_class abstract = keywordlist :: "string list" <= "[]" principal_theorems :: "thm list" -doc_class text_section = +doc_class text_section = text_element + main_author :: "author option" <= None fixme_list :: "string list" <= "[]" level :: "int option" <= "None" - (* this attribute enables doc-notation support section* etc. - we follow LaTeX terminology on levels - part = Some -1 - chapter = Some 0 - section = Some 1 - subsection = Some 2 - subsubsection = Some 3 - ... *) + (* this attribute enables doc-notation support section* etc. + we follow LaTeX terminology on levels + part = Some -1 + chapter = Some 0 + section = Some 1 + subsection = Some 2 + subsubsection = Some 3 + ... *) (* for scholarly paper: invariant level > 0 *) doc_class introduction = text_section +