Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

first version of new commands onto_class // doc_class
ci/woodpecker/push/build Pipeline was successful Details

This commit is contained in:
Burkhart Wolff 2022-08-01 15:53:33 +02:00
parent 99facb109c
commit 81c4ae2c13
3 changed files with 202 additions and 101 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

65
examples/CENELEC_50128/mini_odo/mini_odo.thy
View File

@ -19,6 +19,8 @@ theory
"Isabelle_DOF.technical_report" "Isabelle_DOF.technical_report"
begin begin
declare[[strict_monitor_checking=true]] declare[[strict_monitor_checking=true]]
define_shortcut* dof \<rightleftharpoons> \<open>\dof\<close>
isadof \<rightleftharpoons> \<open>\isadof{}\<close>
(*>*) (*>*)
title*[title::title]\<open>The CENELEC 50128 Ontology\<close> title*[title::title]\<open>The CENELEC 50128 Ontology\<close>
@ -27,14 +29,31 @@ subtitle*[subtitle::subtitle]\<open>Case Study: An Odometer-Subsystem\<close>
chapter*[casestudy::technical]\<open>An Odometer-Subsystem\<close> chapter*[casestudy::technical]\<open>An Odometer-Subsystem\<close>
text\<open> text\<open>
In our case study, we will follow the phases of analysis, design, and implementation of the In our case study, we will follow the phases of analysis, design, and implementation of the
odometry function of a train. This software processes data from an odometer to compute the position, odometry function of a train. This \<^cenelec_term>\<open>SF\<close> processes data from an odometer to compute
speed, and acceleration of a train. This system provides the basis for many the position, speed, and acceleration of a train. This system provides the basis for many
safety critical decisions, \eg, the opening of the doors. Due to its relatively small size, it safety critical decisions, \<^eg>, the opening of the doors. Due to its relatively small size, it
is a manageable, albeit realistic target for a comprehensive formal development: it covers a is a manageable, albeit realistic target for a comprehensive formal development: it covers a
physical model of the environment, the physical and architectural model of the odometer including physical model of the environment, the physical and architectural model of the odometer,
the problem of numerical sampling, and the boundaries of efficient computations. The interplay but also the \<^cenelec_term>\<open>SFRS\<close> aspects including
the problem of numerical sampling and the boundaries of efficient computations. The interplay
between environment and measuring-device as well as the implementation problems on a platform between environment and measuring-device as well as the implementation problems on a platform
with limited resources makes the odometer a fairly typical safety critical embedded system. with limited resources makes the odometer a fairly typical \<^cenelec_term>\<open>safety\<close> critical
\<^cenelec_term>\<open>component\<close> of an embedded system.
The case-study is presented in form of an \<^emph>\<open>integrated source\<close> in \<^isadof> containing all four
reports from the phases:
\<^item> \<^term>\<open>software_requirements\<close>, \<^ie> the \<^onto_class>\<open>SWRS\<close> \<^typ>\<open>software_requirements_specification\<close>(-report)
\<^item> \<^term>\<open>software_architecture_and_design\<close>, \<^ie> the \<^typ>\<open>software_design_specification\<close>(-report)
\<^item> \<^term>\<open>component_implementation_and_testing\<close>, \<^ie> the \<^typ>\<open>software_architecture_and_design_verification\<close>(-report)
\<^item> \<^term>\<open>component_implementation_and_testing\<close>, \<^ie> the \<^typ>\<open>software_component_design_verification\<close>(-report)
The objective of this case study is to demonstrate deep-semantical ontologoies in
software developments targeting certifications, and in particular, how \<^isadof>'s
integrated source concept permits to assure \<^cenelec_term>\<open>traceability\<close>.
\<^bold>\<open>NOTE\<close> that this case study has aspects that were actually covered by CENELEC 50126 -
the 'systems'-counterpart covering hardware aspects. Recall that the CENELEC 50128 covers
software.
Due to space reasons, we will focus on the analysis part of the integrated Due to space reasons, we will focus on the analysis part of the integrated
document; the design and code parts will only be outlined in a final resume. The document; the design and code parts will only be outlined in a final resume. The
@ -45,7 +64,7 @@ text\<open>
development. development.
\<close> \<close>
section\<open>System Requirements as an \<^emph>\<open>Integrated Source\<close>\<close> section\<open>A CENELEC-conform development as an \<^emph>\<open>Integrated Source\<close>\<close>
text\<open>Accurate information of a train's location along a track is in an important prerequisite text\<open>Accurate information of a train's location along a track is in an important prerequisite
to safe railway operation. Position, speed and acceleration measurement usually lies on a to safe railway operation. Position, speed and acceleration measurement usually lies on a
set of independent measurements based on different physical principles---as a way to enhance set of independent measurements based on different physical principles---as a way to enhance
@ -74,17 +93,19 @@ text\<open>
This model is already based on several fundamental assumptions relevant for the correct This model is already based on several fundamental assumptions relevant for the correct
functioning of the system and for its integration into the system as a whole. In functioning of the system and for its integration into the system as a whole. In
particular, we need to make the following assumptions explicit:\vspace{-.3cm} particular, we need to make the following assumptions explicit: \<^vs>\<open>-0.3cm\<close>
\<^item> that the wheel is perfectly circular with a given, constant radius,
\<^item> that the slip between the trains wheel and the track negligible, \<^item> that the wheel is perfectly circular with a given, constant radius,
\<^item> the distance between all teeth of a wheel is the same and constant, and \<^item> that the slip between the trains wheel and the track negligible,
\<^item> the sampling rate of positions is a given constant. \<^item> the distance between all teeth of a wheel is the same and constant, and
\<^item> the sampling rate of positions is a given constant.
These assumptions have to be traced throughout the certification process as These assumptions have to be traced throughout the certification process as
\<^emph>\<open>derived requirements\<close> (or, in CENELEC terminology, as \<^emph>\<open>exported constraints\<close>), which is \<^emph>\<open>derived requirements\<close> (or, in CENELEC terminology, as \<^emph>\<open>exported constraints\<close>), which is
also reflected by their tracing throughout the body of certification documents. This may result also reflected by their tracing throughout the body of certification documents. This may result
in operational regulations, \eg, regular checks for tolerable wheel defects. As for the in operational regulations, \<^eg>, regular checks for tolerable wheel defects. As for the
\<^emph>\<open>no slip\<close>-assumption, this leads to the modeling of constraints under which physical \<^emph>\<open>no slip\<close>-assumption, this leads to the modeling of constraints under which physical
slip can be neglected: the device can only produce reliable results under certain physical slip can be neglected: the device can only produce reliable results under certain physical
constraints (speed and acceleration limits). Moreover, the \<^emph>\<open>no slip\<close>-assumption motivates constraints (speed and acceleration limits). Moreover, the \<^emph>\<open>no slip\<close>-assumption motivates
@ -112,7 +133,7 @@ subsection\<open>Capturing ``System Interfaces.''\<close>
text\<open> text\<open>
The requirements analysis also contains a sub-document \<^emph>\<open>functions and interfaces\<close> The requirements analysis also contains a sub-document \<^emph>\<open>functions and interfaces\<close>
(CENELEC notion) describing the technical format of the output of the odometry function. (CENELEC notion) describing the technical format of the output of the odometry function.
This section, \eg, specifies the output \<^emph>\<open>speed\<close> as given by a \<^verbatim>\<open>int_32\<close> to be the This section, \<^eg>, specifies the output \<^emph>\<open>speed\<close> as given by a \<^verbatim>\<open>int_32\<close> to be the
``Estimation of the speed (in mm/sec) evaluated over the latest $N_{\text{avg}}$ samples'' ``Estimation of the speed (in mm/sec) evaluated over the latest $N_{\text{avg}}$ samples''
where the speed refers to the physical speed of the train and $N_{\text{avg}}$ a parameter of the where the speed refers to the physical speed of the train and $N_{\text{avg}}$ a parameter of the
sub-system configuration. \<close> sub-system configuration. \<close>
@ -143,7 +164,7 @@ text\<open>
The design provides a function that manages an internal first-in-first-out buffer of The design provides a function that manages an internal first-in-first-out buffer of
shaft-encodings and corresponding positions. Central for the design is a step-function analyzing shaft-encodings and corresponding positions. Central for the design is a step-function analyzing
new incoming shaft encodings, checking them and propagating two kinds of error-states (one allowing new incoming shaft encodings, checking them and propagating two kinds of error-states (one allowing
recovery, another one, fatal, signaling, \eg, a defect of the receiver hardware), recovery, another one, fatal, signaling, \<^eg>, a defect of the receiver hardware),
calculating the relative position, speed and acceleration. calculating the relative position, speed and acceleration.
\<close> \<close>
@ -316,7 +337,7 @@ text\<open>
\isadof is designed to annotate text elements with structured meta-information and to reference \isadof is designed to annotate text elements with structured meta-information and to reference
these text elements throughout the integrated source. A classical application of this capability these text elements throughout the integrated source. A classical application of this capability
is the annotation of concepts and terms definitions---be them informal, semi-formal or formal---and is the annotation of concepts and terms definitions---be them informal, semi-formal or formal---and
their consistent referencing. In the context of our CENELEC ontology, \eg, we can translate the their consistent referencing. In the context of our CENELEC ontology, \<^eg>, we can translate the
third chapter of @{cite "bsi:50128:2014"} ``Terms, Definitions and Abbreviations'' directly third chapter of @{cite "bsi:50128:2014"} ``Terms, Definitions and Abbreviations'' directly
into our Ontology Definition Language (ODL). Picking one example out of 49, consider the definition into our Ontology Definition Language (ODL). Picking one example out of 49, consider the definition
of the concept ``traceability'' in paragraphs 3.1.46 (a notion referenced 31 times in the standard), of the concept ``traceability'' in paragraphs 3.1.46 (a notion referenced 31 times in the standard),
@ -370,7 +391,7 @@ datatype vnt_technique =
suggest that their work is superfluous. Our framework allows to statically check that tests or proofs suggest that their work is superfluous. Our framework allows to statically check that tests or proofs
have been provided, at places where the ontology requires them to be, and both assessors and developers have been provided, at places where the ontology requires them to be, and both assessors and developers
can rely on this check and navigate through related information easily. It does not guarantee that can rely on this check and navigate through related information easily. It does not guarantee that
intended concepts for, \eg, safety or security have been adequately modeled. intended concepts for, \<^eg>, safety or security have been adequately modeled.
\<close> \<close>
section*[moe::text_section] section*[moe::text_section]
@ -386,7 +407,7 @@ doc_class requirement = text_element +
where the \inlineisar*roles* are exactly the ones defined in the previous section and represent where the \inlineisar*roles* are exactly the ones defined in the previous section and represent
the groups of stakeholders in the CENELEC process. Therefore, the \inlineisar+is_concerned+-attribute the groups of stakeholders in the CENELEC process. Therefore, the \inlineisar+is_concerned+-attribute
allows expressing who ``owns'' this text-element. \isadof supports a role-based allows expressing who ``owns'' this text-element. \isadof supports a role-based
presentation, \eg, different presentation styles of the presentation, \<^eg>, different presentation styles of the
integrated source may decide to highlight, to omit, to defer into an annex, text entities integrated source may decide to highlight, to omit, to defer into an annex, text entities
according to the role-set. according to the role-set.
@ -400,17 +421,17 @@ doc_class sub_requirement =
section*[claimsreqevidence::text_section]\<open>Tracking Claims, Derived Requirements and Evidence\<close> section*[claimsreqevidence::text_section]\<open>Tracking Claims, Derived Requirements and Evidence\<close>
text\<open>An example for making explicit implicit principles, text\<open>An example for making explicit implicit principles,
consider the following statement @{cite "bsi:50128:2014"}, pp. 25.:\vspace{-1.5mm} consider the following statement @{cite "bsi:50128:2014"}, pp. 25.: \<^vs>\<open>-0.15cm\<close>
\begin{quote}\small \begin{quote}\small
The objective of software verification is to examine and arrive at a judgment based on The objective of software verification is to examine and arrive at a judgment based on
evidence that output items (process, documentation, software or application) of a specific evidence that output items (process, documentation, software or application) of a specific
development phase fulfill the requirements and plans with respect to completeness, correctness development phase fulfill the requirements and plans with respect to completeness, correctness
and consistency. and consistency.
\end{quote}\vspace{-1.5mm} \end{quote} \<^vs>\<open>-0.15cm\<close>
The terms \<^emph>\<open>judgment\<close> and \<^emph>\<open>evidence\<close> are used as a kind of leitmotif throughout the CENELEC The terms \<^emph>\<open>judgment\<close> and \<^emph>\<open>evidence\<close> are used as a kind of leitmotif throughout the CENELEC
standard, but they are neither explained nor even listed in the general glossary. However, the standard, but they are neither explained nor even listed in the general glossary. However, the
standard is fairly explicit on the \<^emph>\<open>phase\<close>s and the organizational roles that different stakeholders standard is fairly explicit on the \<^emph>\<open>phase\<close>s and the organizational roles that different stakeholders
should have in the process. Our version to express this key concept of judgment, \eg, by should have in the process. Our version to express this key concept of judgment, \<^eg>, by
the following concept: the following concept:
\begin{isar} \begin{isar}
doc_class judgement = doc_class judgement =
@ -461,7 +482,7 @@ text*[J1::judgement, refers_to="<@>{docitem <open>encoder_props<close>}",
\end{isar} \end{isar}
The references \inlineisar|<@>{...}|, called antiquotation, allow us not only to reference to The references \inlineisar|<@>{...}|, called antiquotation, allow us not only to reference to
formal concepts, they are checked for consistency and there are also antiquotations that formal concepts, they are checked for consistency and there are also antiquotations that
print the formally checked content (\eg, the statement of a theorem). print the formally checked content (\<^eg>, the statement of a theorem).
\<close> \<close>
subsection\<open>Exporting Claims of the Requirements Specification.\<close> subsection\<open>Exporting Claims of the Requirements Specification.\<close>

22
src/DOF/Isa_DOF.thy
View File

@ -2429,6 +2429,8 @@ val parse_cid = Scan.lift(Parse.position Args.name)
val parse_oid' = Term_Style.parse -- parse_oid val parse_oid' = Term_Style.parse -- parse_oid
val parse_cid' = Term_Style.parse -- parse_cid val parse_cid' = Term_Style.parse -- parse_cid
val parse_attribute_access = (parse_oid val parse_attribute_access = (parse_oid
--| (Scan.lift @{keyword "::"}) --| (Scan.lift @{keyword "::"})
-- Scan.lift (Parse.position Args.name)) -- Scan.lift (Parse.position Args.name))
@ -2473,6 +2475,25 @@ fun pretty_trace_style ctxt (style, (oid,pos)) =
fun pretty_cid_style ctxt (style, (cid,pos)) = fun pretty_cid_style ctxt (style, (cid,pos)) =
Document_Output.pretty_term ctxt (style (compute_cid_repr ctxt cid pos)); Document_Output.pretty_term ctxt (style (compute_cid_repr ctxt cid pos));
(* NEW VERSION: PLEASE INTEGRATE ALL OVER : *)
fun context_position_parser parse_con (ctxt, toks) =
let val pos = case toks of
a :: _ => Token.pos_of a
| _ => @{here} \<comment> \<open>a real hack !\<close>
val (res, (ctxt', toks')) = parse_con (ctxt, toks)
in ((res,pos),(ctxt', toks')) end
val parse_cid = (context_position_parser Args.typ_abbrev)
>> (fn (Type(ss,_),pos) => (pos,ss)
|( _,pos) => ISA_core.err "Undefined Class Id" pos);
val parse_cid' = Term_Style.parse -- parse_cid
fun pretty_cid_style ctxt (style,(pos,cid)) =
(*reconversion to term in order to haave access to term print options like: short_names etc...) *)
Document_Output.pretty_term ctxt ((compute_cid_repr ctxt cid pos));
in in
val _ = Theory.setup val _ = Theory.setup
(ML_Antiquotation.inline \<^binding>\<open>docitem\<close> (ML_Antiquotation.inline \<^binding>\<open>docitem\<close>
@ -2483,6 +2504,7 @@ val _ = Theory.setup
(fn (ctxt,toks) => (parse_oid >> trace_attr_2_ML ctxt) (ctxt, toks)) #> (fn (ctxt,toks) => (parse_oid >> trace_attr_2_ML ctxt) (ctxt, toks)) #>
basic_entity \<^binding>\<open>trace_attribute\<close> parse_oid' pretty_trace_style #> basic_entity \<^binding>\<open>trace_attribute\<close> parse_oid' pretty_trace_style #>
basic_entity \<^binding>\<open>doc_class\<close> parse_cid' pretty_cid_style #> basic_entity \<^binding>\<open>doc_class\<close> parse_cid' pretty_cid_style #>
basic_entity \<^binding>\<open>onto_class\<close> parse_cid' pretty_cid_style #>
basic_entity \<^binding>\<open>docitem_attribute\<close> parse_attribute_access' pretty_attr_access_style basic_entity \<^binding>\<open>docitem_attribute\<close> parse_attribute_access' pretty_attr_access_style
) )
end end

