nicolas.meric
/
Isabelle_DOF
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

pass through miniôdo: deeper ontological reasoning, less LaTeX.

This commit is contained in:
Burkhart Wolff 2022-08-01 21:42:32 +02:00
parent 81c4ae2c13
commit 8a9684590a
3 changed files with 340 additions and 291 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -34,18 +34,21 @@ text\<open>
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, physical model of the environment, the physical and architectural model of the odometer,
but also the \<^cenelec_term>\<open>SFRS\<close> aspects including but also the \<^cenelec_term>\<open>SFRS\<close> aspects including the problem of numerical sampling and the
the problem of numerical sampling and the boundaries of efficient computations. The interplay boundaries of efficient computations. The interplay between environment and measuring-device as
between environment and measuring-device as well as the implementation problems on a platform well as the implementation problems on a platform with limited resources makes the odometer a
with limited resources makes the odometer a fairly typical \<^cenelec_term>\<open>safety\<close> critical fairly typical \<^cenelec_term>\<open>safety\<close> critical \<^cenelec_term>\<open>component\<close> of an embedded system.
\<^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 The case-study is presented in form of an \<^emph>\<open>integrated source\<close> in \<^isadof> containing all four
reports from the phases: 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_requirements\<close>, \<^ie> the \<^onto_class>\<open>SWRS\<close>
\<^item> \<^term>\<open>software_architecture_and_design\<close>, \<^ie> the \<^typ>\<open>software_design_specification\<close>(-report) (or long:\<^typ>\<open>software_requirements_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>software_architecture_and_design\<close>, \<^ie> the \<^onto_class>\<open>SWDS\<close>
\<^item> \<^term>\<open>component_implementation_and_testing\<close>, \<^ie> the \<^typ>\<open>software_component_design_verification\<close>(-report) (or long: \<^typ>\<open>software_design_specification\<close>(-report))
\<^item> \<^term>\<open>component_implementation_and_testing\<close>, \<^ie> the \<^onto_class>\<open>SWADVR\<close>
(or long: \<^typ>\<open>software_architecture_and_design_verification\<close>(-report))
\<^item> \<^term>\<open>component_implementation_and_testing\<close>, \<^ie> the \<^onto_class>\<open>SWADVR\<close>
(or long: \<^typ>\<open>software_component_design_verification\<close>(-report).)
The objective of this case study is to demonstrate deep-semantical ontologoies in The objective of this case study is to demonstrate deep-semantical ontologoies in
software developments targeting certifications, and in particular, how \<^isadof>'s software developments targeting certifications, and in particular, how \<^isadof>'s
@ -65,6 +68,7 @@ text\<open>
\<close> \<close>
section\<open>A CENELEC-conform development 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
@ -93,14 +97,18 @@ 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: \<^vs>\<open>-0.3cm\<close> particular, we need to make the following assumptions explicit: \<^vs>\<open>-0.3cm\<close>\<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> the distance between all teeth of a wheel is the same and constant, and
\<^item> the sampling rate of positions is a given constant.
text*["perfect-wheel"::assumption]
\<open>\<^item> the wheel is perfectly circular with a given, constant radius. \<^vs>\<open>-0.3cm\<close>\<close>
text*["no-slip"::assumption]
\<open>\<^item> the slip between the trains wheel and the track negligible. \<^vs>\<open>-0.3cm\<close>\<close>
text*["constant-teeth-dist"::assumption]
\<open>\<^item> the distance between all teeth of a wheel is the same and constant, and \<^vs>\<open>-0.3cm\<close>\<close>
text*["constant-sampling-rate"::assumption]
\<open>\<^item> the sampling rate of positions is a given constant.\<close>
text\<open>
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
@ -114,53 +122,49 @@ text\<open>
\<close> \<close>
subsection\<open>Capturing ``System Architecture.''\<close> subsection\<open>Capturing ``System Architecture.''\<close>
figure*["three-phase"::figure,relative_width="70",src="''figures/three-phase-odo''"]
\<open>An odometer with three sensors \<open>C1\<close>, \<open>C2\<close>, and \<open>C3\<close>.\<close>
text\<open> text\<open>
\begin{figure} The requirements analysis also contains a document \<^doc_class>\<open>SYSAD\<close>
\centering (\<^typ>\<open>system_architecture_description\<close>) that contains technical drawing of the odometer,
\includegraphics[width=.70\textwidth]{figures/three-phase-odo} a timing diagram (see \<^figure>\<open>three-phase\<close>), and tables describing the encoding of the position
\begin{picture}(0,0) for the possible signal transitions of the sensors \<open>C1\<close>, \<open>C2\<close>, and \<open>C3\<close>.
\put(-112,44){\includegraphics[width=.30\textwidth]{figures/odometer}}
\end{picture}
\caption{An odometer with three sensors \inlineisar{C1}, \inlineisar{C2}, and \inlineisar{C3}.}\label{three-phase}
\end{figure}
The requirements analysis also contains a sub-document \<^emph>\<open>system architecture description\<close>
(CENELEC notion) that contains technical drawing of the odometer, a timing diagrams
(see \autoref{three-phase}), and tables describing the encoding of the position
for the possible signal transitions of the sensors \inlineisar{C1}, \inlineisar{C2}, and $C3.$
\<close> \<close>
subsection\<open>Capturing ``System Interfaces.''\<close> 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 \<^doc_class>\<open>FnI\<close> (\<^typ>\<open>functions_and_interfaces\<close>)
(CENELEC notion) describing the technical format of the output of the odometry function. 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 \<open>N\<^sub>a\<^sub>v\<^sub>g\<close> 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 \<open>N\<^sub>a\<^sub>v\<^sub>g\<close> a parameter of the
sub-system configuration. \<close> sub-system configuration. \<close>
(*<*) (*<*)
declare_reference*["df-numerics-encshaft"::figure] declare_reference*["df-numerics-encshaft"::figure]
(*>*) (*>*)
subsection\<open>Capturing ``Required Performances.''\<close> subsection\<open>Capturing ``Required Performances.''\<close>
text\<open> text\<open>
The given analysis document is relatively implicit on the expected precision of the measurements; The given analysis document is relatively implicit on the expected precision of the measurements;
however, certain interface parameters like \inlineisar*Odometric_Position_TimeStamp* however, certain interface parameters like \<open>Odometric_Position_TimeStamp\<close>
(a counter on the number of samplings) and \inlineisar*Relative_Position* are defined by as (a counter on the number of samplings) and \<open>Relative_Position\<close> are defined by as
unsigned 32 bit integer. These definitions imply that exported constraints concerning the acceptable unsigned 32 bit integer. These definitions imply that exported constraints concerning the acceptable
time of service as well the maximum distance before a necessary reboot of the subsystem. time of service as well the maximum distance before a necessary reboot of the subsystem.
For our case-study, we assume maximum deviation of the \inlineisar*Relative_Position* to the For our case-study, we assume maximum deviation of the \<open>Relative_Position\<close> to the
theoretical distance. theoretical distance.
The requirement analysis document describes the physical environment, the architecture The requirement analysis document describes the physical environment, the architecture
of the measuring device, and the required format and precision of the measurements of the odometry of the measuring device, and the required format and precision of the measurements of the odometry
function as represented (see @{figure (unchecked) "df-numerics-encshaft"}).\<close> function as represented (see @{figure (unchecked) "df-numerics-encshaft"}).\<close>
figure*["df-numerics-encshaft"::figure,relative_width="76",src="''figures/df-numerics-encshaft''"] figure*["df-numerics-encshaft"::figure,relative_width="76",src="''figures/df-numerics-encshaft''"]
\<open>Real distance vs. discrete distance vs. shaft-encoder sequence\<close> \<open>Real distance vs. discrete distance vs. shaft-encoder sequence\<close>
subsection\<open>Capturing the ``Software Design Spec'' (Resume).\<close> subsection\<open>Capturing the ``Software Design Spec'' (Resume).\<close>
text\<open> text\<open>
\enlargethispage{\baselineskip}
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
@ -186,85 +190,94 @@ section\<open>Formal Enrichment of the Software Requirements Specification\<clos
text\<open> text\<open>
After the \<^emph>\<open>capture\<close>-phase, where we converted/integrated existing informal analysis and design After the \<^emph>\<open>capture\<close>-phase, where we converted/integrated existing informal analysis and design
documents as well as code into an integrated Isabelle document, we entered into the phase of documents as well as code into an integrated Isabelle document, we entered into the phase of
\<open>formal enrichment\<close>. For example, from the assumptions in the architecture follow \<open>formal enrichment\<close>. For example, from the assumptions in the architecture follow
the definitions: the definitions:
\begin{isar}
definition teeth_per_wheelturn::nat ("tpw") where "tpw \<equiv> SOME x. x > 0" @{theory_text [display]\<open>
definition wheel_diameter::real ("w$_d$") where "w$_d$ \<equiv> SOME x. x > 0" definition teeth_per_wheelturn::nat ("tpw") where "tpw \<equiv> SOME x. x > 0"
definition wheel_circumference::real ("w$_{\text{circ}}$") where "w$_{\text{circ}}$ \<equiv> pi * w$_d$" definition wheel_diameter::real ("w\<^sub>d") where "w\<^sub>d \<equiv> SOME x. x > 0"
definition \<delta>s$_{\text{res}}$::real where "\<delta>s$_{\text{res}}$ \<equiv> w$_{\text{circ}}$ / (2 * 3 * tpw)" definition wheel_circumference::real ("w\<^sub>0") where "w\<^sub>0 \<equiv> pi * w\<^sub>d"
\end{isar} definition \<delta>s\<^sub>r\<^sub>e\<^sub>s::real where "\<delta>s\<^sub>r\<^sub>e\<^sub>s \<equiv> w\<^sub>0 / (2 * 3 * tpw)"
Here, \inlineisar{real} refers to the real numbers as defined in the HOL-Analysis \<close>}
library, which provides concepts such as Cauchy Sequences, limits,
differentiability, and a very substantial part of classical Calculus. \inlineisar{SOME} is the Here, \<open>real\<close> refers to the real numbers as defined in the HOL-Analysis library, which provides
Hilbert choice operator from HOL; the definitions of the model parameters admit all possible positive values as uninterpreted concepts such as Cauchy Sequences, limits, differentiability, and a very substantial part of
constants. Our perfect-wheel assumption is translated into a calculation of the circumference of the classical Calculus. \<open>SOME\<close> is the Hilbert choice operator from HOL; the definitions of the
wheel, while \inlineisar{\<delta>s<bsub>res<esub>}, the resolution of the odometer, can be calculated model parameters admit all possible positive values as uninterpreted constants. Our
\<^assumption>\<open>perfect-wheel\<close> is translated into a calculation of the circumference of the
wheel, while \<open>\<delta>s\<^sub>r\<^sub>e\<^sub>s\<close>, the resolution of the odometer, can be calculated
from the these parameters. HOL-Analysis permits to formalize the fundamental physical observables: from the these parameters. HOL-Analysis permits to formalize the fundamental physical observables:
\begin{isar}
type_synonym distance_function = "real\<Rightarrow>real" @{theory_text [display]\<open>
definition Speed::"distance_function\<Rightarrow>real\<Rightarrow>real" where "Speed f \<equiv> deriv f" type_synonym distance_function = "real\<Rightarrow>real"
definition Accel::"distance_function\<Rightarrow>real\<Rightarrow>real" definition Speed::"distance_function\<Rightarrow>real\<Rightarrow>real" where "Speed f \<equiv> deriv f"
where "Accel f \<equiv> deriv (deriv f)" definition Accel::"distance_function\<Rightarrow>real\<Rightarrow>real" where "Accel f \<equiv> deriv (deriv f)"
\end{isar} \<close>}
which permits to constrain the central observable \inlineisar|distance_function| in a
which permits to constrain the central observable \<open>distance_function\<close> in a
way that they describe the space of ``normal behavior'' where we expect the odometer to produce way that they describe the space of ``normal behavior'' where we expect the odometer to produce
reliable measurements over a \inlineisar|distance_function df|. reliable measurements over a \<open>distance_function df\<close> .
The essence of the physics of the train is covered by the following definition: The essence of the physics of the train is covered by the following definition:
\begin{isar}
definition normally_behaved_distance_function :: "(real \<Rightarrow> real) \<Rightarrow> bool" @{theory_text [display]\<open>
where normally_behaved_distance_function df = definition normally_behaved_distance_function :: "(real \<Rightarrow> real) \<Rightarrow> bool"
( \<forall> t. df(t) \<in> \<real>$_{\ge 0}$ \<and> (\<forall> t \<in> \<real>$_{\le 0}$. df(t) = 0) where normally_behaved_distance_function df =
\<and> df differentiable on$_{\text{R}}$ \<and> (Speed df)differentiable on$_{\text{R}}$ ( \<forall> t. df(t) \<in> \<real>\<^sub>\<ge>\<^sub>0 \<and> (\<forall> t \<in> \<real>\<real>\<^sub>\<ge>\<^sub>0. df(t) = 0)
\<and> (Accel df)differentiable on$_{\ensuremath{R}}$ \<and> df differentiable on \<real>\<^sub>\<ge>\<^sub>0 \<and> (Speed df)differentiable on \<real>\<^sub>\<ge>\<^sub>0$
\<and> (\<forall> t. (Speed df) t \<in> {-Speed$_{\text{Max}}$ .. Speed$_{\text{Max}}$}) \<and> (Accel df)differentiable on \<real>\<^sub>\<ge>\<^sub>0
\<and> (\<forall> t. (Accel df) t \<in> {-\<bar>Accel$_{\text{Max}}$\<bar> .. \<bar>Accel$_{\text{Max}}$\<bar>})) \<and> (\<forall> t. (Speed df) t \<in> {Speed\<^sub>M\<^sub>i\<^sub>n .. Speed\<^sub>M\<^sub>a\<^sub>x})
\end{isar} \<and> (\<forall> t. (Accel df) t \<in> {Accel\<^sub>M\<^sub>i\<^sub>n .. Accel\<^sub>M\<^sub>a\<^sub>x}))
\<close>}
which constrains the distance functions in the bounds described of the informal descriptions and which constrains the distance functions in the bounds described of the informal descriptions and
states them as three-fold differentiable function in certain bounds concerning speed and acceleration. states them as three-fold differentiable function in certain bounds concerning speed and
Note that violations, in particular of the constraints on speed and acceleration, \<^emph>\<open>do\<close> occur in practice. acceleration. Note that violations, in particular of the constraints on speed and acceleration,
In such cases, the global system adapts recovery strategies that are out of the scope of our model. \<^emph>\<open>do\<close> occur in practice. In such cases, the global system adapts recovery strategies that are out
Concepts like \inlineisar+shaft_encoder_state+ (a triple with the sensor values of the scope of our model. Concepts like \<open>shaft_encoder_state\<close> (a triple with the sensor values
\inlineisar{C1}, \inlineisar{C2}, \inlineisar{C3}) were formalized as types, while tables were \<open>C1\<close>, \<open>C2\<close>, \<open>C3\<close>) were formalized as types, while tables were
defined as recursive functions: defined as recursive functions:
\enlargethispage{2\baselineskip}\begin{isar}
fun phase$_0$ :: "nat \<Rightarrow> shaft_encoder_state" where @{theory_text [display]\<open>
"phase$_0$ (0) = \<lparr> C1 = False, C2 = False, C3 = True \<rparr>" fun phase\<^sub>0 :: "nat \<Rightarrow> shaft_encoder_state" where
|"phase$_0$ (1) = \<lparr> C1 = True, C2 = False, C3 = True \<rparr>" "phase\<^sub>0 (0) = \<lparr> C1 = False, C2 = False, C3 = True \<rparr>"
|"phase$_0$ (2) = \<lparr> C1 = True, C2 = False, C3 = False\<rparr>" |"phase\<^sub>0 (1) = \<lparr> C1 = True, C2 = False, C3 = True \<rparr>"
|"phase$_0$ (3) = \<lparr> C1 = True, C2 = True, C3 = False\<rparr>" |"phase\<^sub>0 (2) = \<lparr> C1 = True, C2 = False, C3 = False\<rparr>"
|"phase$_0$ (4) = \<lparr> C1 = False, C2 = True, C3 = False\<rparr>" |"phase\<^sub>0 (3) = \<lparr> C1 = True, C2 = True, C3 = False\<rparr>"
|"phase$_0$ (5) = \<lparr> C1 = False, C2 = True, C3 = True \<rparr>" |"phase\<^sub>0 (4) = \<lparr> C1 = False, C2 = True, C3 = False\<rparr>"
|"phase$_0$ x = phase$_0$(x - 6)" |"phase\<^sub>0 (5) = \<lparr> C1 = False, C2 = True, C3 = True \<rparr>"
definition Phase ::"nat\<Rightarrow>shaft_encoder_state" where Phase(x) = phase$_0$(x-1) |"phase\<^sub>0 x = phase\<^sub>0(x - 6)"
\end{isar} definition Phase ::"nat\<Rightarrow>shaft_encoder_state" where Phase(x) = phase\<^sub>0(x-1)
We now define shaft encoder sequences as \<close>}
translations of distance functions:
\begin{isar} We now define shaft encoder sequences as translations of distance functions:
definition encoding::"distance_function\<Rightarrow>nat\<Rightarrow>real\<Rightarrow>shaft_encoder_state"
where "encoding df init$_{\text{pos}}$ \<equiv> \<lambda>x. Phase(nat\<lfloor>df(x) / \<delta>s$_{\text{res}}$\<rfloor> + init$_{\text{pos}}$)" @{theory_text [display]\<open>
\end{isar} definition encoding::"distance_function\<Rightarrow>nat\<Rightarrow>real\<Rightarrow>shaft_encoder_state"
where \inlineisar+init$_{\text{pos}}$+ is the initial position of the wheel. where "encoding df init\<^sub>p\<^sub>o\<^sub>s \<equiv> \<lambda>x. Phase(nat\<lfloor>df(x) / \<delta>s\<^sub>r\<^sub>e\<^sub>s\<rfloor> + init\<^sub>p\<^sub>o\<^sub>s)"
\inlineisar+sampling+'s were constructed from encoding sequences over discretized time points: \<close>}
\begin{isar}
definition $\!\!$sampling::"distance$\!$_function\<Rightarrow>nat\<Rightarrow>real\<Rightarrow>nat\<Rightarrow>shaft$\!$_encoder$\!$_state" where \<open>init\<^sub>p\<^sub>o\<^sub>s\<close> is the initial position of the wheel.
where "sampling df init$_{\text{pos}}$ \<delta>t \<equiv> \<lambda>n::nat. encoding df init$_{\text{pos}}$ (n * \<delta>t)" \<open>sampling\<close>'s were constructed from encoding sequences over discretized time points:
\end{isar}
The sampling interval \inlineisar+\<delta>t+ (the inverse of the sampling frequency) is a critical @{theory_text [display]\<open>
definition sampling::"distance_function\<Rightarrow>nat\<Rightarrow>real\<Rightarrow>nat\<Rightarrow>shaft_encoder_state"
where "sampling df init\<^sub>p\<^sub>o\<^sub>s \<delta>t \<equiv> \<lambda>n::nat. encoding df initinit\<^sub>p\<^sub>o\<^sub>s (n * \<delta>t)"
\<close>}
parameter of the configuration of a system. parameter of the configuration of a system.
Finally, we can formally define the required performances. From the interface description Finally, we can formally define the required performances. From the interface description
and the global model parameters such as wheel diameter, the number of teeth per wheel, the sampling and the global model parameters such as wheel diameter, the number of teeth per wheel, the sampling
frequency etc., we can infer the maximal time of service as well the maximum distance the frequency etc., we can infer the maximal time of service as well the maximum distance the
device can measure. device can measure.
As an example configuration, choosing 1m for As an example configuration, choosing 1m for
\inlineisar+w$_d$+, 100 for \inlineisar+tpw+, 80km/h \inlineisar+Speed$_{\text{Max}}$+, \<open>w\<^sub>d\<close>, 100 for \<open>tpw\<close>, 80km/h \<open>Speed\<^sub>M\<^sub>a\<^sub>x\<close>,
and 14400Hz for the sampling frequency, results in an odometer resolution of 2.3mm, and 14400Hz for the sampling frequency, results in an odometer resolution of 2.3mm,
a maximum distance of 9878km, and a maximal system up-time of 123.4 hours. a maximum distance of 9878km, and a maximal system up-time of 123.4 hours.
The required precision of an odometer can be defined by a constant describing The required precision of an odometer can be defined by a constant describing
the maximally allowed difference between \inlineisar+df(n*\<delta>t)+ and the maximally allowed difference between \<open>df(n*\<delta>t)\<close> and
\inlineisar+sampling df init$_{\text{pos}}$ \<delta>t n+ for all \inlineisar+init$_{\text{pos}}$ \<in>{0..5}+. \<open>sampling df init\<^sub>p\<^sub>o\<^sub>s \<delta>t n\<close> for all \<open>init\<^sub>p\<^sub>o\<^sub>s \<in>{0..5}\<close>.
\<close> \<close>
(*<*) (*<*)
ML\<open>val two_thirty2 = 1024 * 1024 * 1024 * 4; ML\<open>val two_thirty2 = 1024 * 1024 * 1024 * 4;
@ -274,41 +287,50 @@ ML\<open>val two_thirty2 = 1024 * 1024 * 1024 * 4;
section*[verific::technical]\<open>Verification of the Software Requirements Specification\<close> section*[verific::technical]\<open>Verification of the Software Requirements Specification\<close>
text\<open>The original documents contained already various statements that motivate certain safety text\<open>The original documents contained already various statements that motivate certain safety
properties of the device. For example, the \inlineisar+Phase+-table excludes situations in which properties of the device. For example, the \<open>Phase\<close>-table excludes situations in which
all sensors \inlineisar{C1}, \inlineisar{C2}, and \inlineisar{C3} are all ``off'' or situations in all sensors \<open>C1\<close>, \<open>C2\<close>, and \<open>C3\<close> are all ``off'' or situations in
which sensors are ``on,'' reflecting a physical or electrical error in the odometer. It can be which sensors are ``on,'' reflecting a physical or electrical error in the odometer. It can be
shown by a very small Isabelle case-distinction proof that this safety requirement follows indeed from the shown by a very small Isabelle case-distinction proof that this safety requirement follows indeed
above definitions: from the above definitions:
\begin{isar}
lemma Encoder_Property_1:(C1(Phase x) \<and> C2(Phase x) \<and> C3(Phase x))=False
proof (cases x)
case 0 then show ?thesis by (simp add: Phase_def)
next
case (Suc n) then show ?thesis
by(simp add: Phase_def,rule_tac n = n in cycle_case_split,simp_all)
qed
\end{isar}
for all positions \inlineisar+x+. Similarly, it is proved that the table is indeed
cyclic: \inlineisar+ phase$_0$ x = phase$_0$(x mod 6)+ and locally injective:
\inlineisar+\<forall>x<6. \<forall>y<6. phase$_0$ x = phase$_0$ y \<longrightarrow> x = y+.
These lemmas, building the ``theory of an odometer,'' culminate in a theorem
that we would like to present in more detail.
\begin{isar}
theorem minimal_sampling :
assumes * : normally_behaved_distance_function df
and ** : \<delta>t * Speed$_{\text{Max}}$ < \<delta>s$_{\text{res}}$
shows \<forall> \<delta>X\<le>\<delta>t. 0<\<delta>X \<longrightarrow>
\<exists>f. retracting (f::nat\<Rightarrow>nat) \<and>
sampling df init$_{\text{pos}}$ \<delta>X = (sampling df init$_{\text{pos}}$ \<delta>t) o f
\end{isar} @{theory_text [display]\<open>
This theorem states for \inlineisar+normally_behaved_distance_function+s that there is lemma Encoder_Property_1:(C1(Phase x) \<and> C2(Phase x) \<and> C3(Phase x))=False
proof (cases x)
case 0 then show ?thesis by (simp add: Phase_def)
next
case (Suc n) then show ?thesis
by(simp add: Phase_def,rule_tac n = n in cycle_case_split,simp_all)
qed
\<close>}
for all positions \<open>x\<close>. Similarly, it is proved that the table is indeed cyclic:
\<open>phase\<^sub>0 x = phase\<^sub>0(x mod 6)\<close>
and locally injective:
\<open>\<forall>x<6. \<forall>y<6. phase\<^sub>0 x = phase\<^sub>0 y \<longrightarrow> x = y\<close>
These lemmas, building the ``theory of an odometer,'' culminate in a theorem
that we would like to present in more detail.
@{theory_text [display]\<open>
theorem minimal_sampling :
assumes * : normally_behaved_distance_function df
and ** : \<delta>t * Speed\<^sub>M\<^sub>a\<^sub>x < \<delta>s\<^sub>r\<^sub>e\<^sub>s
shows \<forall> \<delta>X\<le>\<delta>t. 0<\<delta>X \<longrightarrow>
\<exists>f. retracting (f::nat\<Rightarrow>nat) \<and>
sampling df init\<^sub>p\<^sub>o\<^sub>s \<delta>X = (sampling df init\<^sub>p\<^sub>o\<^sub>s \<delta>t) o f
\<close>}
This theorem states for \<open>normally_behaved_distance_function\<close>s that there is
a minimal sampling frequency assuring the safety of the measurements; samplings on a minimal sampling frequency assuring the safety of the measurements; samplings on
some \inlineisar$df$ gained from this minimal sampling frequency can be ``pumped up'' some \<open>df\<close> gained from this minimal sampling frequency can be ``pumped up''
to samplings of these higher sampling frequencies; they do not contain more information. to samplings of these higher sampling frequencies; they do not contain more information.
Of particular interest is the second assumption, labelled ``\inlineisar|**|,'' which Of particular interest is the second assumption, labelled ``\<open>**\<close>'' which
establishes a lower bound from \inlineisar+w$_{\text{circ}}$+, \inlineisar+tpw+, establishes a lower bound from \<open>w\<^sub>0\<close>, \<open>tpw\<close>,
\inlineisar+Speed$_{\text{Max}}$+ for the sampling frequency. Methodologically, this represents \<open>Speed\<^sub>M\<^sub>a\<^sub>x\<close> for the sampling frequency. Methodologically, this represents
an exported constraint that can not be represented \<^emph>\<open>inside\<close> the design model: it means that the an exported constraint that can not be represented \<^emph>\<open>inside\<close> the design model: it means that the
computations have to be fast enough on the computing platform in order to assure that the computations have to be fast enough on the computing platform in order to assure that the
calculations are valid. It was in particular this exported constraint that forced us to give up calculations are valid. It was in particular this exported constraint that forced us to give up
@ -322,6 +344,7 @@ standard~@{cite "bsi:50128:2014"}, 7.2.4.22 and are usually addressed in an own
\<close> \<close>
chapter*[ontomodeling::text_section]\<open>The CENELEC 50128 Ontology\<close> chapter*[ontomodeling::text_section]\<open>The CENELEC 50128 Ontology\<close>
text\<open> text\<open>
Modeling an ontology from a semi-formal text such as~@{cite"bsi:50128:2014"} is, Modeling an ontology from a semi-formal text such as~@{cite"bsi:50128:2014"} is,
like any other modeling activity, not a simple one-to-one translation of some like any other modeling activity, not a simple one-to-one translation of some
@ -333,125 +356,144 @@ text\<open>
section*[lhf::text_section] section*[lhf::text_section]
\<open>Tracking Concepts and Definitions\<close> \<open>Tracking Concepts and Definitions\<close>
text\<open> 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 \<^cenelec_term>\<open>traceability\<close> in paragraphs 3.1.46 (a notion referenced 31 times in
which we translated directly into: the standard), which we translated directly into:
\begin{isar}
Definition*[traceability::concept]<open> degree to which relationship @{theory_text [display]\<open>
can be established between two or more products of a development Definition*[traceability, short_name="''traceability''"]
process, especially those having a predecessor/successor or \<open>degree to which relationship can be established between two or more products of a
master/subordinate relationship to one another. <close> development process, especially those having a predecessor/successor or
\end{isar} master/subordinate relationship to one another.\<close>
In the integrated source of the odometry study, we can reference in a text element to this \<close>}
In the integrated source of the odometry study, we can reference in a text element to this
concept as follows: concept as follows:
\begin{isar}
text*[...]<open> ... to assure <@>{concept traceability} for @{theory_text [display]\<open>
<@>{requirement bitwiseAND}, we prove ... <close> text*[...]\<open> ... to assure <@>{cenelec_term traceability} for
\end{isar} <@>{requirement bitwiseAND}, we prove ... \<close>
The presentation of this document element inside \isadof is immediately hyperlinked against the \<close>}
\inlineisar+Definition*+ element shown above; this serves as documentation of
\<^isadof> also uses the underlying ontology to generate the navigation markup inside the IDE, \<^ie>
the presentation of this document element inside \<^isadof> is immediately hyperlinked against the
@{theory_text \<open> Definition* \<close>}-element shown above; this serves as documentation of
the standard for the development team working on the integrated source. The PDF presentation the standard for the development team working on the integrated source. The PDF presentation
of such links depends on the actual configurations for the document generation; We will explain of such links depends on the actual configurations for the document generation; We will explain
this later. this later.
CENELEC foresees also a number of roles, phases, safety integration levels, etc., which were CENELEC foresees also a number of roles, phases, safety integration levels, etc., which were
directly translated into HOL enumeration types usable in ontological concepts of ODL. directly translated into HOL enumeration types usable in ontological concepts of ODL.
\begin{isar}
datatype role = @{theory_text [display]\<open>
PM (* Program Manager *) | RQM (* Requirements Manager *) datatype role =
| DES (* Designer *) | IMP (* Implementer *) | PM (* Program Manager *) | RQM (* Requirements Manager *)
| VER (* Verifier *) | VAL (* Validator *) | ... | DES (* Designer *) | IMP (* Implementer *) |
datatype phase = | VER (* Verifier *) | VAL (* Validator *) | ...
SYSDEV_ext (* System Development *) | SPl (* Software Planning *) datatype phase =
| SR (* Software Requirement *) | SA (* Software Architecture *) SYSDEV_ext (* System Development *) | SPl (* Software Planning *)
| SDES (* Software Design *) | ... | SR (* Software Requirement *) | SA (* Software Architecture *)
\end{isar} | SDES (* Software Design *) | ...
Similarly, we can formalize the Table A.5: Verification and Testing of @{cite "bsi:50128:2014"}: \<close>}
a classification of \<^emph>\<open>verification and testing techniques\<close>:
\begin{isar} Similarly, we can formalize the Table A.5: Verification and Testing of @{cite "bsi:50128:2014"}:
datatype vnt_technique = a classification of \<^emph>\<open>verification and testing techniques\<close>:
@{theory_text [display]\<open>
datatype vnt_technique =
formal_proof "thm list" | stat_analysis formal_proof "thm list" | stat_analysis
| dyn_analysis dyn_ana_kind | ... | dyn_analysis dyn_ana_kind | ...
\end{isar} \<close>}
In contrast to the standard, we can parameterize \inlineisar+formal_proof+ with a list of
theorems, an entity known in the Isabelle kernel. Here, \isadof assures for text elements In contrast to the standard, we can parameterize \<open>formal_proof\<close> with a list of
theorems, an entity known in the Isabelle kernel. Here, \<^isadof> assures for text elements
annotated with theorem names, that they refer indeed to established theorems in the Isabelle annotated with theorem names, that they refer indeed to established theorems in the Isabelle
environment. Additional checks could be added to make sure that these theorems have a particular environment. Additional checks could be added to make sure that these theorems have a particular
form. form.
While we claim that this possibility to link to theorems (and test-results) is unique in the While we claim that this possibility to link to theorems (and test-results) is unique in the
world of systems attempting to assure traceability, referencing a particular (proven) theorem is world of systems attempting to assure \<^cenelec_term>\<open>traceability\<close>, referencing a particular
definitively not sufficient to satisfy the claimed requirement. Human evaluators will always have (proven) theorem is definitively not sufficient to satisfy the claimed requirement. Human
to check that the provided theorem \<open>adequately\<close> represents the claim; we do not in the slightest evaluators will always have to check that the provided theorem \<open>adequately\<close> represents the claim;
suggest that their work is superfluous. Our framework allows to statically check that tests or proofs we do not in the slightest suggest that their work is superfluous. Our framework allows to
have been provided, at places where the ontology requires them to be, and both assessors and developers statically check that tests or proofs have been provided, at places where the ontology requires
can rely on this check and navigate through related information easily. It does not guarantee that them to be, and both assessors and developers can rely on this check and navigate through
intended concepts for, \<^eg>, safety or security have been adequately modeled. related information easily. It does not guarantee that intended concepts for, \<^eg>, safety
or security have been adequately modeled.
\<close> \<close>
section*[moe::text_section] section*[moe::text_section]
\<open>Major Ontological Entities: Requirements and Evidence\<close> \<open>Major Ontological Entities: Requirements and Evidence\<close>
text\<open> text\<open>
We introduce central concept of a \<^emph>\<open>requirement\<close> as an ODL \inlineisar*doc_class* We introduce central concept of a \<^emph>\<open>requirement\<close> as an ODL \<^theory_text>\<open>doc_class\<close>
based on some generic basic library \inlineisar*text_element* providing basic layout attributes. based on the generic basic library \<^doc_class>\<open>text_element\<close> providing basic layout attributes.
\begin{isar}
doc_class requirement = text_element + @{theory_text [display]\<open>
long_name :: "string option" doc_class requirement = text_element +
is_concerned :: "role set" long_name :: "string option"
\end{isar} is_concerned :: "role set"
where the \inlineisar*roles* are exactly the ones defined in the previous section and represent \<close>}
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 the groups of stakeholders in the CENELEC process. Therefore, the \<open>is_concerned\<close>-attribute
presentation, \<^eg>, different presentation styles of the allows expressing who ``owns'' this text-element. \<^isadof> supports a role-based
integrated source may decide to highlight, to omit, to defer into an annex, text entities presentation, \<^eg>, different presentation styles of the integrated source may decide to highlight,
according to the role-set. to omit, to defer into an annex, text entities according to the role-set.
Since ODL supports single inheritance, we can express sub-requirements and therefore a style Since ODL supports single inheritance, we can express sub-requirements and therefore a style
of requirement decomposition as advocated in GSN~@{cite "kelly.ea:goal:2004"}: of requirement decomposition as advocated in GSN~@{cite "kelly.ea:goal:2004"}:
\begin{isar}
doc_class sub_requirement = @{theory_text [display]\<open>
decomposes :: "requirement" doc_class sub_requirement =
relates_to :: "requirement set" decomposes :: "requirement"
\end{isar}\<close> relates_to :: "requirement set"
\<close>}
\<close>
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.: \<^vs>\<open>-0.15cm\<close> 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} \<^vs>\<open>-0.15cm\<close> \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
standard, but they are neither explained nor even listed in the general glossary. However, the The terms \<^onto_class>\<open>judgement\<close> based on \<^term>\<open>evidence\<close> are used as a kind of leitmotif throughout
standard is fairly explicit on the \<^emph>\<open>phase\<close>s and the organizational roles that different stakeholders the CENELEC standard, but they are neither explained nor even listed in the general glossary.
should have in the process. Our version to express this key concept of judgment, \<^eg>, by However, the standard is fairly explicit on the \<^emph>\<open>phase\<close>s and the organizational roles that
the following concept: different stakeholders should have in the process. Our version to express this key concept of
\begin{isar} \<^onto_class>\<open>judgement\<close> , \<^eg>, by the following concept:
doc_class judgement =
refers_to :: requirement @{theory_text [display]\<open>
evidence :: "vnt_technique list" doc_class judgement =
status :: status refers_to :: requirement
is_concerned :: "role set" <= "{VER,ASR,VAL}" evidence :: "vnt_technique list"
\end{isar} status :: status
is_concerned :: "role set" <= "{VER,ASR,VAL}"
\<close>}
As one can see, the role set is per default set to the verification team, the assessors and the As one can see, the role set is per default set to the verification team, the assessors and the
validation team. validation team.
There are different views possible here: an alternative would be to define \inlineisar+evidence+ There are different views possible here: an alternative would be to define \<^term>\<open>evidence\<close>
as ontological concept with \inlineisar+vnt_technique+'s (rather than an attribute of judgement) as ontological concept with \<^typ>\<open>vnt_technique\<close>'s (rather than an attribute of judgement)
and consider the basis of judgments as a relation between requirements and relation: and consider the basis of a summary containing the relation between requirements and relation:
\begin{isar}
doc_class judgement = @{theory_text [display]\<open>
based_on :: "(requirement \<times> evidence) set" doc_class summary =
status :: status based_on :: "(requirement \<times> evidence) set"
is_concerned :: "role set" <= "{VER,ASR,VAL}" status :: status
\end{isar} is_concerned :: "role set" <= "{VER,ASR,VAL}"
\<close>}
More experimentation will be needed to find out what kind of ontological modeling is most More experimentation will be needed to find out what kind of ontological modeling is most
adequate for developers in the context of \isadof. adequate for developers in the context of \isadof.
@ -463,60 +505,66 @@ text\<open>From the variety of different possibilities for adding CENELEC annota
integrated source, we will, in the following, point out three scenarios.\<close> integrated source, we will, in the following, point out three scenarios.\<close>
subsection\<open>Internal Verification of Claims in the Requirements Specification.\<close> subsection\<open>Internal Verification of Claims in the Requirements Specification.\<close>
text\<open>In our case, the SR-team early on detected a property necessary text\<open>In our case, the \<^term>\<open>SR\<close>-team early on detected a property necessary
for error-detection of the device (c.f. @{technical verific}): for error-detection of the device (c.f. @{technical verific}):
\enlargethispage{2\baselineskip}\begin{isar}
text*[encoder_props::requirement]<open> The requirement specification team ... @{theory_text [display]\<open>
C1 & C2 & C3 = 0 (bitwise logical AND operation) text*[encoder_props::requirement]\<open> The requirement specification team identifies the property:
C1 | C2 | C3 = 1 (bitwise logical OR operation) <close> C1 & C2 & C3 = 0 (bitwise logical AND operation)
\end{isar} C1 | C2 | C3 = 1 (bitwise logical OR operation) \<close>
\<close>}
After the Isabelle proofs shown in @{technical verific}, we can either register the theorems After the Isabelle proofs shown in @{technical verific}, we can either register the theorems
directly in an evidence statement: directly in an evidence statement:
\begin{isar} @{theory_text [display]\<open>
text*[J1::judgement, refers_to="<@>{docitem <open>encoder_props<close>}", text*[J1::judgement, refers_to="@{docitem <open>encoder_props<close>}",
evidence="[formal_proof[<@>{thm <open>Encoder_Property_1<close>}, evidence="[formal_proof[@{thm <open>Encoder_Property_1<close>},
<@>{thm <open>Encoder_Property_2<close>}]]"] @{thm <open>Encoder_Property_2<close>}]]"]
<open>The required encoder properties are in fact verified to be consistent \<open>The required encoder properties are in fact verified to be consistent
with the formalization of <@>{term "phase$_0$"}.<close> with the formalization of @{term "phase\<^sub>0"}.\<close>
\end{isar} \<close>}
The references \inlineisar|<@>{...}|, called antiquotation, allow us not only to reference to
The references \<open>@{...}\<close>, 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>
text\<open>By definition, the main purpose of the requirement specification is the
identification of the safety requirements. As an example, we state the required precision of an
odometric function: for any normally behaved distance function \inlineisar+df+, and any representable
and valid sampling sequence that can be constructed for \inlineisar+df+, we require that the
difference between the physical distance and distance calculable from the
@{term Odometric_Position_Count} is bound by the minimal resolution of the odometer.
\begin{isar}
text*[R5::safety_requirement]<open>We can now state ... <close>
definition
Odometric_Position_Count_precise::(shaft_encoder_state list\<Rightarrow>output)\<Rightarrow>bool
where Odometric_Position_Count_precise odofunction \<equiv>
(\<forall> df. \<forall>S. normally_behaved_distance_function df
\<longrightarrow> representable S
\<longrightarrow> valid_sampling S df
\<longrightarrow> (let pos = uint(Odometric_Position_Count(odofunction S))
in \<bar>df((length S - 1)*\<delta>t$_{\text{odo}}$) - (\<delta>s$_{\text{res}}$ * pos)\<bar> \<le> \<delta>s$_{\text{res}}$))
update_instance*[R5::safety_requirement, text\<open>By definition, the main purpose of the requirement specification is the identification of
formal_definition:="[<@>{thm <open>Odometric_Position_Count_precise_def<close>}]"] the safety requirements. As an example, we state the required precision of an odometric function:
\end{isar} for any normally behaved distance function \<open>df\<close>, and any representable and valid
By \inlineisar+update_instance*+, we book the property \inlineisar+Position_Count_precise_def+ as sampling sequence that can be constructed for \<open>df\<close>, we require that the difference
\inlineisar+safety_requirement+, a specific sub-class of \inlineisar+requirement+s between the physical distance and distance calculable from the @{term Odometric_Position_Count}
is bound by the minimal resolution of the odometer.
@{theory_text [display]\<open>
text*[R5::safety_requirement]\<open>We can now state ... \<close>
definition Odometric_Position_Count_precise :: "(shaft_encoder_state list\<Rightarrow>output)\<Rightarrow>bool"
where "Odometric_Position_Count_precise odofunction \<equiv>
(\<forall> df. \<forall>S. normally_behaved_distance_function df
\<longrightarrow> representable S
\<longrightarrow> valid_sampling S df
\<longrightarrow> (let pos = uint(Odometric_Position_Count(odofunction S))
in \<bar>df((length S - 1)*\<delta>t\<^sub>o\<^sub>d\<^sub>o) - (\<delta>s\<^sub>r\<^sub>e\<^sub>s * pos)\<bar> \<le> \<delta>s\<^sub>r\<^sub>e\<^sub>s))"
update_instance*[R5::safety_requirement,
formal_definition:="[@{thm \<open>Odometric_Position_Count_precise_def\<close>}]"]
\<close>}
By \<^theory_text>\<open>update_instance*\<close>, we book the property \<open>Position_Count_precise_def\<close> as
\<^onto_class>\<open>safety_requirement\<close>, a specific sub-class of \<^onto_class>\<open>requirement\<close>s
requesting a formal definition in Isabelle.\<close> requesting a formal definition in Isabelle.\<close>
subsection\<open>Exporting Derived Requirements.\<close> subsection\<open>Exporting Derived Requirements.\<close>
text\<open>Finally, we discuss the situation where the verification team discovered a critical side-condition text\<open>Finally, we discuss the situation where the verification team discovered a critical side-condition
for a major theorem necessary for the safety requirements; this was in our development the case for for a major theorem necessary for the safety requirements; this was in our development the case for
the condition labelled ``\inlineisar|**|'' in @{docitem verific}. The current CENELEC standard clearly separates the condition labelled ``\<open>**\<close>'' in @{docitem verific}. The current CENELEC standard clearly separates
``requirement specifications'' from ``verification reports,'' which is probably motivated ``requirement specifications'' from ``verification reports,'' which is probably motivated
by the overall concern of organizational separation and of document consistency. While this by the overall concern of organizational separation and of document consistency. While this
document organization is possible in \isadof, it is in our experience often counter-productive document organization is possible in \<^isadof>, it is in our experience often counter-productive
in practice: organizations tend to defend their documents because the impact of changes is more and more in practice: organizations tend to defend their documents because the impact of changes is more and more
difficult to oversee. This effect results in a dramatic development slow-down and an increase of difficult to oversee. This effect results in a dramatic development slow-down and an increase of
costs. Furthermore, these barriers exclude situations where developers perfectly know, for example, costs. Furthermore, these barriers exclude situations where developers perfectly know, for example,
@ -531,58 +579,58 @@ different PDF versions and for each version, document specific consistency guara
automatically enforced. automatically enforced.
In our case study, we define this condition as predicate, declare an explanation of it as In our case study, we define this condition as predicate, declare an explanation of it as
\inlineisar+SRAC+ (CENELEC for: safety-related application condition; ontologically, this is a \<^onto_class>\<open>SRAC\<close> (CENELEC for: safety-related application condition; ontologically, this is a
derived class from \inlineisar+requirement+.) and add the definition of the predicate into the derived class from \<^onto_class>\<open>requirement\<close>.) and add the definition of the predicate into the
document instance as described in the previous section.\<close> document instance as described in the previous section.\<close>
text\<open>\appendix\<close>
chapter\<open>Appendix\<close> chapter\<open>Appendix\<close>
text\<open> text\<open>
\<^item> \inlineisar|<@>{thm refl}|: @{thm refl} \<^item> \<open>@{thm refl}\<close> : @{thm refl}
\<^item> \inlineisar|<@>{thm [source] refl}|: @{thm [source] refl} \<^item> \<open>@{thm [source] refl}\<close> : @{thm [source] refl}
\<^item> \inlineisar|<@>{thm[mode=Rule] conjI}|: @{thm[mode=Rule] conjI} \<^item> \<open>@{thm[mode=Rule] conjI}\<close> : @{thm[mode=Rule] conjI}
\<^item> \inlineisar|<@>{file "mini_odo.thy"}|: @{file "mini_odo.thy"} \<^item> \<open>@{file "mini_odo.thy"}\<close> : @{file "mini_odo.thy"}
\<^item> \inlineisar|<@>{value "3+4::int"}|: @{value "3+4::int"} \<^item> \<open>@{value "3+4::int"}}\<close> : @{value "3+4::int"}
\<^item> \inlineisar|<@>{const hd}|: @{const hd} \<^item> \<open>@{const hd}\<close> : @{const hd}
\<^item> \inlineisar|<@>{theory HOL.List}|: @{theory HOL.List} \<^item> \<open>@{theory HOL.List}\<close> : @{theory HOL.List}
\<^item> \inlineisar|<@>{term "3"}|: @{term "3"} \<^item> \<open>@{term "3"}\<close> : @{term "3"}
\<^item> \inlineisar|<@>{type bool}|: @{type bool} \<^item> \<open>@{type bool}\<close> : @{type bool}
\<^item> \inlineisar|<@>{term [show_types] "f x = a + x"}|: @{term [show_types] "f x = a + x"} \<^item> \<open>@{thm term [show_types] "f x = a + x"}\<close> : @{term [show_types] "f x = a + x"}
\<close> \<close>
text\<open>Examples for declaration of typed doc-items "assumption" and "hypothesis", text\<open>Examples for declaration of typed doc-classes "assumption" (sic!) and "hypothesis" (sic!!),
concepts defined in the underlying ontology @{theory "Isabelle_DOF.CENELEC_50128"}. \<close> concepts defined in the underlying ontology @{theory "Isabelle_DOF.CENELEC_50128"}. \<close>
text*[ass2::assumption, long_name="Some ''assumption one''"] \<open> The subsystem Y is safe. \<close> text*[ass2::assumption, long_name="Some ''assumption one''"] \<open> The subsystem Y is safe. \<close>
text*[hyp1::hypothesis] \<open> P not equal NP \<close> text*[hyp1::hypothesis] \<open> P not equal NP \<close>
text\<open>A real example fragment from a larger project, declaring a text-element as a text\<open>
"safety-related application condition", a concept defined in the A real example fragment from a larger project, declaring a text-element as a
@{theory "Isabelle_DOF.CENELEC_50128"} ontology:\<close> "safety-related application condition", a concept defined in the
@{theory "Isabelle_DOF.CENELEC_50128"} ontology:\<close>
text*[hyp2::hypothesis]\<open>Under the assumption @{assumption \<open>ass2\<close>} we establish the following: ... \<close> text*[hyp2::hypothesis]\<open>Under the assumption @{assumption \<open>ass2\<close>} we establish the following: ... \<close>
text*[ass122::SRAC, long_name="Some ''ass122''"] \<open> The overall sampling frequence of the odometer text*[ass122::SRAC, long_name="Some ''ass122''"]
subsystem is therefore 14 khz, which includes sampling, computing and \<open> The overall sampling frequence of the odometer subsystem is therefore 14 khz,
result communication times... \<close> which includes sampling, computing and result communication times... \<close>
text*[ass123::SRAC] \<open> The overall sampling frequence of the odometer text*[ass123::SRAC]
subsystem is therefore 14 khz, which includes sampling, computing and \<open> The overall sampling frequence of the odometer subsystem is therefore 14 khz,
result communication times... \<close> which includes sampling, computing and result communication times... \<close>
text*[ass124::EC, long_name="Some ''ass124''"] \<open> The overall sampling frequence of the odometer text*[ass124::EC, long_name="Some ''ass124''"]
subsystem is therefore 14 khz, which includes sampling, computing and \<open> The overall sampling frequence of the odometer subsystem is therefore 14 khz,
result communication times... \<close> which includes sampling, computing and result communication times... \<close>
text*[t10::test_result] \<open> This is a meta-test. This could be an ML-command text*[t10::test_result]
that governs the external test-execution via, eg., a makefile or specific calls \<open> This is a meta-test. This could be an ML-command that governs the external
to a test-environment or test-engine. \<close> test-execution via, \<^eg>, a makefile or specific calls to a test-environment or test-engine. \<close>
text\<open>Finally some examples of references to doc-items, i.e. text-elements with declared text
meta-information and status. \<close> \<open> Finally some examples of references to doc-items, i.e. text-elements
with declared meta-information and status. \<close>
text \<open> As established by @{test_result (unchecked) \<open>t10\<close>}, text \<open> As established by @{test_result (unchecked) \<open>t10\<close>},
@{test_result (define) \<open>t10\<close>} \<close> @{test_result (define) \<open>t10\<close>} \<close>
text \<open> the @{test_result \<open>t10\<close>} text \<open> the @{test_result \<open>t10\<close>}
@ -590,10 +638,10 @@ text \<open> the @{test_result \<open>t10\<close>}
text \<open> represent a justification of the safety related applicability text \<open> represent a justification of the safety related applicability
condition @{SRAC \<open>ass122\<close>} aka exported constraint @{EC \<open>ass122\<close>}.\<close> condition @{SRAC \<open>ass122\<close>} aka exported constraint @{EC \<open>ass122\<close>}.\<close>
(* due to notational conventions for antiquotations, one may even write: *) text \<open> due to notational conventions for antiquotations, one may even write:
(* CRASHES WITH LaTeX backend error. *)
text \<open> represent a justification of the safety related applicability "represent a justification of the safety related applicability
condition \<^SRAC>\<open>ass122\<close> aka exported constraint \<^EC>\<open>ass122\<close>.\<close> condition \<^SRAC>\<open>ass122\<close> aka exported constraint \<^EC>\<open>ass122\<close>."\<close>
(*<*) (*<*)

2
src/DOF/Isa_DOF.thy
View File

@ -2462,7 +2462,7 @@ fun trace_attr_2_ML ctxt (oid:string,pos) =
fun compute_cid_repr ctxt cid pos = fun compute_cid_repr ctxt cid pos =
if DOF_core.is_defined_cid_local cid ctxt then Const(cid,dummyT) if DOF_core.is_defined_cid_local cid ctxt then Const(cid,dummyT)
else ISA_core.err "Undefined Class Id" pos else ISA_core.err ("Undefined Class Identifier:"^cid) pos
local local

15
src/ontologies/technical_report/technical_report.thy
View File

@ -38,15 +38,16 @@ doc_class "code" = technical +
checked :: bool <= "False" checked :: bool <= "False"
caption :: "string" <= "''''" caption :: "string" <= "''''"
typ code
text\<open>The @{doc_class "code"} is a general stub for free-form and type-checked code-fragments text\<open>The \<^doc_class>\<open>code\<close> is a general stub for free-form and type-checked code-fragments such as:
such as: \<^enum> SML code
\<^enum> SML code \<^enum> bash code
\<^enum> bash code \<^enum> isar code (although this might be an unwanted concurrence
\<^enum> isar code (although this might be an unwanted concurrence to the Isabelle standard cartouche) to the Isabelle standard cartouche)
\<^enum> C code. \<^enum> C code.
it is intended that later refinements of this "stub" as done in \<^verbatim>\<open>Isabelle_C\<close> which come with their It is intended that later refinements of this "stub" as done in \<^verbatim>\<open>Isabelle_C\<close> which come with their
own content checking and, of course, presentation styles. own content checking and, of course, presentation styles.
\<close> \<close>