Import of CENELEC_50128.thy changes from /ICFEM-2022
ci/woodpecker/push/build Pipeline was successful
Details
ci/woodpecker/push/build Pipeline was successful
Details
This commit is contained in:
parent
61f167c29c
commit
ae3300ac2c
|
@ -272,34 +272,36 @@ NOTE Verification is mostly based on document reviews (design, implementation, t
|
|||
Definition*[verifier, short_name="''verifier''"]
|
||||
\<open>entity that is responsible for one or more verification activities\<close>
|
||||
|
||||
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>
|
||||
|
||||
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 \<comment> \<open>Program Manager\<close>
|
||||
| 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>
|
||||
| VAL \<comment> \<open>Validator\<close>
|
||||
|
||||
|
||||
|
||||
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 \<comment> \<open> System Development Phase (external)\<close>
|
||||
| SPl \<comment> \<open>Software Planning\<close>
|
||||
| SR \<comment> \<open>Software Requirement\<close>
|
||||
| SA \<comment> \<open>Software Architecture\<close>
|
||||
| SDES \<comment> \<open>Software Design\<close>
|
||||
| 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>
|
||||
| SD \<comment> \<open>Software Deployment\<close>
|
||||
| SM \<comment> \<open>Software Maintenance\<close>
|
||||
|
||||
abbreviation software_requirement :: "phase" where "software_requirement \<equiv> SR"
|
||||
abbreviation software_architecture :: "phase" where "software_architecture \<equiv> SA"
|
||||
|
@ -429,6 +431,21 @@ doc_class TC = requirement +
|
|||
is_concerned :: "role set" <= "UNIV"
|
||||
type_synonym timing_constraint = TC
|
||||
|
||||
|
||||
section\<open>Personal Competence\<close>
|
||||
|
||||
text\<open>pp. 20 MORE TO COME\<close>
|
||||
|
||||
section\<open>Lifecycle Issues and Documentation\<close>
|
||||
|
||||
text\<open>Figure 3 in Chapter 5: Illustrative Development Lifecycle 1\<close>
|
||||
|
||||
text\<open>Global Overview\<close>
|
||||
|
||||
figure*[fig3::figure, relative_width="100",
|
||||
src="''examples/CENELEC_50128/mini_odo/document/figures/CENELEC-Fig.3-docStructure.png''"]
|
||||
\<open>Illustrative Development Lifecycle 1\<close>
|
||||
|
||||
section\<open>Software Assurance related Entities and Concepts\<close>
|
||||
|
||||
|
||||
|
@ -494,121 +511,145 @@ doc_class judgement =
|
|||
|
||||
section\<open> Design and Test Documents \<close>
|
||||
|
||||
doc_class cenelec_text = text_element +
|
||||
doc_class cenelec_document = text_element +
|
||||
phase :: "phase"
|
||||
level :: "int option" <= "Some(0)"
|
||||
written_by :: role \<comment> \<open>Annex C Table C.1 \<close>
|
||||
fst_check :: role \<comment> \<open>Annex C Table C.1\<close>
|
||||
snd_check :: role \<comment> \<open>Annex C Table C.1\<close>
|
||||
is_concerned :: "role set" <= "UNIV"
|
||||
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>"
|
||||
text\<open>see Fig.3.\<close>
|
||||
|
||||
|
||||
|
||||
doc_class SYSREQS = cenelec_text +
|
||||
doc_class SYSREQS = cenelec_document +
|
||||
phase :: "phase" <= "SYSDEV_ext"
|
||||
accepts "\<lbrace>objectives||requirement||cenelec_text\<rbrace>\<^sup>+ "
|
||||
accepts "\<lbrace>objectives||requirement||cenelec_document\<rbrace>\<^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 =
|
||||
\<comment> \<open>input - output of an operation; alternatives could be channels or public global variables ...\<close>
|
||||
op_name :: "string"
|
||||
op_args_ty :: "(string \<times> typ) list \<times> typ"
|
||||
raises_exn :: "(string \<times> typ) list" \<comment> \<open>exn name and value\<close>
|
||||
pre_cond :: "(string \<times> thm) list" <= "[]" \<comment> \<open>labels and predicates\<close>
|
||||
post_cond :: "(string \<times> thm) list" <= "[]" \<comment> \<open>labels and predicates\<close>
|
||||
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\<open> Software Assurance \<close>
|
||||
\<comment> \<open>MORE TO COME\<close>
|
||||
|
||||
subsection\<open> Software Testing \<close>
|
||||
text\<open>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 ~~
|
||||
\<lbrace>test_case~~test_result\<rbrace>\<^sup>+ ~~
|
||||
\<lbrace>test_environment||test_tool\<rbrace>\<^sup>+ ~~
|
||||
\<lbrakk>test_requirement\<rbrakk> ~~
|
||||
test_adm_role"
|
||||
accepts "test_specification ~~
|
||||
\<lbrace>test_case~~test_result\<rbrace>\<^sup>+ ~~
|
||||
\<lbrace>test_environment||test_tool\<rbrace>\<^sup>+ ~~
|
||||
\<lbrakk>test_requirement \<rbrakk> ~~
|
||||
test_adm_role"
|
||||
|
||||
|
||||
section\<open>Global Documentation Structure\<close>
|
||||
|
||||
doc_class global_documentation_structure = text_element +
|
||||
level :: "int option" <= "Some(-1::int)" \<comment> \<open>document must be a chapter\<close>
|
||||
accepts "SYSREQS ~~ \<comment> \<open>system_requirements_specification\<close>
|
||||
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
|
||||
overall software test specification\<close>
|
||||
(* MORE TO COME : *)
|
||||
|
||||
section\<open> META : Testing and Validation \<close>
|
||||
|
||||
|
@ -771,4 +818,4 @@ ML
|
|||
Syntax.read_typ @{context} "hypothesis" handle _ => dummyT;
|
||||
Proof_Context.init_global; \<close>
|
||||
|
||||
end
|
||||
end
|
Loading…
Reference in New Issue