From 81c4ae2c13132fdedceb96870a7cfc982ea2d3c3 Mon Sep 17 00:00:00 2001 From: Burkhart Wolff Date: Mon, 1 Aug 2022 15:53:33 +0200 Subject: [PATCH 1/3] first version of new commands onto_class // doc_class --- examples/CENELEC_50128/mini_odo/mini_odo.thy | 65 ++++-- src/DOF/Isa_DOF.thy | 22 ++ .../CENELEC_50128/CENELEC_50128.thy | 216 +++++++++++------- 3 files changed, 202 insertions(+), 101 deletions(-) diff --git a/examples/CENELEC_50128/mini_odo/mini_odo.thy b/examples/CENELEC_50128/mini_odo/mini_odo.thy index f3b5e92..3bd7021 100644 --- a/examples/CENELEC_50128/mini_odo/mini_odo.thy +++ b/examples/CENELEC_50128/mini_odo/mini_odo.thy @@ -19,6 +19,8 @@ theory "Isabelle_DOF.technical_report" begin declare[[strict_monitor_checking=true]] +define_shortcut* dof \ \\dof\ + isadof \ \\isadof{}\ (*>*) title*[title::title]\The CENELEC 50128 Ontology\ @@ -27,14 +29,31 @@ subtitle*[subtitle::subtitle]\Case Study: An Odometer-Subsystem\ chapter*[casestudy::technical]\An Odometer-Subsystem\ text\ 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, - 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 + odometry function of a train. This \<^cenelec_term>\SF\ processes data from an odometer to compute + 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 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 - the problem of numerical sampling, and the boundaries of efficient computations. The interplay + physical model of the environment, the physical and architectural model of the odometer, + but also the \<^cenelec_term>\SFRS\ 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 - with limited resources makes the odometer a fairly typical safety critical embedded system. + with limited resources makes the odometer a fairly typical \<^cenelec_term>\safety\ critical + \<^cenelec_term>\component\ of an embedded system. + + The case-study is presented in form of an \<^emph>\integrated source\ in \<^isadof> containing all four + reports from the phases: + \<^item> \<^term>\software_requirements\, \<^ie> the \<^onto_class>\SWRS\ \<^typ>\software_requirements_specification\(-report) + \<^item> \<^term>\software_architecture_and_design\, \<^ie> the \<^typ>\software_design_specification\(-report) + \<^item> \<^term>\component_implementation_and_testing\, \<^ie> the \<^typ>\software_architecture_and_design_verification\(-report) + \<^item> \<^term>\component_implementation_and_testing\, \<^ie> the \<^typ>\software_component_design_verification\(-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>\traceability\. + + \<^bold>\NOTE\ 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 document; the design and code parts will only be outlined in a final resume. The @@ -45,7 +64,7 @@ text\ development. \ -section\System Requirements as an \<^emph>\Integrated Source\\ +section\A CENELEC-conform development as an \<^emph>\Integrated Source\\ text\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 set of independent measurements based on different physical principles---as a way to enhance @@ -74,17 +93,19 @@ text\ 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 - particular, we need to make the following assumptions explicit:\vspace{-.3cm} - \<^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. + particular, we need to make the following assumptions explicit: \<^vs>\-0.3cm\ + + \<^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. These assumptions have to be traced throughout the certification process as + \<^emph>\derived requirements\ (or, in CENELEC terminology, as \<^emph>\exported constraints\), which is 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>\no slip\-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 constraints (speed and acceleration limits). Moreover, the \<^emph>\no slip\-assumption motivates @@ -112,7 +133,7 @@ subsection\Capturing ``System Interfaces.''\ text\ The requirements analysis also contains a sub-document \<^emph>\functions and interfaces\ (CENELEC notion) describing the technical format of the output of the odometry function. - This section, \eg, specifies the output \<^emph>\speed\ as given by a \<^verbatim>\int_32\ to be the + This section, \<^eg>, specifies the output \<^emph>\speed\ as given by a \<^verbatim>\int_32\ to be the ``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 sub-system configuration. \ @@ -143,7 +164,7 @@ text\ 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 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. \ @@ -316,7 +337,7 @@ text\ \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 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 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), @@ -370,7 +391,7 @@ datatype vnt_technique = 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 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. \ 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 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 -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 according to the role-set. @@ -400,17 +421,17 @@ doc_class sub_requirement = section*[claimsreqevidence::text_section]\Tracking Claims, Derived Requirements and Evidence\ text\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>\-0.15cm\ \begin{quote}\small 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 development phase fulfill the requirements and plans with respect to completeness, correctness and consistency. -\end{quote}\vspace{-1.5mm} +\end{quote} \<^vs>\-0.15cm\ The terms \<^emph>\judgment\ and \<^emph>\evidence\ 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 is fairly explicit on the \<^emph>\phase\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: \begin{isar} doc_class judgement = @@ -461,7 +482,7 @@ text*[J1::judgement, refers_to="<@>{docitem encoder_props}", \end{isar} 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 -print the formally checked content (\eg, the statement of a theorem). +print the formally checked content (\<^eg>, the statement of a theorem). \ subsection\Exporting Claims of the Requirements Specification.\ diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index 915e37a..26bad3c 100644 --- a/src/DOF/Isa_DOF.thy +++ b/src/DOF/Isa_DOF.thy @@ -2429,6 +2429,8 @@ val parse_cid = Scan.lift(Parse.position Args.name) val parse_oid' = Term_Style.parse -- parse_oid val parse_cid' = Term_Style.parse -- parse_cid + + val parse_attribute_access = (parse_oid --| (Scan.lift @{keyword "::"}) -- 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)) = 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} \ \a real hack !\ + 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 val _ = Theory.setup (ML_Antiquotation.inline \<^binding>\docitem\ @@ -2483,6 +2504,7 @@ val _ = Theory.setup (fn (ctxt,toks) => (parse_oid >> trace_attr_2_ML ctxt) (ctxt, toks)) #> basic_entity \<^binding>\trace_attribute\ parse_oid' pretty_trace_style #> basic_entity \<^binding>\doc_class\ parse_cid' pretty_cid_style #> + basic_entity \<^binding>\onto_class\ parse_cid' pretty_cid_style #> basic_entity \<^binding>\docitem_attribute\ parse_attribute_access' pretty_attr_access_style ) end diff --git a/src/ontologies/CENELEC_50128/CENELEC_50128.thy b/src/ontologies/CENELEC_50128/CENELEC_50128.thy index de97088..71fdee6 100644 --- a/src/ontologies/CENELEC_50128/CENELEC_50128.thy +++ b/src/ontologies/CENELEC_50128/CENELEC_50128.thy @@ -15,9 +15,9 @@ chapter \An Outline of a CENELEC Ontology\ text\ NOTE: An Ontology-Model of a certification standard such as CENELEC or Common Criteria identifies: -- notions (conceptual \emph{categories}) having \emph{instances} +- notions (conceptual \<^emph>\categories\) having \<^emph>\instances\ (similar to classes and objects), -- their subtype relation (eg., a "SRAC" is an "assumption"), +- their \<^emph>\subtype\ relation (eg., a "SRAC" is an "assumption"), - their syntactical structure (for the moment: defined by regular expressions describing the order of category instances in the overall document as a regular language) @@ -40,23 +40,78 @@ begin *) -text\We re-use the class @\typ math_content\, which provides also a framework for +text\We re-use the class \<^typ>\math_content\, which provides also a framework for semi-formal "math-alike" terminology, which we re-use by this definition.\ doc_class semi_formal_content = math_content + status :: status <= "semiformal" - mcc :: math_content_class <= "terminology" + mcc :: math_content_class + + 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\ in the following, all \<^theory_text>\Definition*\ statements are interpreted as + \<^doc_class>\cenelec_term\s, i.e. semi-formal teminological definitions.\ + +(* +ML\ +val typ_abbrev = Scan.lift +\ + +ML\ +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")) + + +\ +ML\ + +fun context_position_parser parse_con (ctxt, toks) = + let val pos = case toks of + a :: _ => Token.pos_of a + | _ => @{here} \ \a real hack !\ + 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>\Onto_class\ parse_cid' pretty_cid_style) + +\ + +text\ \<^Onto_class>\cenelec_term\ \ + +*) + +declare[[ Definition_default_class="cenelec_term"]] +(*>>*) text\ Excerpt of the BE EN 50128:2011, page 22. \ - section\Terms and Definitions\ 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.\ Definition*[assessor, short_name="''assessor''"] -\entity that carries out an assessment\ +\entity that carries out an assessment.\ Definition*[COTS, short_name="''commercial off-the-shelf software''"] \software defined by market-driven need, commercially available and whose fitness for purpose -has been demonstrated by a broad spectrum of commercial users\ +has been demonstrated by a broad spectrum of commercial users.\ Definition*[component] \a constituent part of software which has well-defined interfaces and behaviour with respect to the software architecture and design and fulfils the following criteria: -\<^enum> it is designed according to “Components” (see Table A.20); -\<^enum> it covers a specific subset of software requirements; -\<^enum> it is clearly identified and has an independent version inside the - configuration management system or is a part of a collection of components - (e. g. subsystems) which have an independent version + \<^enum> it is designed according to “Components” (see Table A.20); + \<^enum> it covers a specific subset of software requirements; + \<^enum> it is clearly identified and has an independent version inside the + configuration management system or is a part of a collection of components + (e. g. subsystems) which have an independent version \ typ "sfc" Definition*[CMGR, short_name="''configuration manager''"] \entity that is responsible for implementing and carrying out the processes for the configuration management of documents, software and related tools including -\<^emph>\change management\\ +\<^emph>\change management\.\ Definition*[customer] -\entity which purchases a railway control and protection system including the software\ +\entity which purchases a railway control and protection system including the software.\ Definition*[designer] \entity that analyses and transforms specified requirements into acceptable design solutions -which have the required safety integrity level\ +which have the required safety integrity level.\ Definition*[entity] -\person, group or organisation who fulfils a role as defined in this European Standard\ +\person, group or organisation who fulfils a role as defined in this European Standard.\ declare_reference*[fault] Definition*[error] \defect, mistake or inaccuracy which could result in failure or in a deviation -from the intended performance or behaviour (cf. @{semi_formal_content (unchecked) \fault\}))\ +from the intended performance or behaviour (cf. @{cenelec_term (unchecked) \fault\})).\ Definition*[fault] \defect, mistake or inaccuracy which could result in failure or in a deviation -from the intended performance or behaviour (cf @{semi_formal_content \error\})\ +from the intended performance or behaviour (cf @{cenelec_term \error\}).\ Definition*[failure] -\unacceptable difference between required and observed performance\ +\unacceptable difference between required and observed performance.\ Definition*[FT, short_name="''fault tolerance''"] \built-in capability of a system to provide continued correct provision of service as specified, -in the presence of a limited number of hardware or software faults\ +in the presence of a limited number of hardware or software faults.\ Definition*[firmware] \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\ +way that is functionally independent of applicative software.\ Definition*[GS,short_name="''generic software''"] \software which can be used for a variety of installations purely by the provision of -application-specific data and/or algorithms\ +application-specific data and/or algorithms.\ Definition*[implementer] -\entity that transforms specified designs into their physical realisation\ +\entity that transforms specified designs into their physical realisation.\ Definition*[integration] \process of assembling software and/or hardware items, according to the architectural and -design specification, and testing the integrated unit\ +design specification, and testing the integrated unit.\ Definition*[integrator] -\entity that carries out software integration\ +\entity that carries out software integration.\ -Definition*[PES :: sfc, short_name="''pre-existing software''"] +Definition*[PES, short_name="''pre-existing software''"] \software developed prior to the application currently in question, including COTS (commercial -off-the shelf) and open source software\ +off-the shelf) and open source software.\ -Definition*[OSS :: sfc, short_name="''open source software''"] -\source code available to the general public with relaxed or non-existent copyright restrictions\ +Definition*[OS, short_name="''open source software''"] +\source code available to the general public with relaxed or non-existent copyright restrictions.\ Definition*[PLC, short_name="''programmable logic controller''"] \solid-state control system which has a user programmable memory for storage of instructions to -implement specific functions\ +implement specific functions.\ Definition*[PM, short_name="''project management''"] -\administrative and/or technical conduct of a project, including safety aspects\ +\administrative and/or technical conduct of a project, including safety aspects.\ Definition*[PMGR, short_name="''project manager''"] -\entity that carries out project management\ +\entity that carries out \<^cenelec_term>\PM\.\ Definition*[reliability] \ability of an item to perform a required function under given conditions for a given period of time\ @@ -157,52 +212,52 @@ Definition*[reliability] Definition*[robustness] \ability of an item to detect and handle abnormal situations\ -Definition*[RMGR, short_name="''requirements manager''"] -\entity that carries out requirements management\ - Definition*[RM, short_name="''requirements management''"] \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 throughout a project\ +Definition*[RMGR, short_name="''requirements manager''"] +\entity that carries out \<^cenelec_term>\RM\.\ + Definition*[risk] \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\ +a hazard) and the degree of severity of that harm.\ Definition*[safety] -\freedom from unacceptable levels of risk of harm to people\ +\freedom from unacceptable levels of risk of harm to people.\ Definition*[SA, short_name="''safety authority''"] \body responsible for certifying that safety related software or services comply with relevant -statutory safety requirements\ +statutory safety requirements.\ Definition*[SF, short_name="''safety function''"] -\a function that implements a part or whole of a safety requirement\ +\a function that implements a part or whole of a safety requirement.\ Definition*[SFRS, short_name= "''safety-related software''"] -\software which performs safety functions\ +\software which performs safety functions.\ Definition*[software] \intellectual creation comprising the programs, procedures, rules, data and any associated -documentation pertaining to the operation of a system\ +documentation pertaining to the operation of a system.\ Definition*[SB, short_name="''software baseline''"] \complete and consistent set of source code, executable files, configuration files, 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 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\ +for future releases at enhancements or at upgrade in the maintenance phase.\ Definition*[SD, short_name="''software deployment''"] \transferring, installing and activating a deliverable software baseline that has already been -released and assessed\ +released and assessed.\ Definition*[SWLC, short_name="''software life-cycle''"] \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 -cycle typically includes a requirements phase, design phase,test phase, integration phase, -deployment phase and a maintenance phase\ +cycle typically includes a requirements phase, design phase, test phase, integration phase, +deployment phase and a maintenance phase.\ Definition*[SWMA, short_name="''software maintainability''"] \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''"] \ 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\ +performance or other attributes, or adapt it with the aim of enhancing or correcting its behaviour.\ Definition*[SOSIL, short_name="''software safety integrity level''"] \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 0 is the lowest and 4 the highest.\ @@ -255,16 +311,16 @@ not obvious; a compiler that incorporates an executable run-time package into th Definition*[traceability, short_name="''traceability''"] \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 -another\ +another.\ Definition*[validation, short_name="''validation''"] \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 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\ +operation in accordance to its purpose in its intended environment.\ Definition*[validator, short_name="''validator''"] -\entity that is responsible for the validation\ +\entity that is responsible for the validation.\ Definition*[verification, short_name="''verification''"] \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 \ Definition*[verifier, short_name="''verifier''"] -\entity that is responsible for one or more verification activities\ +\entity that is responsible for one or more verification activities.\ chapter\Software Management and Organisation\ text\Representing chapter 5 in @{cite "bsi:50128:2014"}.\ section\Organization, Roles and Responsabilities\ -text\See also section \<^emph>\Software management and organization\. and Annex B and C\ +text\See also section \<^emph>\Software management and organization\ and Annex B and C.\ text\REQ role in Table C.1 is assumed to be a typo and should be RQM.\ @@ -300,17 +356,17 @@ datatype role = RQM \ \Requirements Manager\ datatype phase = SYSDEV_ext \ \ System Development Phase (external)\ - | SPl \ \Software Planning\ - | SR \ \Software Requirements\ - | SADES \ \Software Architecture and Design\ - | SCDES \ \Software Component Design\ - | CInT \ \Component Implementation and Testing\ - | SI \ \Software Integration\ - | SV \ \Overall Software Testing/Final Validation\ - | SCADA \ \Systems Configured by Application Data/Algorithms\ - | SD \ \Software Deployment\ - | SM \ \Software Maintenance\ - | SA \ \Software Assessment\ + | SPl \ \Software Planning\ + | SR \ \Software Requirements\ + | SADES \ \Software Architecture and Design\ + | SCDES \ \Software Component Design\ + | CInT \ \Component Implementation and Testing\ + | SI \ \Software Integration\ + | SV \ \Overall Software Testing/Final Validation\ + | SCADA \ \Systems Configured by Application Data/Algorithms\ + | SD \ \Software Deployment\ + | SM \ \Software Maintenance\ + | SA \ \Software Assessment\ abbreviation software_planning :: "phase" where "software_planning \ SPl" abbreviation software_requirements :: "phase" where "software_requirements \ SR" @@ -340,7 +396,7 @@ text\Requirement levels specified Annex A: we use the term \<^emph>\ them from the requirements specified in the standard.\ datatype normative_level = - M \ \(Mandatory)\ + M \ \(Mandatory)\ | HR \ \Highly Recommended\ | R \ \Recommended\ | Any \ \No recommendation\ @@ -365,14 +421,15 @@ doc_class safety_requirement = requirement + formal_definition :: "thm list" -text\The category @{emph \hypothesis\} is used for assumptions from the - foundational mathematical or physical domain, so for example: - \<^item> the Mordell-Lang conjecture holds, - \<^item> euklidian geometry is assumed, or - \<^item> Newtonian (non-relativistic) physics is assumed, - Their acceptance is inherently outside the scope of the model - and can only established inside certification process by - authority argument. +text\ +The category \<^emph>\hypothesis\ is used for assumptions from the +foundational mathematical or physical domain, so for example: + \<^item> the Mordell-Lang conjecture holds, + \<^item> euklidian geometry is assumed, or + \<^item> Newtonian (non-relativistic) physics is assumed, +Their acceptance is inherently outside the scope of the model +and can only established inside certification process by +authority argument. \ datatype hyp_type = physical | mathematical | computational | other @@ -384,7 +441,7 @@ doc_class hypothesis = requirement + hyp_type :: hyp_type <= physical (* default *) text\ The following sub-class of security related hypothesis might comprise, for example: - \<^item> @{term "P \ NP"}, + \<^item> \<^term>\P \ NP\, \<^item> or the computational hardness of certain functions relevant for cryptography (like prime-factorization). (* speculation bu, not 50128 *)\ @@ -469,7 +526,7 @@ figure*[fig3::figure, relative_width="100", \Illustrative Development Lifecycle 1\ text\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.\ +to the remaining document: Software Architecture and Design phases are merged, like in 7.3.\ section\Software Assurance related Entities and Concepts\ @@ -541,8 +598,9 @@ doc_class judgement = status :: status is_concerned :: "role set" <= "{VER,ASR,VAL}" -section\ Design and Test Documents \ +section\ A Classification of CENELEC Reports and Documents \ +(* should we rename this as "report" ??? bu *) doc_class cenelec_document = text_element + phase :: "phase" sil :: "sil" @@ -680,7 +738,7 @@ doc_class SWADVR = cenelec_document + phase :: "phase" <= "SADES" nlvl :: "normative_level" <= "HR" invariant force_nlvl_swadvr :: "nlvl \ = HR" - type_synonym software_architecture_and_design_verification_report = SWADVR + type_synonym software_architecture_and_design_verification = SWADVR doc_class SWCDS = cenelec_document + phase :: "phase" <= "SCDES" @@ -695,7 +753,7 @@ doc_class SWCTS = cenelec_document + doc_class SWCDVR = cenelec_document + phase :: "phase" <= "SCDES" invariant force_nlvl_swcdvr :: "if sil \ = SIL0 then nlvl \ = R else nlvl \ = HR" - type_synonym software_component_design_verification_report = SWCDVR + type_synonym software_component_design_verification = SWCDVR doc_class SWSCD = cenelec_document + phase :: "phase" <= "CInT" From 8a9684590ae2a3f7ff99d55cd943891ce484dba5 Mon Sep 17 00:00:00 2001 From: Burkhart Wolff Date: Mon, 1 Aug 2022 21:42:32 +0200 Subject: [PATCH 2/3] =?UTF-8?q?pass=20through=20mini=C3=B4do:=20deeper=20o?= =?UTF-8?q?ntological=20reasoning,=20less=20LaTeX.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- examples/CENELEC_50128/mini_odo/mini_odo.thy | 614 ++++++++++-------- src/DOF/Isa_DOF.thy | 2 +- .../technical_report/technical_report.thy | 15 +- 3 files changed, 340 insertions(+), 291 deletions(-) diff --git a/examples/CENELEC_50128/mini_odo/mini_odo.thy b/examples/CENELEC_50128/mini_odo/mini_odo.thy index 3bd7021..a06f001 100644 --- a/examples/CENELEC_50128/mini_odo/mini_odo.thy +++ b/examples/CENELEC_50128/mini_odo/mini_odo.thy @@ -34,18 +34,21 @@ text\ 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 physical model of the environment, the physical and architectural model of the odometer, - but also the \<^cenelec_term>\SFRS\ 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 - with limited resources makes the odometer a fairly typical \<^cenelec_term>\safety\ critical - \<^cenelec_term>\component\ of an embedded system. + but also the \<^cenelec_term>\SFRS\ 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 with limited resources makes the odometer a + fairly typical \<^cenelec_term>\safety\ critical \<^cenelec_term>\component\ of an embedded system. The case-study is presented in form of an \<^emph>\integrated source\ in \<^isadof> containing all four reports from the phases: - \<^item> \<^term>\software_requirements\, \<^ie> the \<^onto_class>\SWRS\ \<^typ>\software_requirements_specification\(-report) - \<^item> \<^term>\software_architecture_and_design\, \<^ie> the \<^typ>\software_design_specification\(-report) - \<^item> \<^term>\component_implementation_and_testing\, \<^ie> the \<^typ>\software_architecture_and_design_verification\(-report) - \<^item> \<^term>\component_implementation_and_testing\, \<^ie> the \<^typ>\software_component_design_verification\(-report) + \<^item> \<^term>\software_requirements\, \<^ie> the \<^onto_class>\SWRS\ + (or long:\<^typ>\software_requirements_specification\(-report)) + \<^item> \<^term>\software_architecture_and_design\, \<^ie> the \<^onto_class>\SWDS\ + (or long: \<^typ>\software_design_specification\(-report)) + \<^item> \<^term>\component_implementation_and_testing\, \<^ie> the \<^onto_class>\SWADVR\ + (or long: \<^typ>\software_architecture_and_design_verification\(-report)) + \<^item> \<^term>\component_implementation_and_testing\, \<^ie> the \<^onto_class>\SWADVR\ + (or long: \<^typ>\software_component_design_verification\(-report).) The objective of this case study is to demonstrate deep-semantical ontologoies in software developments targeting certifications, and in particular, how \<^isadof>'s @@ -65,6 +68,7 @@ text\ \ section\A CENELEC-conform development as an \<^emph>\Integrated Source\\ + text\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 set of independent measurements based on different physical principles---as a way to enhance @@ -93,14 +97,18 @@ text\ 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 - particular, we need to make the following assumptions explicit: \<^vs>\-0.3cm\ - - \<^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. + particular, we need to make the following assumptions explicit: \<^vs>\-0.3cm\\ +text*["perfect-wheel"::assumption] +\\<^item> the wheel is perfectly circular with a given, constant radius. \<^vs>\-0.3cm\\ +text*["no-slip"::assumption] +\\<^item> the slip between the trains wheel and the track negligible. \<^vs>\-0.3cm\\ +text*["constant-teeth-dist"::assumption] +\\<^item> the distance between all teeth of a wheel is the same and constant, and \<^vs>\-0.3cm\\ +text*["constant-sampling-rate"::assumption] +\\<^item> the sampling rate of positions is a given constant.\ +text\ These assumptions have to be traced throughout the certification process as \<^emph>\derived requirements\ (or, in CENELEC terminology, as \<^emph>\exported constraints\), which is @@ -114,53 +122,49 @@ text\ \ subsection\Capturing ``System Architecture.''\ + +figure*["three-phase"::figure,relative_width="70",src="''figures/three-phase-odo''"] +\An odometer with three sensors \C1\, \C2\, and \C3\.\ + text\ - \begin{figure} - \centering - \includegraphics[width=.70\textwidth]{figures/three-phase-odo} - \begin{picture}(0,0) - \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>\system architecture description\ - (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.$ + The requirements analysis also contains a document \<^doc_class>\SYSAD\ + (\<^typ>\system_architecture_description\) that contains technical drawing of the odometer, + a timing diagram (see \<^figure>\three-phase\), and tables describing the encoding of the position + for the possible signal transitions of the sensors \C1\, \C2\, and \C3\. \ subsection\Capturing ``System Interfaces.''\ text\ - The requirements analysis also contains a sub-document \<^emph>\functions and interfaces\ - (CENELEC notion) describing the technical format of the output of the odometry function. + The requirements analysis also contains a sub-document \<^doc_class>\FnI\ (\<^typ>\functions_and_interfaces\) + describing the technical format of the output of the odometry function. This section, \<^eg>, specifies the output \<^emph>\speed\ as given by a \<^verbatim>\int_32\ to be the - ``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 + ``Estimation of the speed (in mm/sec) evaluated over the latest \N\<^sub>a\<^sub>v\<^sub>g\ samples'' + where the speed refers to the physical speed of the train and \N\<^sub>a\<^sub>v\<^sub>g\ a parameter of the sub-system configuration. \ (*<*) -declare_reference*["df-numerics-encshaft"::figure] +declare_reference*["df-numerics-encshaft"::figure] (*>*) subsection\Capturing ``Required Performances.''\ text\ The given analysis document is relatively implicit on the expected precision of the measurements; - however, certain interface parameters like \inlineisar*Odometric_Position_TimeStamp* - (a counter on the number of samplings) and \inlineisar*Relative_Position* are defined by as + however, certain interface parameters like \Odometric_Position_TimeStamp\ + (a counter on the number of samplings) and \Relative_Position\ are defined by as 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. - 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 \Relative_Position\ to the theoretical distance. 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 function as represented (see @{figure (unchecked) "df-numerics-encshaft"}).\ + figure*["df-numerics-encshaft"::figure,relative_width="76",src="''figures/df-numerics-encshaft''"] \Real distance vs. discrete distance vs. shaft-encoder sequence\ subsection\Capturing the ``Software Design Spec'' (Resume).\ text\ -\enlargethispage{\baselineskip} 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 new incoming shaft encodings, checking them and propagating two kinds of error-states (one allowing @@ -186,85 +190,94 @@ section\Formal Enrichment of the Software Requirements Specification\ After the \<^emph>\capture\-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 - \formal enrichment\. For example, from the assumptions in the architecture follow - the definitions: -\begin{isar} -definition teeth_per_wheelturn::nat ("tpw") where "tpw \ SOME x. x > 0" -definition wheel_diameter::real ("w$_d$") where "w$_d$ \ SOME x. x > 0" -definition wheel_circumference::real ("w$_{\text{circ}}$") where "w$_{\text{circ}}$ \ pi * w$_d$" -definition \s$_{\text{res}}$::real where "\s$_{\text{res}}$ \ w$_{\text{circ}}$ / (2 * 3 * tpw)" -\end{isar} - Here, \inlineisar{real} refers to the real numbers as defined in the HOL-Analysis - library, which provides concepts such as Cauchy Sequences, limits, - differentiability, and a very substantial part of classical Calculus. \inlineisar{SOME} is the - Hilbert choice operator from HOL; the definitions of the model parameters admit all possible positive values as uninterpreted - constants. Our perfect-wheel assumption is translated into a calculation of the circumference of the - wheel, while \inlineisar{\sres}, the resolution of the odometer, can be calculated + \formal enrichment\. For example, from the assumptions in the architecture follow + the definitions: + + @{theory_text [display]\ + definition teeth_per_wheelturn::nat ("tpw") where "tpw \ SOME x. x > 0" + definition wheel_diameter::real ("w\<^sub>d") where "w\<^sub>d \ SOME x. x > 0" + definition wheel_circumference::real ("w\<^sub>0") where "w\<^sub>0 \ pi * w\<^sub>d" + definition \s\<^sub>r\<^sub>e\<^sub>s::real where "\s\<^sub>r\<^sub>e\<^sub>s \ w\<^sub>0 / (2 * 3 * tpw)" + \} + + Here, \real\ refers to the real numbers as defined in the HOL-Analysis library, which provides + concepts such as Cauchy Sequences, limits, differentiability, and a very substantial part of + classical Calculus. \SOME\ is the Hilbert choice operator from HOL; the definitions of the + model parameters admit all possible positive values as uninterpreted constants. Our + \<^assumption>\perfect-wheel\ is translated into a calculation of the circumference of the + wheel, while \\s\<^sub>r\<^sub>e\<^sub>s\, the resolution of the odometer, can be calculated from the these parameters. HOL-Analysis permits to formalize the fundamental physical observables: -\begin{isar} -type_synonym distance_function = "real\real" -definition Speed::"distance_function\real\real" where "Speed f \ deriv f" -definition Accel::"distance_function\real\real" - where "Accel f \ deriv (deriv f)" -\end{isar} -which permits to constrain the central observable \inlineisar|distance_function| in a + + @{theory_text [display]\ + type_synonym distance_function = "real\real" + definition Speed::"distance_function\real\real" where "Speed f \ deriv f" + definition Accel::"distance_function\real\real" where "Accel f \ deriv (deriv f)" + \} + +which permits to constrain the central observable \distance_function\ in a 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 \distance_function df\ . The essence of the physics of the train is covered by the following definition: -\begin{isar} -definition normally_behaved_distance_function :: "(real \ real) \ bool" - where normally_behaved_distance_function df = - ( \ t. df(t) \ \$_{\ge 0}$ \ (\ t \ \$_{\le 0}$. df(t) = 0) - \ df differentiable on$_{\text{R}}$ \ (Speed df)differentiable on$_{\text{R}}$ - \ (Accel df)differentiable on$_{\ensuremath{R}}$ - \ (\ t. (Speed df) t \ {-Speed$_{\text{Max}}$ .. Speed$_{\text{Max}}$}) - \ (\ t. (Accel df) t \ {-\Accel$_{\text{Max}}$\ .. \Accel$_{\text{Max}}$\})) -\end{isar} + + @{theory_text [display]\ + definition normally_behaved_distance_function :: "(real \ real) \ bool" + where normally_behaved_distance_function df = + ( \ t. df(t) \ \\<^sub>\\<^sub>0 \ (\ t \ \\\<^sub>\\<^sub>0. df(t) = 0) + \ df differentiable on \\<^sub>\\<^sub>0 \ (Speed df)differentiable on \\<^sub>\\<^sub>0$ + \ (Accel df)differentiable on \\<^sub>\\<^sub>0 + \ (\ t. (Speed df) t \ {Speed\<^sub>M\<^sub>i\<^sub>n .. Speed\<^sub>M\<^sub>a\<^sub>x}) + \ (\ t. (Accel df) t \ {Accel\<^sub>M\<^sub>i\<^sub>n .. Accel\<^sub>M\<^sub>a\<^sub>x})) + \} + 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. -Note that violations, in particular of the constraints on speed and acceleration, \<^emph>\do\ occur in practice. -In such cases, the global system adapts recovery strategies that are out of the scope of our model. -Concepts like \inlineisar+shaft_encoder_state+ (a triple with the sensor values -\inlineisar{C1}, \inlineisar{C2}, \inlineisar{C3}) were formalized as types, while tables were +states them as three-fold differentiable function in certain bounds concerning speed and +acceleration. Note that violations, in particular of the constraints on speed and acceleration, +\<^emph>\do\ occur in practice. In such cases, the global system adapts recovery strategies that are out +of the scope of our model. Concepts like \shaft_encoder_state\ (a triple with the sensor values +\C1\, \C2\, \C3\) were formalized as types, while tables were defined as recursive functions: -\enlargethispage{2\baselineskip}\begin{isar} -fun phase$_0$ :: "nat \ shaft_encoder_state" where - "phase$_0$ (0) = \ C1 = False, C2 = False, C3 = True \" - |"phase$_0$ (1) = \ C1 = True, C2 = False, C3 = True \" - |"phase$_0$ (2) = \ C1 = True, C2 = False, C3 = False\" - |"phase$_0$ (3) = \ C1 = True, C2 = True, C3 = False\" - |"phase$_0$ (4) = \ C1 = False, C2 = True, C3 = False\" - |"phase$_0$ (5) = \ C1 = False, C2 = True, C3 = True \" - |"phase$_0$ x = phase$_0$(x - 6)" -definition Phase ::"nat\shaft_encoder_state" where Phase(x) = phase$_0$(x-1) -\end{isar} -We now define shaft encoder sequences as -translations of distance functions: -\begin{isar} -definition encoding::"distance_function\nat\real\shaft_encoder_state" - where "encoding df init$_{\text{pos}}$ \ \x. Phase(nat\df(x) / \s$_{\text{res}}$\ + init$_{\text{pos}}$)" -\end{isar} -where \inlineisar+init$_{\text{pos}}$+ is the initial position of the wheel. -\inlineisar+sampling+'s were constructed from encoding sequences over discretized time points: -\begin{isar} -definition $\!\!$sampling::"distance$\!$_function\nat\real\nat\shaft$\!$_encoder$\!$_state" - where "sampling df init$_{\text{pos}}$ \t \ \n::nat. encoding df init$_{\text{pos}}$ (n * \t)" -\end{isar} -The sampling interval \inlineisar+\t+ (the inverse of the sampling frequency) is a critical + + @{theory_text [display]\ + fun phase\<^sub>0 :: "nat \ shaft_encoder_state" where + "phase\<^sub>0 (0) = \ C1 = False, C2 = False, C3 = True \" + |"phase\<^sub>0 (1) = \ C1 = True, C2 = False, C3 = True \" + |"phase\<^sub>0 (2) = \ C1 = True, C2 = False, C3 = False\" + |"phase\<^sub>0 (3) = \ C1 = True, C2 = True, C3 = False\" + |"phase\<^sub>0 (4) = \ C1 = False, C2 = True, C3 = False\" + |"phase\<^sub>0 (5) = \ C1 = False, C2 = True, C3 = True \" + |"phase\<^sub>0 x = phase\<^sub>0(x - 6)" + definition Phase ::"nat\shaft_encoder_state" where Phase(x) = phase\<^sub>0(x-1) + \} + +We now define shaft encoder sequences as translations of distance functions: + + @{theory_text [display]\ + definition encoding::"distance_function\nat\real\shaft_encoder_state" + where "encoding df init\<^sub>p\<^sub>o\<^sub>s \ \x. Phase(nat\df(x) / \s\<^sub>r\<^sub>e\<^sub>s\ + init\<^sub>p\<^sub>o\<^sub>s)" + \} + +where \init\<^sub>p\<^sub>o\<^sub>s\ is the initial position of the wheel. +\sampling\'s were constructed from encoding sequences over discretized time points: + + @{theory_text [display]\ + definition sampling::"distance_function\nat\real\nat\shaft_encoder_state" + where "sampling df init\<^sub>p\<^sub>o\<^sub>s \t \ \n::nat. encoding df initinit\<^sub>p\<^sub>o\<^sub>s (n * \t)" + \} + 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 frequency etc., we can infer the maximal time of service as well the maximum distance the device can measure. As an example configuration, choosing 1m for -\inlineisar+w$_d$+, 100 for \inlineisar+tpw+, 80km/h \inlineisar+Speed$_{\text{Max}}$+, +\w\<^sub>d\, 100 for \tpw\, 80km/h \Speed\<^sub>M\<^sub>a\<^sub>x\, 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. The required precision of an odometer can be defined by a constant describing -the maximally allowed difference between \inlineisar+df(n*\t)+ and -\inlineisar+sampling df init$_{\text{pos}}$ \t n+ for all \inlineisar+init$_{\text{pos}}$ \{0..5}+. +the maximally allowed difference between \df(n*\t)\ and +\sampling df init\<^sub>p\<^sub>o\<^sub>s \t n\ for all \init\<^sub>p\<^sub>o\<^sub>s \{0..5}\. \ (*<*) ML\val two_thirty2 = 1024 * 1024 * 1024 * 4; @@ -274,41 +287,50 @@ ML\val two_thirty2 = 1024 * 1024 * 1024 * 4; section*[verific::technical]\Verification of the Software Requirements Specification\ text\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 -all sensors \inlineisar{C1}, \inlineisar{C2}, and \inlineisar{C3} are all ``off'' or situations in +properties of the device. For example, the \Phase\-table excludes situations in which +all sensors \C1\, \C2\, and \C3\ are all ``off'' or situations in 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 -above definitions: -\begin{isar} -lemma Encoder_Property_1:(C1(Phase x) \ C2(Phase x) \ 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+\x<6. \y<6. phase$_0$ x = phase$_0$ y \ 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 ** : \t * Speed$_{\text{Max}}$ < \s$_{\text{res}}$ - shows \ \X\\t. 0<\X \ - \f. retracting (f::nat\nat) \ - sampling df init$_{\text{pos}}$ \X = (sampling df init$_{\text{pos}}$ \t) o f +shown by a very small Isabelle case-distinction proof that this safety requirement follows indeed +from the above definitions: -\end{isar} -This theorem states for \inlineisar+normally_behaved_distance_function+s that there is + @{theory_text [display]\ + lemma Encoder_Property_1:(C1(Phase x) \ C2(Phase x) \ 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 + \} + +for all positions \x\. Similarly, it is proved that the table is indeed cyclic: + + \phase\<^sub>0 x = phase\<^sub>0(x mod 6)\ + +and locally injective: + + \\x<6. \y<6. phase\<^sub>0 x = phase\<^sub>0 y \ x = y\ + +These lemmas, building the ``theory of an odometer,'' culminate in a theorem +that we would like to present in more detail. + + @{theory_text [display]\ + theorem minimal_sampling : + assumes * : normally_behaved_distance_function df + and ** : \t * Speed\<^sub>M\<^sub>a\<^sub>x < \s\<^sub>r\<^sub>e\<^sub>s + shows \ \X\\t. 0<\X \ + \f. retracting (f::nat\nat) \ + sampling df init\<^sub>p\<^sub>o\<^sub>s \X = (sampling df init\<^sub>p\<^sub>o\<^sub>s \t) o f + + \} + +This theorem states for \normally_behaved_distance_function\s that there is 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 \df\ gained from this minimal sampling frequency can be ``pumped up'' to samplings of these higher sampling frequencies; they do not contain more information. -Of particular interest is the second assumption, labelled ``\inlineisar|**|,'' which -establishes a lower bound from \inlineisar+w$_{\text{circ}}$+, \inlineisar+tpw+, -\inlineisar+Speed$_{\text{Max}}$+ for the sampling frequency. Methodologically, this represents +Of particular interest is the second assumption, labelled ``\**\'' which +establishes a lower bound from \w\<^sub>0\, \tpw\, +\Speed\<^sub>M\<^sub>a\<^sub>x\ for the sampling frequency. Methodologically, this represents an exported constraint that can not be represented \<^emph>\inside\ the design model: it means 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 @@ -322,6 +344,7 @@ standard~@{cite "bsi:50128:2014"}, 7.2.4.22 and are usually addressed in an own \ chapter*[ontomodeling::text_section]\The CENELEC 50128 Ontology\ + text\ 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 @@ -333,125 +356,144 @@ text\ section*[lhf::text_section] \Tracking Concepts and Definitions\ + text\ - \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 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 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 - of the concept ``traceability'' in paragraphs 3.1.46 (a notion referenced 31 times in the standard), - which we translated directly into: -\begin{isar} -Definition*[traceability::concept] 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 another. -\end{isar} - In the integrated source of the odometry study, we can reference in a text element to this + of the concept \<^cenelec_term>\traceability\ in paragraphs 3.1.46 (a notion referenced 31 times in + the standard), which we translated directly into: + + @{theory_text [display]\ + Definition*[traceability, short_name="''traceability''"] + \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 another.\ + \} + + In the integrated source of the odometry study, we can reference in a text element to this concept as follows: -\begin{isar} -text*[...] ... to assure <@>{concept traceability} for - <@>{requirement bitwiseAND}, we prove ... -\end{isar} - The presentation of this document element inside \isadof is immediately hyperlinked against the - \inlineisar+Definition*+ element shown above; this serves as documentation of + + @{theory_text [display]\ + text*[...]\ ... to assure <@>{cenelec_term traceability} for + <@>{requirement bitwiseAND}, we prove ... \ + \} + + + \<^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 \ Definition* \}-element shown above; this serves as documentation of 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 this later. 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. -\begin{isar} -datatype role = - PM (* Program Manager *) | RQM (* Requirements Manager *) - | DES (* Designer *) | IMP (* Implementer *) | - | VER (* Verifier *) | VAL (* Validator *) | ... -datatype phase = - SYSDEV_ext (* System Development *) | SPl (* Software Planning *) - | SR (* Software Requirement *) | SA (* Software Architecture *) - | SDES (* Software Design *) | ... -\end{isar} -Similarly, we can formalize the Table A.5: Verification and Testing of @{cite "bsi:50128:2014"}: -a classification of \<^emph>\verification and testing techniques\: -\begin{isar} -datatype vnt_technique = + + @{theory_text [display]\ + datatype role = + PM (* Program Manager *) | RQM (* Requirements Manager *) + | DES (* Designer *) | IMP (* Implementer *) | + | VER (* Verifier *) | VAL (* Validator *) | ... + datatype phase = + SYSDEV_ext (* System Development *) | SPl (* Software Planning *) + | SR (* Software Requirement *) | SA (* Software Architecture *) + | SDES (* Software Design *) | ... + \} + + Similarly, we can formalize the Table A.5: Verification and Testing of @{cite "bsi:50128:2014"}: + a classification of \<^emph>\verification and testing techniques\: + + @{theory_text [display]\ + datatype vnt_technique = formal_proof "thm list" | stat_analysis | dyn_analysis dyn_ana_kind | ... -\end{isar} - 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 \formal_proof\ 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 environment. Additional checks could be added to make sure that these theorems have a particular form. 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 - definitively not sufficient to satisfy the claimed requirement. Human evaluators will always have - to check that the provided theorem \adequately\ represents the claim; we do not in the slightest - 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 - 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. + world of systems attempting to assure \<^cenelec_term>\traceability\, referencing a particular + (proven) theorem is definitively not sufficient to satisfy the claimed requirement. Human + evaluators will always have to check that the provided theorem \adequately\ represents the claim; + we do not in the slightest 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 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. \ section*[moe::text_section] \Major Ontological Entities: Requirements and Evidence\ text\ - We introduce central concept of a \<^emph>\requirement\ as an ODL \inlineisar*doc_class* - based on some generic basic library \inlineisar*text_element* providing basic layout attributes. -\begin{isar} -doc_class requirement = text_element + - long_name :: "string option" - is_concerned :: "role set" -\end{isar} -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 -allows expressing who ``owns'' this text-element. \isadof supports a role-based -presentation, \<^eg>, different presentation styles of the -integrated source may decide to highlight, to omit, to defer into an annex, text entities -according to the role-set. + We introduce central concept of a \<^emph>\requirement\ as an ODL \<^theory_text>\doc_class\ + based on the generic basic library \<^doc_class>\text_element\ providing basic layout attributes. + + @{theory_text [display]\ + doc_class requirement = text_element + + long_name :: "string option" + is_concerned :: "role set" + \} + +the groups of stakeholders in the CENELEC process. Therefore, the \is_concerned\-attribute +allows expressing who ``owns'' this text-element. \<^isadof> supports a role-based +presentation, \<^eg>, different presentation styles of the integrated source may decide to highlight, +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 of requirement decomposition as advocated in GSN~@{cite "kelly.ea:goal:2004"}: -\begin{isar} -doc_class sub_requirement = - decomposes :: "requirement" - relates_to :: "requirement set" -\end{isar}\ + + @{theory_text [display]\ + doc_class sub_requirement = + decomposes :: "requirement" + relates_to :: "requirement set" + \} +\ section*[claimsreqevidence::text_section]\Tracking Claims, Derived Requirements and Evidence\ text\An example for making explicit implicit principles, consider the following statement @{cite "bsi:50128:2014"}, pp. 25.: \<^vs>\-0.15cm\ + \begin{quote}\small 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 development phase fulfill the requirements and plans with respect to completeness, correctness and consistency. \end{quote} \<^vs>\-0.15cm\ -The terms \<^emph>\judgment\ and \<^emph>\evidence\ 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 is fairly explicit on the \<^emph>\phase\s and the organizational roles that different stakeholders -should have in the process. Our version to express this key concept of judgment, \<^eg>, by -the following concept: -\begin{isar} -doc_class judgement = - refers_to :: requirement - evidence :: "vnt_technique list" - status :: status - is_concerned :: "role set" <= "{VER,ASR,VAL}" -\end{isar} + +The terms \<^onto_class>\judgement\ based on \<^term>\evidence\ 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 is fairly explicit on the \<^emph>\phase\s and the organizational roles that +different stakeholders should have in the process. Our version to express this key concept of +\<^onto_class>\judgement\ , \<^eg>, by the following concept: + + @{theory_text [display]\ + doc_class judgement = + refers_to :: requirement + evidence :: "vnt_technique list" + status :: status + is_concerned :: "role set" <= "{VER,ASR,VAL}" + \} + As one can see, the role set is per default set to the verification team, the assessors and the validation team. -There are different views possible here: an alternative would be to define \inlineisar+evidence+ -as ontological concept with \inlineisar+vnt_technique+'s (rather than an attribute of judgement) -and consider the basis of judgments as a relation between requirements and relation: -\begin{isar} -doc_class judgement = - based_on :: "(requirement \ evidence) set" - status :: status - is_concerned :: "role set" <= "{VER,ASR,VAL}" -\end{isar} +There are different views possible here: an alternative would be to define \<^term>\evidence\ +as ontological concept with \<^typ>\vnt_technique\'s (rather than an attribute of judgement) +and consider the basis of a summary containing the relation between requirements and relation: + + @{theory_text [display]\ + doc_class summary = + based_on :: "(requirement \ evidence) set" + status :: status + is_concerned :: "role set" <= "{VER,ASR,VAL}" + \} More experimentation will be needed to find out what kind of ontological modeling is most adequate for developers in the context of \isadof. @@ -463,60 +505,66 @@ text\From the variety of different possibilities for adding CENELEC annota integrated source, we will, in the following, point out three scenarios.\ subsection\Internal Verification of Claims in the Requirements Specification.\ -text\In our case, the SR-team early on detected a property necessary +text\In our case, the \<^term>\SR\-team early on detected a property necessary for error-detection of the device (c.f. @{technical verific}): -\enlargethispage{2\baselineskip}\begin{isar} -text*[encoder_props::requirement] The requirement specification team ... - C1 & C2 & C3 = 0 (bitwise logical AND operation) - C1 | C2 | C3 = 1 (bitwise logical OR operation) -\end{isar} + + @{theory_text [display]\ + text*[encoder_props::requirement]\ The requirement specification team identifies the property: + C1 & C2 & C3 = 0 (bitwise logical AND operation) + C1 | C2 | C3 = 1 (bitwise logical OR operation) \ + \} + After the Isabelle proofs shown in @{technical verific}, we can either register the theorems directly in an evidence statement: -\begin{isar} -text*[J1::judgement, refers_to="<@>{docitem encoder_props}", - evidence="[formal_proof[<@>{thm Encoder_Property_1}, - <@>{thm Encoder_Property_2}]]"] - The required encoder properties are in fact verified to be consistent - with the formalization of <@>{term "phase$_0$"}. -\end{isar} -The references \inlineisar|<@>{...}|, called antiquotation, allow us not only to reference to + @{theory_text [display]\ + text*[J1::judgement, refers_to="@{docitem encoder_props}", + evidence="[formal_proof[@{thm Encoder_Property_1}, + @{thm Encoder_Property_2}]]"] + \The required encoder properties are in fact verified to be consistent + with the formalization of @{term "phase\<^sub>0"}.\ + \} + +The references \@{...}\, called antiquotation, allow us not only to reference to formal concepts, they are checked for consistency and there are also antiquotations that print the formally checked content (\<^eg>, the statement of a theorem). \ subsection\Exporting Claims of the Requirements Specification.\ -text\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]We can now state ... -definition -Odometric_Position_Count_precise::(shaft_encoder_state list\output)\bool -where Odometric_Position_Count_precise odofunction \ - (\ df. \S. normally_behaved_distance_function df - \ representable S - \ valid_sampling S df - \ (let pos = uint(Odometric_Position_Count(odofunction S)) - in \df((length S - 1)*\t$_{\text{odo}}$) - (\s$_{\text{res}}$ * pos)\ \ \s$_{\text{res}}$)) -update_instance*[R5::safety_requirement, - formal_definition:="[<@>{thm Odometric_Position_Count_precise_def}]"] -\end{isar} -By \inlineisar+update_instance*+, we book the property \inlineisar+Position_Count_precise_def+ as -\inlineisar+safety_requirement+, a specific sub-class of \inlineisar+requirement+s +text\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 \df\, and any representable and valid +sampling sequence that can be constructed for \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. + + @{theory_text [display]\ + text*[R5::safety_requirement]\We can now state ... \ + definition Odometric_Position_Count_precise :: "(shaft_encoder_state list\output)\bool" + where "Odometric_Position_Count_precise odofunction \ + (\ df. \S. normally_behaved_distance_function df + \ representable S + \ valid_sampling S df + \ (let pos = uint(Odometric_Position_Count(odofunction S)) + in \df((length S - 1)*\t\<^sub>o\<^sub>d\<^sub>o) - (\s\<^sub>r\<^sub>e\<^sub>s * pos)\ \ \s\<^sub>r\<^sub>e\<^sub>s))" + + update_instance*[R5::safety_requirement, + formal_definition:="[@{thm \Odometric_Position_Count_precise_def\}]"] + \} + +By \<^theory_text>\update_instance*\, we book the property \Position_Count_precise_def\ as +\<^onto_class>\safety_requirement\, a specific sub-class of \<^onto_class>\requirement\s requesting a formal definition in Isabelle.\ subsection\Exporting Derived Requirements.\ + text\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 -the condition labelled ``\inlineisar|**|'' in @{docitem verific}. The current CENELEC standard clearly separates +the condition labelled ``\**\'' in @{docitem verific}. The current CENELEC standard clearly separates ``requirement specifications'' from ``verification reports,'' which is probably motivated 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 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, @@ -531,58 +579,58 @@ different PDF versions and for each version, document specific consistency guara automatically enforced. 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 -derived class from \inlineisar+requirement+.) and add the definition of the predicate into the +\<^onto_class>\SRAC\ (CENELEC for: safety-related application condition; ontologically, this is a +derived class from \<^onto_class>\requirement\.) and add the definition of the predicate into the document instance as described in the previous section.\ - -text\\appendix\ chapter\Appendix\ text\ -\<^item> \inlineisar|<@>{thm refl}|: @{thm refl} -\<^item> \inlineisar|<@>{thm [source] refl}|: @{thm [source] refl} -\<^item> \inlineisar|<@>{thm[mode=Rule] conjI}|: @{thm[mode=Rule] conjI} -\<^item> \inlineisar|<@>{file "mini_odo.thy"}|: @{file "mini_odo.thy"} -\<^item> \inlineisar|<@>{value "3+4::int"}|: @{value "3+4::int"} -\<^item> \inlineisar|<@>{const hd}|: @{const hd} -\<^item> \inlineisar|<@>{theory HOL.List}|: @{theory HOL.List} -\<^item> \inlineisar|<@>{term "3"}|: @{term "3"} -\<^item> \inlineisar|<@>{type bool}|: @{type bool} -\<^item> \inlineisar|<@>{term [show_types] "f x = a + x"}|: @{term [show_types] "f x = a + x"} +\<^item> \@{thm refl}\ : @{thm refl} +\<^item> \@{thm [source] refl}\ : @{thm [source] refl} +\<^item> \@{thm[mode=Rule] conjI}\ : @{thm[mode=Rule] conjI} +\<^item> \@{file "mini_odo.thy"}\ : @{file "mini_odo.thy"} +\<^item> \@{value "3+4::int"}}\ : @{value "3+4::int"} +\<^item> \@{const hd}\ : @{const hd} +\<^item> \@{theory HOL.List}\ : @{theory HOL.List} +\<^item> \@{term "3"}\ : @{term "3"} +\<^item> \@{type bool}\ : @{type bool} +\<^item> \@{thm term [show_types] "f x = a + x"}\ : @{term [show_types] "f x = a + x"} \ -text\Examples for declaration of typed doc-items "assumption" and "hypothesis", +text\Examples for declaration of typed doc-classes "assumption" (sic!) and "hypothesis" (sic!!), concepts defined in the underlying ontology @{theory "Isabelle_DOF.CENELEC_50128"}. \ text*[ass2::assumption, long_name="Some ''assumption one''"] \ The subsystem Y is safe. \ text*[hyp1::hypothesis] \ P not equal NP \ -text\A real example fragment from a larger project, declaring a text-element as a - "safety-related application condition", a concept defined in the - @{theory "Isabelle_DOF.CENELEC_50128"} ontology:\ +text\ + A real example fragment from a larger project, declaring a text-element as a + "safety-related application condition", a concept defined in the + @{theory "Isabelle_DOF.CENELEC_50128"} ontology:\ text*[hyp2::hypothesis]\Under the assumption @{assumption \ass2\} we establish the following: ... \ -text*[ass122::SRAC, long_name="Some ''ass122''"] \ The overall sampling frequence of the odometer -subsystem is therefore 14 khz, which includes sampling, computing and -result communication times... \ +text*[ass122::SRAC, long_name="Some ''ass122''"] +\ The overall sampling frequence of the odometer subsystem is therefore 14 khz, + which includes sampling, computing and result communication times... \ -text*[ass123::SRAC] \ The overall sampling frequence of the odometer -subsystem is therefore 14 khz, which includes sampling, computing and -result communication times... \ +text*[ass123::SRAC] +\ The overall sampling frequence of the odometer subsystem is therefore 14 khz, + which includes sampling, computing and result communication times... \ -text*[ass124::EC, long_name="Some ''ass124''"] \ The overall sampling frequence of the odometer -subsystem is therefore 14 khz, which includes sampling, computing and -result communication times... \ +text*[ass124::EC, long_name="Some ''ass124''"] +\ The overall sampling frequence of the odometer subsystem is therefore 14 khz, + which includes sampling, computing and result communication times... \ -text*[t10::test_result] \ This is a meta-test. This could be an ML-command -that governs the external test-execution via, eg., a makefile or specific calls -to a test-environment or test-engine. \ +text*[t10::test_result] +\ This is a meta-test. This could be an ML-command that governs the external + test-execution via, \<^eg>, a makefile or specific calls to a test-environment or test-engine. \ -text\Finally some examples of references to doc-items, i.e. text-elements with declared - meta-information and status. \ +text +\ Finally some examples of references to doc-items, i.e. text-elements + with declared meta-information and status. \ text \ As established by @{test_result (unchecked) \t10\}, @{test_result (define) \t10\} \ text \ the @{test_result \t10\} @@ -590,10 +638,10 @@ text \ the @{test_result \t10\} text \ represent a justification of the safety related applicability condition @{SRAC \ass122\} aka exported constraint @{EC \ass122\}.\ -(* due to notational conventions for antiquotations, one may even write: *) -(* CRASHES WITH LaTeX backend error. *) -text \ represent a justification of the safety related applicability - condition \<^SRAC>\ass122\ aka exported constraint \<^EC>\ass122\.\ +text \ due to notational conventions for antiquotations, one may even write: + + "represent a justification of the safety related applicability + condition \<^SRAC>\ass122\ aka exported constraint \<^EC>\ass122\."\ (*<*) diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index 26bad3c..0e58a91 100644 --- a/src/DOF/Isa_DOF.thy +++ b/src/DOF/Isa_DOF.thy @@ -2462,7 +2462,7 @@ fun trace_attr_2_ML ctxt (oid:string,pos) = fun compute_cid_repr ctxt cid pos = 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 diff --git a/src/ontologies/technical_report/technical_report.thy b/src/ontologies/technical_report/technical_report.thy index e52a3b2..48d9c33 100644 --- a/src/ontologies/technical_report/technical_report.thy +++ b/src/ontologies/technical_report/technical_report.thy @@ -38,15 +38,16 @@ doc_class "code" = technical + checked :: bool <= "False" caption :: "string" <= "''''" +typ code -text\The @{doc_class "code"} is a general stub for free-form and type-checked code-fragments -such as: -\<^enum> SML code -\<^enum> bash code -\<^enum> isar code (although this might be an unwanted concurrence to the Isabelle standard cartouche) -\<^enum> C code. +text\The \<^doc_class>\code\ is a general stub for free-form and type-checked code-fragments such as: + \<^enum> SML code + \<^enum> bash code + \<^enum> isar code (although this might be an unwanted concurrence + to the Isabelle standard cartouche) + \<^enum> C code. -it is intended that later refinements of this "stub" as done in \<^verbatim>\Isabelle_C\ which come with their +It is intended that later refinements of this "stub" as done in \<^verbatim>\Isabelle_C\ which come with their own content checking and, of course, presentation styles. \ From 583636404f32b623a4e8728aceed3a6923258047 Mon Sep 17 00:00:00 2001 From: Burkhart Wolff Date: Mon, 1 Aug 2022 21:50:49 +0200 Subject: [PATCH 3/3] renamed cenelec_document into cenelec_report. --- .../CENELEC_50128/CENELEC_50128.thy | 94 +++++++++---------- .../technical_report/technical_report.thy | 2 +- 2 files changed, 48 insertions(+), 48 deletions(-) diff --git a/src/ontologies/CENELEC_50128/CENELEC_50128.thy b/src/ontologies/CENELEC_50128/CENELEC_50128.thy index 71fdee6..088441d 100644 --- a/src/ontologies/CENELEC_50128/CENELEC_50128.thy +++ b/src/ontologies/CENELEC_50128/CENELEC_50128.thy @@ -601,7 +601,7 @@ doc_class judgement = section\ A Classification of CENELEC Reports and Documents \ (* should we rename this as "report" ??? bu *) -doc_class cenelec_document = text_element + +doc_class cenelec_report = text_element + phase :: "phase" sil :: "sil" level :: "int option" <= "Some(0)" @@ -641,61 +641,61 @@ doc_class SYS_VnV_pl = external_specification + phase :: "phase" <= "SYSDEV_ext" type_synonym system_VnV_plan = SYS_VnV_pl -doc_class SQAP = cenelec_document + +doc_class SQAP = cenelec_report + phase :: "phase" <= "SPl" nlvl :: "normative_level" <= "HR" invariant force_nlvl_sqap :: "nlvl \ = HR" type_synonym software_quality_assurance_plan = SQAP -doc_class SQAVR = cenelec_document + +doc_class SQAVR = cenelec_report + phase :: "phase" <= "SPl" nlvl :: "normative_level" <= "HR" invariant force_nlvl_sqavr :: "nlvl \ = HR" type_synonym software_quality_assurance_verfication_report = SQAVR -doc_class SCMP = cenelec_document + +doc_class SCMP = cenelec_report + phase :: "phase" <= "SPl" nlvl :: "normative_level" <= "HR" invariant force_nlvl_scmp :: "nlvl \ = HR" type_synonym software_configuration_management_plan = SCMP -doc_class SVP = cenelec_document + +doc_class SVP = cenelec_report + phase :: "phase" <= "SPl" nlvl :: "normative_level" <= "HR" invariant force_nlvl_svp :: "nlvl \ = HR" type_synonym software_verification_plan = SVP -doc_class SVAP = cenelec_document + +doc_class SVAP = cenelec_report + phase :: "phase" <= "SPl" nlvl :: "normative_level" <= "HR" invariant force_nlvl_svap :: "nlvl \ = HR" type_synonym software_validation_plan = SVAP -doc_class SWRS = cenelec_document + +doc_class SWRS = cenelec_report + phase :: "phase" <= "SR" nlvl :: "normative_level" <= "HR" invariant force_nlvl_swrs :: "nlvl \ = HR" type_synonym software_requirements_specification = SWRS -doc_class OSWTS = cenelec_document + +doc_class OSWTS = cenelec_report + phase :: "phase" <= "SR" nlvl :: "normative_level" <= "HR" invariant force_nlvl_oswts :: "nlvl \ = HR" type_synonym overall_software_test_specification = OSWTS -doc_class SWRVR = cenelec_document + +doc_class SWRVR = cenelec_report + phase :: "phase" <= "SR" nlvl :: "normative_level" <= "HR" invariant force_nlvl_swrvr :: "nlvl \ = HR" type_synonym software_requirements_verification_report = SWRVR -doc_class SWAS = cenelec_document + +doc_class SWAS = cenelec_report + phase :: "phase" <= "SADES" nlvl :: "normative_level" <= "HR" invariant force_nlvl_swas :: "nlvl \ = HR" type_synonym software_architecture_specification = SWAS -doc_class SWDS = cenelec_document + +doc_class SWDS = cenelec_report + phase :: "phase" <= "SADES" nlvl :: "normative_level" <= "HR" invariant force_nlvl_swds :: "nlvl \ = HR" @@ -712,7 +712,7 @@ doc_class SWIS_E = type_synonym software_interface_specification_element = SWIS_E -doc_class SWIS = cenelec_document + +doc_class SWIS = cenelec_report + phase :: "phase" <= "SADES" nlvl :: "normative_level" <= "HR" written_by :: "role option" <= "Some DES" @@ -722,198 +722,198 @@ doc_class SWIS = cenelec_document + invariant force_nlvl_swis :: "nlvl \ = HR" type_synonym software_interface_specifications = SWIS -doc_class SWITS = cenelec_document + +doc_class SWITS = cenelec_report + phase :: "phase" <= "SADES" nlvl :: "normative_level" <= "HR" invariant force_nlvl_swits :: "nlvl \ = HR" type_synonym software_integration_test_specification = SWITS -doc_class SWHITS = cenelec_document + +doc_class SWHITS = cenelec_report + phase :: "phase" <= "SADES" nlvl :: "normative_level" <= "HR" invariant force_nlvl_swhits :: "nlvl \ = HR" type_synonym software_hardware_integration_test_specification = SWHITS -doc_class SWADVR = cenelec_document + +doc_class SWADVR = cenelec_report + phase :: "phase" <= "SADES" nlvl :: "normative_level" <= "HR" invariant force_nlvl_swadvr :: "nlvl \ = HR" type_synonym software_architecture_and_design_verification = SWADVR -doc_class SWCDS = cenelec_document + +doc_class SWCDS = cenelec_report + phase :: "phase" <= "SCDES" invariant force_nlvl_swcds :: "if sil \ = SIL0 then nlvl \ = R else nlvl \ = HR" type_synonym software_component_design_specification = SWCDS -doc_class SWCTS = cenelec_document + +doc_class SWCTS = cenelec_report + phase :: "phase" <= "SCDES" invariant force_nlvl_swcts :: "if sil \ = SIL0 then nlvl \ = R else nlvl \ = HR" type_synonym software_component_test_specification = SWCTS -doc_class SWCDVR = cenelec_document + +doc_class SWCDVR = cenelec_report + phase :: "phase" <= "SCDES" invariant force_nlvl_swcdvr :: "if sil \ = SIL0 then nlvl \ = R else nlvl \ = HR" type_synonym software_component_design_verification = SWCDVR -doc_class SWSCD = cenelec_document + +doc_class SWSCD = cenelec_report + phase :: "phase" <= "CInT" nlvl :: "normative_level" <= "HR" invariant force_nlvl_swscd :: "nlvl \ = HR" type_synonym software_source_code_and_documentation = SWSCD -doc_class SWCTR = cenelec_document + +doc_class SWCTR = cenelec_report + phase :: "phase" <= "CInT" invariant force_nlvl_swctr :: "if sil \ = SIL0 then nlvl \ = R else nlvl \ = HR" type_synonym software_component_test_report = SWCTR -doc_class SWSCVR = cenelec_document + +doc_class SWSCVR = cenelec_report + phase :: "phase" <= "CInT" nlvl :: "normative_level" <= "HR" invariant force_nlvl_swscvr :: "nlvl \ = HR" type_synonym software_source_code_verification_report = SWSCVR -doc_class SWITR = cenelec_document + +doc_class SWITR = cenelec_report + phase :: "phase" <= "SI" nlvl :: "normative_level" <= "HR" invariant force_nlvl_switr :: "nlvl \ = HR" type_synonym software_integration_test_report = SWITR -doc_class SWHAITR = cenelec_document + +doc_class SWHAITR = cenelec_report + phase :: "phase" <= "SI" nlvl :: "normative_level" <= "HR" invariant force_nlvl_swhaitr :: "nlvl \ = HR" type_synonym software_hardware_integration_test_report = SWHAITR -doc_class SWIVR = cenelec_document + +doc_class SWIVR = cenelec_report + phase :: "phase" <= "SI" nlvl :: "normative_level" <= "HR" invariant force_nlvl_swivr :: "nlvl \ = HR" type_synonym software_integration_verification_report = SWIVR -doc_class OSWTR = cenelec_document + +doc_class OSWTR = cenelec_report + phase :: "phase" <= "SV" nlvl :: "normative_level" <= "HR" invariant force_nlvl_oswtr :: "nlvl \ = HR" type_synonym overall_software_test_report = OSWTR -doc_class SWVALR = cenelec_document + +doc_class SWVALR = cenelec_report + phase :: "phase" <= "SV" nlvl :: "normative_level" <= "HR" invariant force_nlvl_swvalr :: "nlvl \ = HR" type_synonym software_validation_report = SWVALR -doc_class TVALR = cenelec_document + +doc_class TVALR = cenelec_report + phase :: "phase" <= "SV" invariant force_nlvl_tvalr :: "if sil \ = SIL0 then nlvl \ = R else nlvl \ = HR" type_synonym tools_validation_report = TVALR -doc_class SWVRN = cenelec_document + +doc_class SWVRN = cenelec_report + phase :: "phase" <= "SV" nlvl :: "normative_level" <= "HR" invariant force_nlvl_swvrn :: "nlvl \ = HR" type_synonym software_validation_release_note = SWVRN -doc_class ARS = cenelec_document + +doc_class ARS = cenelec_report + phase :: "phase" <= "SCADA" nlvl :: "normative_level" <= "HR" invariant force_nlvl_ars :: "nlvl \ = HR" type_synonym application_requirements_specification = ARS -doc_class APP = cenelec_document + +doc_class APP = cenelec_report + phase :: "phase" <= "SCADA" nlvl :: "normative_level" <= "HR" invariant force_nlvl_APP :: "nlvl \ = HR" type_synonym application_preparation_plan = APP -doc_class ATS = cenelec_document + +doc_class ATS = cenelec_report + phase :: "phase" <= "SCADA" nlvl :: "normative_level" <= "HR" invariant force_nlvl_ats :: "nlvl \ = HR" type_synonym application_test_specification = ATS -doc_class AAD = cenelec_document + +doc_class AAD = cenelec_report + phase :: "phase" <= "SCADA" nlvl :: "normative_level" <= "HR" invariant force_nlvl_aad :: "nlvl \ = HR" type_synonym application_architecture_design = AAD -doc_class APVR = cenelec_document + +doc_class APVR = cenelec_report + phase :: "phase" <= "SCADA" nlvl :: "normative_level" <= "HR" invariant force_nlvl_apvr :: "nlvl \ = HR" type_synonym application_preparation_verification_report = APVR -doc_class ATR = cenelec_document + +doc_class ATR = cenelec_report + phase :: "phase" <= "SCADA" nlvl :: "normative_level" <= "HR" invariant force_nlvl_atr :: "nlvl \ = HR" type_synonym application_test_report= ATR -doc_class SOCOADA = cenelec_document + +doc_class SOCOADA = cenelec_report + phase :: "phase" <= "SCADA" nlvl :: "normative_level" <= "HR" invariant force_nlvl_socoada :: "nlvl \ = HR" type_synonym source_code_application_data_algorithms = SOCOADA -doc_class ADAVR = cenelec_document + +doc_class ADAVR = cenelec_report + phase :: "phase" <= "SCADA" nlvl :: "normative_level" <= "HR" invariant force_nlvl_adavr :: "nlvl \ = HR" type_synonym application_data_algorithms_verification_report= ADAVR -doc_class SWRDP = cenelec_document + +doc_class SWRDP = cenelec_report + phase :: "phase" <= "SD" invariant force_nlvl_swrdp :: "if sil \ = SIL0 then nlvl \ = R else nlvl \ = HR" type_synonym software_release_deployment_plan = SWRDP -doc_class SWDM = cenelec_document + +doc_class SWDM = cenelec_report + phase :: "phase" <= "SD" invariant force_nlvl_swdm :: "if sil \ = SIL0 then nlvl \ = R else nlvl \ = HR" type_synonym software_deployment_manual = SWDM -doc_class SWDRN = cenelec_document + +doc_class SWDRN = cenelec_report + phase :: "phase" <= "SD" nlvl :: "normative_level" <= "HR" invariant force_nlvl_swdrn :: "nlvl \ = HR" type_synonym software_deployment_release_notes = SWDRN -doc_class SWDR = cenelec_document + +doc_class SWDR = cenelec_report + phase :: "phase" <= "SD" invariant force_nlvl_swdr :: "if sil \ = SIL0 then nlvl \ = R else nlvl \ = HR" type_synonym software_deployment_records = SWDR -doc_class SWDVR = cenelec_document + +doc_class SWDVR = cenelec_report + phase :: "phase" <= "SD" invariant force_nlvl_swdvr :: "if sil \ = SIL0 then nlvl \ = R else nlvl \ = HR" type_synonym software_deployment_verification_report = SWDVR -doc_class SWMP = cenelec_document + +doc_class SWMP = cenelec_report + phase :: "phase" <= "SM" invariant force_nlvl_swmp :: "if sil \ = SIL0 then nlvl \ = R else nlvl \ = HR" type_synonym software_maintenance_plan = SWMP -doc_class SWCR = cenelec_document + +doc_class SWCR = cenelec_report + phase :: "phase" <= "SM" nlvl :: "normative_level" <= "HR" invariant force_nlvl_swcr :: "nlvl \ = HR" type_synonym software_change_records = SWCR -doc_class SWMR = cenelec_document + +doc_class SWMR = cenelec_report + phase :: "phase" <= "SM" invariant force_nlvl_swmr :: "if sil \ = SIL0 then nlvl \ = R else nlvl \ = HR" type_synonym software_maintenance_records = SWMR -doc_class SWMVR = cenelec_document + +doc_class SWMVR = cenelec_report + phase :: "phase" <= "SM" invariant force_nlvl_swmvr :: "if sil \ = SIL0 then nlvl \ = R else nlvl \ = HR" type_synonym software_maintenance_verification_report = SWMVR -doc_class SWAP = cenelec_document + +doc_class SWAP = cenelec_report + phase :: "phase" <= "SA" invariant force_nlvl_swap :: "if sil \ = SIL0 then nlvl \ = R else nlvl \ = HR" type_synonym software_assessment_plan = SWAP -doc_class SWAR = cenelec_document + +doc_class SWAR = cenelec_report + phase :: "phase" <= "SA" invariant force_nlvl_swar :: "if sil \ = SIL0 then nlvl \ = R else nlvl \ = HR" type_synonym software_assessment_report = SWAR diff --git a/src/ontologies/technical_report/technical_report.thy b/src/ontologies/technical_report/technical_report.thy index 48d9c33..0876379 100644 --- a/src/ontologies/technical_report/technical_report.thy +++ b/src/ontologies/technical_report/technical_report.thy @@ -48,7 +48,7 @@ text\The \<^doc_class>\code\ is a general stub for free-form \<^enum> C code. It is intended that later refinements of this "stub" as done in \<^verbatim>\Isabelle_C\ which come with their -own content checking and, of course, presentation styles. +own content checking and presentation styles. \ doc_class "SML" = code +