A dramatically improved ontological model of CENELEC 50128
HOL-OCL/Isabelle_DOF/master This commit looks good Details

This commit is contained in:
Burkhart Wolff 2019-02-12 22:13:28 +01:00
parent eb772155ad
commit 5f7e7259d5
3 changed files with 241 additions and 26 deletions

View File

@ -13,6 +13,9 @@ begin
section\<open> Library of Standard Text Ontology \<close>
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\<open> 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 \<close>
doc_class text_element =
level :: "int option" <= "None"
section\<open>Some attempt to model standardized links to Standard Isabelle Formal Content\<close>
@ -64,7 +80,7 @@ doc_class formal_content =
doc_class concept =
tag :: "string" <= "''''"
properties :: "thm list"
properties :: "thm list" <= "[]"
section\<open>Tests\<close>

View File

@ -28,7 +28,7 @@ Safety assessment is focused on but not limited to the safety properties of a sy
Definition*[assessor::concept, tag="''assessor''"]
\<open>entity that carries out an assessment\<close>
Definition*[cots::concept, tag="''commercial off-the-shelf (COTS) software''"]
Definition*[COTS::concept, tag="''commercial off-the-shelf software''"]
\<open>software defined by market-driven need, commercially available and whose fitness for purpose
has been demonstrated by a broad spectrum of commercial users\<close>
@ -44,7 +44,7 @@ criteria:
(e. g. subsystems) which have an independent version
\<close>
Definition*[cmgr::concept, tag="''configuration manager''"]
Definition*[CMGR::concept, tag="''configuration manager''"]
\<open>entity that is responsible for implementing and carrying out the processes
for the configuration management of documents, software and related tools including
\<^emph>\<open>change management\<close>\<close>
@ -71,7 +71,7 @@ from the intended performance or behaviour (cf @{concept \<open>error\<close>})\
Definition*[failure::concept]
\<open>unacceptable difference between required and observed performance\<close>
Definition*[ft::concept, tag="''fault tolerance''"]
Definition*[FT::concept, tag="''fault tolerance''"]
\<open>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\<close>
@ -79,7 +79,7 @@ Definition*[firmware::concept]
\<open>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\<close>
Definition*[gen_soft::concept,tag="''generic software''"]
Definition*[GS::concept,tag="''generic software''"]
\<open>software which can be used for a variety of installations purely by the provision of
application-specific data and/or algorithms\<close>
@ -231,6 +231,8 @@ NOTE Verification is mostly based on document reviews (design, implementation, t
Definition*[verifier::concept]
\<open>entity that is responsible for one or more verification activities\<close>
section\<open>Organization, Roles and Responsabilities\<close>
text\<open>see also section \<^emph>\<open>Software management and organization\<close>.\<close>
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 \<equiv> SR"
abbreviation software_architecture :: "phase" where "software_architecture \<equiv> SA"
@ -264,16 +270,209 @@ abbreviation software_validation :: "phase" where "software_validation \<equi
abbreviation software_deployment :: "phase" where "software_deployment \<equiv> SD"
abbreviation software_maintenance :: "phase" where "software_maintenance \<equiv> SM"
term "SR"
term "SR" (* meta-test *)
section\<open>Objectives, Conformance and Software Integrity Levels\<close>
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\<open>The following class is a bit unclear about usage and seems to be in
conceptual mismatch with @{typ objectives}: \<close>
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\<open> Design and Test Documents \<close>
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\<open> Software Assurance \<close>
subsection\<open> Software Testing \<close>
text\<open>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.
\<close>
text\<open>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
\<close>
subsection\<open> Software Verification \<close>
text\<open>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 \<open>verifier\<close>}.
\<close>
text\<open>Outputs:
\<^enum> Software Verification Plan
\<^enum> Software Verification Report(s)
\<^enum> Software Quality Assurance Verification Report
\<close>
subsection\<open> Software Validation \<close>
text\<open>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.
\<close>
text\<open>Output documents:
\<^enum> Software Validation Plan
\<^enum> Software Validation Report
\<^enum> Software Validation Verification Report
\<close>
subsection\<open> Software Assessment \<close> (* other word for : formal evaluation. *)
text\<open>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.
\<close>
subsection\<open> Software Quality Assurance \<close>
text\<open>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.\<close>
(* So : pretty much META *)
section\<open> Requirements-Analysis related Categories \<close>
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\<open> Testing and Validation \<close>
text\<open>Test : @{concept \<open>cots\<close>}\<close>
text\<open>Test : @{concept \<open>COTS\<close>}\<close>
ML\<open>

View File

@ -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 +