216
src/ontologies/CENELEC_50128/CENELEC_50128.thy
View File

@ -15,9 +15,9 @@ chapter \<open>An Outline of a CENELEC Ontology\<close>
text\<open> NOTE: An Ontology-Model of a certification standard such as CENELEC or Common Criteria text\<open> NOTE: An Ontology-Model of a certification standard such as CENELEC or Common Criteria
identifies: identifies:
- notions (conceptual \emph{categories}) having \emph{instances} - notions (conceptual \<^emph>\<open>categories\<close>) having \<^emph>\<open>instances\<close>
(similar to classes and objects), (similar to classes and objects),
- their subtype relation (eg., a "SRAC" is an "assumption"), - their \<^emph>\<open>subtype\<close> relation (eg., a "SRAC" is an "assumption"),
- their syntactical structure - their syntactical structure
(for the moment: defined by regular expressions describing the (for the moment: defined by regular expressions describing the
order of category instances in the overall document as a regular language) order of category instances in the overall document as a regular language)
@ -40,23 +40,78 @@ begin
*) *)
text\<open>We re-use the class @\<open>typ math_content\<close>, which provides also a framework for text\<open>We re-use the class \<^typ>\<open>math_content\<close>, which provides also a framework for
semi-formal "math-alike" terminology, which we re-use by this definition.\<close> semi-formal "math-alike" terminology, which we re-use by this definition.\<close>
doc_class semi_formal_content = math_content + doc_class semi_formal_content = math_content +
status :: status <= "semiformal" status :: status <= "semiformal"
mcc :: math_content_class <= "terminology" mcc :: math_content_class
type_synonym sfc = semi_formal_content type_synonym sfc = semi_formal_content
(*>>*) doc_class cenelec_term = semi_formal_content +
mcc :: math_content_class <= "terminology"
declare[[ Definition_default_class="semi_formal_content"]]
text\<open> in the following, all \<^theory_text>\<open>Definition*\<close> statements are interpreted as
\<^doc_class>\<open>cenelec_term\<close>s, i.e. semi-formal teminological definitions.\<close>
(*
ML\<open>
val typ_abbrev = Scan.lift
\<close>
ML\<open>
Parse.position: ( Token.T list -> 'a * Token.T list) -> ('a * Position.T) parser;
Scan.lift(Parse.position Args.name) ;
Args.name_position;
Proof_Context.read_typ_abbrev;
Args.typ_abbrev : Context.generic * Token.T list -> typ * (Context.generic * Token.T list) ;
Proof_Context.read_typ_abbrev;
(Args.typ_abbrev >> (fn Type(ss,_) => ss
| _ => error "Undefined Class Id"))
\<close>
ML\<open>
fun context_position_parser parse_con (ctxt, toks) =
let val pos = case toks of
a :: _ => Token.pos_of a
| _ => @{here} \<comment> \<open>a real hack !\<close>
val (res, (ctxt', toks')) = parse_con (ctxt, toks)
in ((res,pos),(ctxt', toks')) end
val parse_cid = (context_position_parser Args.typ_abbrev)
>> (fn (Type(ss,_),pos) => (pos,ss)
|( _,pos) => ISA_core.err "Undefined Class Id" pos);
val parse_cid' = Term_Style.parse -- parse_cid
fun pretty_cid_style ctxt (style,(pos,cid)) =
(*reconversion to term in order to haave access to term print options like: short_names etc...) *)
Document_Output.pretty_term ctxt ((AttributeAccess.compute_cid_repr ctxt cid pos));
val _ = Theory.setup (AttributeAccess.basic_entity \<^binding>\<open>Onto_class\<close> parse_cid' pretty_cid_style)
\<close>
text\<open> \<^Onto_class>\<open>cenelec_term\<close> \<close>
*)
declare[[ Definition_default_class="cenelec_term"]]
(*>>*)
text\<open> Excerpt of the BE EN 50128:2011, page 22. \<close> text\<open> Excerpt of the BE EN 50128:2011, page 22. \<close>
section\<open>Terms and Definitions\<close> section\<open>Terms and Definitions\<close>
Definition*[assessment,short_name="''assessment''"] Definition*[assessment,short_name="''assessment''"]
@ -66,90 +121,90 @@ requirements and to form a judgement as to whether the software is fit for its
Safety assessment is focused on but not limited to the safety properties of a system.\<close> Safety assessment is focused on but not limited to the safety properties of a system.\<close>
Definition*[assessor, short_name="''assessor''"] Definition*[assessor, short_name="''assessor''"]
\<open>entity that carries out an assessment\<close> \<open>entity that carries out an assessment.\<close>
Definition*[COTS, short_name="''commercial off-the-shelf software''"] Definition*[COTS, short_name="''commercial off-the-shelf software''"]
\<open>software defined by market-driven need, commercially available and whose fitness for purpose \<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> has been demonstrated by a broad spectrum of commercial users.\<close>
Definition*[component] Definition*[component]
\<open>a constituent part of software which has well-defined interfaces and behaviour \<open>a constituent part of software which has well-defined interfaces and behaviour
with respect to the software architecture and design and fulfils the following with respect to the software architecture and design and fulfils the following
criteria: criteria:
\<^enum> it is designed according to “Components” (see Table A.20); \<^enum> it is designed according to “Components” (see Table A.20);
\<^enum> it covers a specific subset of software requirements; \<^enum> it covers a specific subset of software requirements;
\<^enum> it is clearly identified and has an independent version inside the \<^enum> it is clearly identified and has an independent version inside the
configuration management system or is a part of a collection of components configuration management system or is a part of a collection of components
(e. g. subsystems) which have an independent version (e. g. subsystems) which have an independent version
\<close> \<close>
typ "sfc" typ "sfc"
Definition*[CMGR, short_name="''configuration manager''"] Definition*[CMGR, short_name="''configuration manager''"]
\<open>entity that is responsible for implementing and carrying out the processes \<open>entity that is responsible for implementing and carrying out the processes
for the configuration management of documents, software and related tools including for the configuration management of documents, software and related tools including
\<^emph>\<open>change management\<close>\<close> \<^emph>\<open>change management\<close>.\<close>
Definition*[customer] Definition*[customer]
\<open>entity which purchases a railway control and protection system including the software\<close> \<open>entity which purchases a railway control and protection system including the software.\<close>
Definition*[designer] Definition*[designer]
\<open>entity that analyses and transforms specified requirements into acceptable design solutions \<open>entity that analyses and transforms specified requirements into acceptable design solutions
which have the required safety integrity level\<close> which have the required safety integrity level.\<close>
Definition*[entity] Definition*[entity]
\<open>person, group or organisation who fulfils a role as defined in this European Standard\<close> \<open>person, group or organisation who fulfils a role as defined in this European Standard.\<close>
declare_reference*[fault] declare_reference*[fault]
Definition*[error] Definition*[error]
\<open>defect, mistake or inaccuracy which could result in failure or in a deviation \<open>defect, mistake or inaccuracy which could result in failure or in a deviation
from the intended performance or behaviour (cf. @{semi_formal_content (unchecked) \<open>fault\<close>}))\<close> from the intended performance or behaviour (cf. @{cenelec_term (unchecked) \<open>fault\<close>})).\<close>
Definition*[fault] Definition*[fault]
\<open>defect, mistake or inaccuracy which could result in failure or in a deviation \<open>defect, mistake or inaccuracy which could result in failure or in a deviation
from the intended performance or behaviour (cf @{semi_formal_content \<open>error\<close>})\<close> from the intended performance or behaviour (cf @{cenelec_term \<open>error\<close>}).\<close>
Definition*[failure] Definition*[failure]
\<open>unacceptable difference between required and observed performance\<close> \<open>unacceptable difference between required and observed performance.\<close>
Definition*[FT, short_name="''fault tolerance''"] Definition*[FT, short_name="''fault tolerance''"]
\<open>built-in capability of a system to provide continued correct provision of service as specified, \<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> in the presence of a limited number of hardware or software faults.\<close>
Definition*[firmware] Definition*[firmware]
\<open>software stored in read-only memory or in semi-permanent storage such as flash memory, in a \<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> way that is functionally independent of applicative software.\<close>
Definition*[GS,short_name="''generic software''"] Definition*[GS,short_name="''generic software''"]
\<open>software which can be used for a variety of installations purely by the provision of \<open>software which can be used for a variety of installations purely by the provision of
application-specific data and/or algorithms\<close> application-specific data and/or algorithms.\<close>
Definition*[implementer] Definition*[implementer]
\<open>entity that transforms specified designs into their physical realisation\<close> \<open>entity that transforms specified designs into their physical realisation.\<close>
Definition*[integration] Definition*[integration]
\<open>process of assembling software and/or hardware items, according to the architectural and \<open>process of assembling software and/or hardware items, according to the architectural and
design specification, and testing the integrated unit\<close> design specification, and testing the integrated unit.\<close>
Definition*[integrator] Definition*[integrator]
\<open>entity that carries out software integration\<close> \<open>entity that carries out software integration.\<close>
Definition*[PES :: sfc, short_name="''pre-existing software''"] Definition*[PES, short_name="''pre-existing software''"]
\<open>software developed prior to the application currently in question, including COTS (commercial \<open>software developed prior to the application currently in question, including COTS (commercial
off-the shelf) and open source software\<close> off-the shelf) and open source software.\<close>
Definition*[OSS :: sfc, short_name="''open source software''"] Definition*[OS, short_name="''open source software''"]
\<open>source code available to the general public with relaxed or non-existent copyright restrictions\<close> \<open>source code available to the general public with relaxed or non-existent copyright restrictions.\<close>
Definition*[PLC, short_name="''programmable logic controller''"] Definition*[PLC, short_name="''programmable logic controller''"]
\<open>solid-state control system which has a user programmable memory for storage of instructions to \<open>solid-state control system which has a user programmable memory for storage of instructions to
implement specific functions\<close> implement specific functions.\<close>
Definition*[PM, short_name="''project management''"] Definition*[PM, short_name="''project management''"]
\<open>administrative and/or technical conduct of a project, including safety aspects\<close> \<open>administrative and/or technical conduct of a project, including safety aspects.\<close>
Definition*[PMGR, short_name="''project manager''"] Definition*[PMGR, short_name="''project manager''"]
\<open>entity that carries out project management\<close> \<open>entity that carries out \<^cenelec_term>\<open>PM\<close>.\<close>
Definition*[reliability] Definition*[reliability]
\<open>ability of an item to perform a required function under given conditions for a given period of time\<close> \<open>ability of an item to perform a required function under given conditions for a given period of time\<close>
@ -157,52 +212,52 @@ Definition*[reliability]
Definition*[robustness] Definition*[robustness]
\<open>ability of an item to detect and handle abnormal situations\<close> \<open>ability of an item to detect and handle abnormal situations\<close>
Definition*[RMGR, short_name="''requirements manager''"]
\<open>entity that carries out requirements management\<close>
Definition*[RM, short_name="''requirements management''"] Definition*[RM, short_name="''requirements management''"]
\<open>the process of eliciting, documenting, analysing, prioritising and agreeing on requirements and \<open>the process of eliciting, documenting, analysing, prioritising and agreeing on requirements and
then controlling change and communicating to relevant stakeholders. It is a continuous process then controlling change and communicating to relevant stakeholders. It is a continuous process
throughout a project\<close> throughout a project\<close>
Definition*[RMGR, short_name="''requirements manager''"]
\<open>entity that carries out \<^cenelec_term>\<open>RM\<close>.\<close>
Definition*[risk] Definition*[risk]
\<open>combination of the rate of occurrence of accidents and incidents resulting in harm (caused by \<open>combination of the rate of occurrence of accidents and incidents resulting in harm (caused by
a hazard) and the degree of severity of that harm\<close> a hazard) and the degree of severity of that harm.\<close>
Definition*[safety] Definition*[safety]
\<open>freedom from unacceptable levels of risk of harm to people\<close> \<open>freedom from unacceptable levels of risk of harm to people.\<close>
Definition*[SA, short_name="''safety authority''"] Definition*[SA, short_name="''safety authority''"]
\<open>body responsible for certifying that safety related software or services comply with relevant \<open>body responsible for certifying that safety related software or services comply with relevant
statutory safety requirements\<close> statutory safety requirements.\<close>
Definition*[SF, short_name="''safety function''"] Definition*[SF, short_name="''safety function''"]
\<open>a function that implements a part or whole of a safety requirement\<close> \<open>a function that implements a part or whole of a safety requirement.\<close>
Definition*[SFRS, short_name= "''safety-related software''"] Definition*[SFRS, short_name= "''safety-related software''"]
\<open>software which performs safety functions\<close> \<open>software which performs safety functions.\<close>
Definition*[software] Definition*[software]
\<open>intellectual creation comprising the programs, procedures, rules, data and any associated \<open>intellectual creation comprising the programs, procedures, rules, data and any associated
documentation pertaining to the operation of a system\<close> documentation pertaining to the operation of a system.\<close>
Definition*[SB, short_name="''software baseline''"] Definition*[SB, short_name="''software baseline''"]
\<open>complete and consistent set of source code, executable files, configuration files, \<open>complete and consistent set of source code, executable files, configuration files,
installation scripts and documentation that are needed for a software release. Information about installation scripts and documentation that are needed for a software release. Information about
compilers, operating systems, preexisting software and dependent tools is stored as part of the compilers, operating systems, preexisting software and dependent tools is stored as part of the
baseline. This will enable the organisation to reproduce defined versions and be the input baseline. This will enable the organisation to reproduce defined versions and be the input
for future releases at enhancements or at upgrade in the maintenance phase\<close> for future releases at enhancements or at upgrade in the maintenance phase.\<close>
Definition*[SD, short_name="''software deployment''"] Definition*[SD, short_name="''software deployment''"]
\<open>transferring, installing and activating a deliverable software baseline that has already been \<open>transferring, installing and activating a deliverable software baseline that has already been
released and assessed\<close> released and assessed.\<close>
Definition*[SWLC, short_name="''software life-cycle''"] Definition*[SWLC, short_name="''software life-cycle''"]
\<open>those activities occurring during a period of time that starts when \<open>those activities occurring during a period of time that starts when
software is conceived and ends when the software is no longer available for use. The software life software is conceived and ends when the software is no longer available for use. The software life
cycle typically includes a requirements phase, design phase,test phase, integration phase, cycle typically includes a requirements phase, design phase, test phase, integration phase,
deployment phase and a maintenance phase\<close> deployment phase and a maintenance phase.\<close>
Definition*[SWMA, short_name="''software maintainability''"] Definition*[SWMA, short_name="''software maintainability''"]
\<open>capability of the software to be modified; to correct faults, \<open>capability of the software to be modified; to correct faults,
@ -210,11 +265,12 @@ improve performance or other attributes, or adapt it to a different environment\
Definition*[SM, short_name="''software maintenance''"] Definition*[SM, short_name="''software maintenance''"]
\<open> action, or set of actions, carried out on software after deployment functionality \<open> action, or set of actions, carried out on software after deployment functionality
performance or other attributes, or adapt it with the aim of enhancing or correcting its\<close> performance or other attributes, or adapt it with the aim of enhancing or correcting its behaviour.\<close>
Definition*[SOSIL, short_name="''software safety integrity level''"] Definition*[SOSIL, short_name="''software safety integrity level''"]
\<open>classification number which determines the techniques and measures that have to be applied to \<open>classification number which determines the techniques and measures that have to be applied to
software software.
NOTE: Safety-related software has been classified into five safety integrity levels, where NOTE: Safety-related software has been classified into five safety integrity levels, where
0 is the lowest and 4 the highest.\<close> 0 is the lowest and 4 the highest.\<close>
@ -255,16 +311,16 @@ not obvious; a compiler that incorporates an executable run-time package into th
Definition*[traceability, short_name="''traceability''"] Definition*[traceability, short_name="''traceability''"]
\<open>degree to which relationship can be established between two or more products of a development \<open>degree to which relationship can be established between two or more products of a development
process, especially those having a predecessor/successor or master/subordinate relationship to one process, especially those having a predecessor/successor or master/subordinate relationship to one
another\<close> another.\<close>
Definition*[validation, short_name="''validation''"] Definition*[validation, short_name="''validation''"]
\<open>process of analysis followed by a judgment based on evidence to \<open>process of analysis followed by a judgment based on evidence to
documentation, software or application) fits the user needs,in particular with respect to safety documentation, software or application) fits the user needs,in particular with respect to safety
and quality and determine whether an item (e.g. process, with emphasis on the suitability of its and quality and determine whether an item (e.g. process, with emphasis on the suitability of its
operation in accordance to its purpose in its intended environment\<close> operation in accordance to its purpose in its intended environment.\<close>
Definition*[validator, short_name="''validator''"] Definition*[validator, short_name="''validator''"]
\<open>entity that is responsible for the validation\<close> \<open>entity that is responsible for the validation.\<close>
Definition*[verification, short_name="''verification''"] Definition*[verification, short_name="''verification''"]
\<open>process of examination followed by a judgment based on evidence that output items (process, \<open>process of examination followed by a judgment based on evidence that output items (process,
@ -275,13 +331,13 @@ NOTE: Verification is mostly based on document reviews
\<close> \<close>
Definition*[verifier, short_name="''verifier''"] Definition*[verifier, short_name="''verifier''"]
\<open>entity that is responsible for one or more verification activities\<close> \<open>entity that is responsible for one or more verification activities.\<close>
chapter\<open>Software Management and Organisation\<close> chapter\<open>Software Management and Organisation\<close>
text\<open>Representing chapter 5 in @{cite "bsi:50128:2014"}.\<close> text\<open>Representing chapter 5 in @{cite "bsi:50128:2014"}.\<close>
section\<open>Organization, Roles and Responsabilities\<close> section\<open>Organization, Roles and Responsabilities\<close>
text\<open>See also section \<^emph>\<open>Software management and organization\<close>. and Annex B and C\<close> text\<open>See also section \<^emph>\<open>Software management and organization\<close> and Annex B and C.\<close>
text\<open>REQ role in Table C.1 is assumed to be a typo and should be RQM.\<close> text\<open>REQ role in Table C.1 is assumed to be a typo and should be RQM.\<close>
@ -300,17 +356,17 @@ datatype role = RQM \<comment> \<open>Requirements Manager\<close>
datatype phase = SYSDEV_ext \<comment> \<open> System Development Phase (external)\<close> datatype phase = SYSDEV_ext \<comment> \<open> System Development Phase (external)\<close>
| SPl \<comment> \<open>Software Planning\<close> | SPl \<comment> \<open>Software Planning\<close>
| SR \<comment> \<open>Software Requirements\<close> | SR \<comment> \<open>Software Requirements\<close>
| SADES \<comment> \<open>Software Architecture and Design\<close> | SADES \<comment> \<open>Software Architecture and Design\<close>
| SCDES \<comment> \<open>Software Component Design\<close> | SCDES \<comment> \<open>Software Component Design\<close>
| CInT \<comment> \<open>Component Implementation and Testing\<close> | CInT \<comment> \<open>Component Implementation and Testing\<close>
| SI \<comment> \<open>Software Integration\<close> | SI \<comment> \<open>Software Integration\<close>
| SV \<comment> \<open>Overall Software Testing/Final Validation\<close> | SV \<comment> \<open>Overall Software Testing/Final Validation\<close>
| SCADA \<comment> \<open>Systems Configured by Application Data/Algorithms\<close> | SCADA \<comment> \<open>Systems Configured by Application Data/Algorithms\<close>
| SD \<comment> \<open>Software Deployment\<close> | SD \<comment> \<open>Software Deployment\<close>
| SM \<comment> \<open>Software Maintenance\<close> | SM \<comment> \<open>Software Maintenance\<close>
| SA \<comment> \<open>Software Assessment\<close> | SA \<comment> \<open>Software Assessment\<close>
abbreviation software_planning :: "phase" where "software_planning \<equiv> SPl" abbreviation software_planning :: "phase" where "software_planning \<equiv> SPl"
abbreviation software_requirements :: "phase" where "software_requirements \<equiv> SR" abbreviation software_requirements :: "phase" where "software_requirements \<equiv> SR"
@ -340,7 +396,7 @@ text\<open>Requirement levels specified Annex A: we use the term \<^emph>\<open>
them from the requirements specified in the standard.\<close> them from the requirements specified in the standard.\<close>
datatype normative_level = datatype normative_level =
M \<comment> \<open>(Mandatory)\<close> M \<comment> \<open>(Mandatory)\<close>
| HR \<comment> \<open>Highly Recommended\<close> | HR \<comment> \<open>Highly Recommended\<close>
| R \<comment> \<open>Recommended\<close> | R \<comment> \<open>Recommended\<close>
| Any \<comment> \<open>No recommendation\<close> | Any \<comment> \<open>No recommendation\<close>
@ -365,14 +421,15 @@ doc_class safety_requirement = requirement +
formal_definition :: "thm list" formal_definition :: "thm list"
text\<open>The category @{emph \<open>hypothesis\<close>} is used for assumptions from the text\<open>
foundational mathematical or physical domain, so for example: The category \<^emph>\<open>hypothesis\<close> is used for assumptions from the
\<^item> the Mordell-Lang conjecture holds, foundational mathematical or physical domain, so for example:
\<^item> euklidian geometry is assumed, or \<^item> the Mordell-Lang conjecture holds,
\<^item> Newtonian (non-relativistic) physics is assumed, \<^item> euklidian geometry is assumed, or
Their acceptance is inherently outside the scope of the model \<^item> Newtonian (non-relativistic) physics is assumed,
and can only established inside certification process by Their acceptance is inherently outside the scope of the model
authority argument. and can only established inside certification process by
authority argument.
\<close> \<close>
datatype hyp_type = physical | mathematical | computational | other datatype hyp_type = physical | mathematical | computational | other
@ -384,7 +441,7 @@ doc_class hypothesis = requirement +
hyp_type :: hyp_type <= physical (* default *) hyp_type :: hyp_type <= physical (* default *)
text\<open> The following sub-class of security related hypothesis might comprise, for example: text\<open> The following sub-class of security related hypothesis might comprise, for example:
\<^item> @{term "P \<noteq> NP"}, \<^item> \<^term>\<open>P \<noteq> NP\<close>,
\<^item> or the computational hardness of certain functions \<^item> or the computational hardness of certain functions
relevant for cryptography (like prime-factorization). relevant for cryptography (like prime-factorization).
(* speculation bu, not 50128 *)\<close> (* speculation bu, not 50128 *)\<close>
@ -469,7 +526,7 @@ figure*[fig3::figure, relative_width="100",
\<open>Illustrative Development Lifecycle 1\<close> \<open>Illustrative Development Lifecycle 1\<close>
text\<open>Actually, the Figure 4 in Chapter 5: Illustrative Development Lifecycle 2 is more fidele text\<open>Actually, the Figure 4 in Chapter 5: Illustrative Development Lifecycle 2 is more fidele
to the remaining document: Software Architecture and Dediwn phases are merged, like in 7.3.\<close> to the remaining document: Software Architecture and Design phases are merged, like in 7.3.\<close>
section\<open>Software Assurance related Entities and Concepts\<close> section\<open>Software Assurance related Entities and Concepts\<close>
@ -541,8 +598,9 @@ doc_class judgement =
status :: status status :: status
is_concerned :: "role set" <= "{VER,ASR,VAL}" is_concerned :: "role set" <= "{VER,ASR,VAL}"
section\<open> Design and Test Documents \<close> section\<open> A Classification of CENELEC Reports and Documents \<close>
(* should we rename this as "report" ??? bu *)
doc_class cenelec_document = text_element + doc_class cenelec_document = text_element +
phase :: "phase" phase :: "phase"
sil :: "sil" sil :: "sil"
@ -680,7 +738,7 @@ doc_class SWADVR = cenelec_document +
phase :: "phase" <= "SADES" phase :: "phase" <= "SADES"
nlvl :: "normative_level" <= "HR" nlvl :: "normative_level" <= "HR"
invariant force_nlvl_swadvr :: "nlvl \<sigma> = HR" invariant force_nlvl_swadvr :: "nlvl \<sigma> = HR"
type_synonym software_architecture_and_design_verification_report = SWADVR type_synonym software_architecture_and_design_verification = SWADVR
doc_class SWCDS = cenelec_document + doc_class SWCDS = cenelec_document +
phase :: "phase" <= "SCDES" phase :: "phase" <= "SCDES"
@ -695,7 +753,7 @@ doc_class SWCTS = cenelec_document +
doc_class SWCDVR = cenelec_document + doc_class SWCDVR = cenelec_document +
phase :: "phase" <= "SCDES" phase :: "phase" <= "SCDES"
invariant force_nlvl_swcdvr :: "if sil \<sigma> = SIL0 then nlvl \<sigma> = R else nlvl \<sigma> = HR" invariant force_nlvl_swcdvr :: "if sil \<sigma> = SIL0 then nlvl \<sigma> = R else nlvl \<sigma> = HR"
type_synonym software_component_design_verification_report = SWCDVR type_synonym software_component_design_verification = SWCDVR
doc_class SWSCD = cenelec_document + doc_class SWSCD = cenelec_document +
phase :: "phase" <= "CInT" phase :: "phase" <= "CInT"