Towards the Design of Safety-Critical Software | Journal of Applied Research and Technology. JART

array:23 ["pii" => "S1665642313715761" "issn" => "16656423" "doi" => "10.1016/S1665-6423(13)71576-1" "estado" => "S300" "fechaPublicacion" => "2013-10-01" "aid" => "71576" "copyright" => "Universidad Nacional Autónoma de México" "copyrightAnyo" => "2013" "documento" => "article" "licencia" => "http://creativecommons.org/licenses/by-nc-nd/4.0/" "subdocumento" => "fla" "cita" => "Journal of Applied Research and Technology. 2013;11:683-94" "abierto" => array:3 [ "ES" => true "ES2" => true "LATM" => true ] "gratuito" => true "lecturas" => array:2 [ "total" => 947 "formatos" => array:3 [ "EPUB" => 29 "HTML" => 608 "PDF" => 310 ] ] "itemSiguiente" => array:18 [ "pii" => "S1665642313715773" "issn" => "16656423" "doi" => "10.1016/S1665-6423(13)71577-3" "estado" => "S300" "fechaPublicacion" => "2013-10-01" "aid" => "71577" "copyright" => "Universidad Nacional Autónoma de México" "documento" => "article" "licencia" => "http://creativecommons.org/licenses/by-nc-nd/4.0/" "subdocumento" => "fla" "cita" => "Journal of Applied Research and Technology. 2013;11:695-701" "abierto" => array:3 [ "ES" => true "ES2" => true "LATM" => true ] "gratuito" => true "lecturas" => array:2 [ "total" => 1267 "formatos" => array:3 [ "EPUB" => 35 "HTML" => 831 "PDF" => 401 ] ] "en" => array:11 [ "idiomaDefecto" => true "titulo" => "Fiber Optic Pressure Sensor of 0–0.36 psi by Multimode Interference Technique" "tienePdf" => "en" "tieneTextoCompleto" => "en" "tieneResumen" => array:2 [ 0 => "en" 1 => "es" ] "paginas" => array:1 [ 0 => array:2 [ "paginaInicial" => "695" "paginaFinal" => "701" ] ] "contieneResumen" => array:2 [ "en" => true "es" => true ] "contieneTextoCompleto" => array:1 [ "en" => true ] "contienePdf" => array:1 [ "en" => true ] "resumenGrafico" => array:2 [ "original" => 0 "multimedia" => array:7 [ "identificador" => "fig0025" "etiqueta" => "Figure 5" "tipo" => "MULTIMEDIAFIGURA" "mostrarFloat" => true "mostrarDisplay" => false "figura" => array:1 [ 0 => array:4 [ "imagen" => "gr5.jpeg" "Alto" => 579 "Ancho" => 616 "Tamanyo" => 53011 ] ] "descripcion" => array:1 [ "en" => "Sensor body." ] ] ] "autores" => array:1 [ 0 => array:2 [ "autoresLista" => "A.R. Mejia-Aranda, M.A. Basurto-Pensado, E.E. Antunez-Ceron, L.L. Castro-Gómez, G. Urquiza-Beltran, J.A. Rodriguez, J.C. García, J.J. Sánchez-Mondragón, V.I. Ruiz-Pérez" "autores" => array:9 [ 0 => array:2 [ "nombre" => "A.R." "apellidos" => "Mejia-Aranda" ] 1 => array:2 [ "nombre" => "M.A." "apellidos" => "Basurto-Pensado" ] 2 => array:2 [ "nombre" => "E.E." "apellidos" => "Antunez-Ceron" ] 3 => array:2 [ "nombre" => "L.L." "apellidos" => "Castro-Gómez" ] 4 => array:2 [ "nombre" => "G." "apellidos" => "Urquiza-Beltran" ] 5 => array:2 [ "nombre" => "J.A." "apellidos" => "Rodriguez" ] 6 => array:2 [ "nombre" => "J.C." "apellidos" => "García" ] 7 => array:2 [ "nombre" => "J.J." "apellidos" => "Sánchez-Mondragón" ] 8 => array:2 [ "nombre" => "V.I." "apellidos" => "Ruiz-Pérez" ] ] ] ] ] "idiomaDefecto" => "en" "EPUB" => "https://multimedia.elsevier.es/PublicationsMultimediaV1/item/epub/S1665642313715773?idApp=UINPBA00004N" "url" => "/16656423/0000001100000005/v2_201505081700/S1665642313715773/v2_201505081700/en/main.assets" ] "itemAnterior" => array:18 [ "pii" => "S166564231371575X" "issn" => "16656423" "doi" => "10.1016/S1665-6423(13)71575-X" "estado" => "S300" "fechaPublicacion" => "2013-10-01" "aid" => "71575" "copyright" => "Universidad Nacional Autónoma de México" "documento" => "article" "licencia" => "http://creativecommons.org/licenses/by-nc-nd/4.0/" "subdocumento" => "fla" "cita" => "Journal of Applied Research and Technology. 2013;11:674-82" "abierto" => array:3 [ "ES" => true "ES2" => true "LATM" => true ] "gratuito" => true "lecturas" => array:2 [ "total" => 3304 "formatos" => array:3 [ "EPUB" => 44 "HTML" => 2575 "PDF" => 685 ] ] "en" => array:11 [ "idiomaDefecto" => true "titulo" => "Temperature and Thermal Stresses of Vehicles Gray Cast Brake" "tienePdf" => "en" "tieneTextoCompleto" => "en" "tieneResumen" => "en" "paginas" => array:1 [ 0 => array:2 [ "paginaInicial" => "674" "paginaFinal" => "682" ] ] "contieneResumen" => array:1 [ "en" => true ] "contieneTextoCompleto" => array:1 [ "en" => true ] "contienePdf" => array:1 [ "en" => true ] "resumenGrafico" => array:2 [ "original" => 0 "multimedia" => array:7 [ "identificador" => "fig0005" "etiqueta" => "Figure 1" "tipo" => "MULTIMEDIAFIGURA" "mostrarFloat" => true "mostrarDisplay" => false "figura" => array:1 [ 0 => array:4 [ "imagen" => "gr1.jpeg" "Alto" => 493 "Ancho" => 806 "Tamanyo" => 72953 ] ] "descripcion" => array:1 [ "en" => "Disc-pads assembly with forces applied to the disc." ] ] ] "autores" => array:1 [ 0 => array:2 [ "autoresLista" => "A. Belhocine, M. Bouchetara" "autores" => array:2 [ 0 => array:2 [ "nombre" => "A." "apellidos" => "Belhocine" ] 1 => array:2 [ "nombre" => "M." "apellidos" => "Bouchetara" ] ] ] ] ] "idiomaDefecto" => "en" "EPUB" => "https://multimedia.elsevier.es/PublicationsMultimediaV1/item/epub/S166564231371575X?idApp=UINPBA00004N" "url" => "/16656423/0000001100000005/v2_201505081700/S166564231371575X/v2_201505081700/en/main.assets" ] "en" => array:14 [ "idiomaDefecto" => true "titulo" => "Towards the Design of Safety-Critical Software" "tieneTextoCompleto" => true "paginas" => array:1 [ 0 => array:2 [ "paginaInicial" => "683" "paginaFinal" => "694" ] ] "autores" => array:1 [ 0 => array:3 [ "autoresLista" => "R. Rafeh, A. Rabiee" "autores" => array:2 [ 0 => array:4 [ "nombre" => "R." "apellidos" => "Rafeh" "email" => array:1 [ 0 => "r-rafeh@araku.ac.ir" ] "referencia" => array:1 [ 0 => array:2 [ "etiqueta" => "1" "identificador" => "aff0010" ] ] ] 1 => array:4 [ "nombre" => "A." "apellidos" => "Rabiee" "email" => array:1 [ 0 => "arvand.rabiee@gmail.com" ] "referencia" => array:1 [ 0 => array:2 [ "etiqueta" => "1,2" "identificador" => "aff0005" ] ] ] ] "afiliaciones" => array:2 [ 0 => array:3 [ "entidad" => "Department of Computer Engineering Arak University Arak, Iran" "etiqueta" => "1,2" "identificador" => "aff0005" ] 1 => array:3 [ "entidad" => "Department of IT, Education Organization Arak, Iran" "etiqueta" => "2" "identificador" => "aff0010" ] ] ] ] "textoCompleto" => "1IntroductionComputers play a significant role in operating many modern systems some of which are classified as safety-critical. Any failure in safety-critical systems may result in loss of life or significant damage to the environment. Examples include medical systems, aircraft flight control systems, weapons and nuclear systems. When designing such systems, which usually include both software and hardware, the most important factor is safety. In this paper, we focus on the design of safety-critical software.The main approaches to improve the safety are divided into three classes: Theorem proving <a class="elsevierStyleCrossRef" href="#bib0005">[1]</a>, model checking <a class="elsevierStyleCrossRef" href="#bib0010">[2]</a> and runtime verification <a class="elsevierStyleCrossRef" href="#bib0015">[3]</a>. Current safety paradigms usually use one of the aforementioned approaches or a combination of them. For example, runtime reflection <a class="elsevierStyleCrossRef" href="#bib0015">[3]</a> employs runtime verification and the approach proposed in <a class="elsevierStyleCrossRef" href="#bib0020">[4]</a> uses a combination of theorem proving and model checking. Safety approaches like timed automata <a class="elsevierStyleCrossRef" href="#bib0025">[5]</a> and Event-B <a class="elsevierStyleCrossRef" href="#bib0030">[6]</a> usually use formal methods to specify the system requirements or monitor the system behavior. Formal languages such as Z <a class="elsevierStyleCrossRef" href="#bib0035">[7]</a>, is usually used to specify the system. For example, the approach proposed in <a class="elsevierStyleCrossRef" href="#bib0040">[8]</a> uses a combination of Petri-net and the Z language to verify medical software.However, the main issue with current approaches is that they are not taking into consideration all safety angles. We believe safety must be observed in all software production phases. Therefore, we propose a formal approach which takes into account all software production phases including planning, requirements specification, designing, and implementation <a class="elsevierStyleCrossRef" href="#bib0045">[9]</a>. We explain the proposed approach step by step using continuous infusion insulin pump (CIIP) which is a familiar safety-critical system.The paper is organized as follows: In <a class="elsevierStyleCrossRef" href="#sec0010">Section 2</a>, we explain briefly CIIP. In <a class="elsevierStyleCrossRef" href="#sec0015">Section 3</a>, we explain the steps that must be taken for achieving safety in CIIP based on the proposed approach. Finally, <a class="elsevierStyleCrossRef" href="#sec0020">Section 4</a> concludes the paper.2Continuous infusion insulin pumpDiabetes is a disease originated when the human body cannot produce enough insulin hormones. Insulin metabolizes the available sugar in the blood. The known therapy for diabetes consists in injecting enough insulin to the patient's blood. High blood sugar levels may hurt kidney, heart and eyes. Low blood sugar levels may paralyze brain and cause diabetic death. CIIP is a modern medical system for<a name="p684"></a> controlling the blood sugar levels by injecting the adequate doses of insulin to the patient's blood. This system takes blood samples every 10 minutes and checks its sugar level. Then the amount of necessary insulin is computed for injection in the blood <a class="elsevierStyleCrossRef" href="#bib0035">[7]</a>.3The proposed approachIn this section, we explain our approach in detail and use CIIP as an example. Our proposed approach consists of three steps as follows:Step one: In the first Step, we specify all safety requirements. For safety requirements we need to investigate the system in detail which includes the goals of the system, environments, users, operators, and preliminary resources. These goals are shown in <a class="elsevierStyleCrossRef" href="#tbl0005">Table 1</a> for CIIP.<elsevierMultimedia ident="tbl0005"></elsevierMultimedia>Some of the equipment needed in CIIP are sampling and injecting equipment, insulin resource, processor, LCD, and warning systems. A high level description of CIIP behavior is as follows: The system takes a sample of patient blood every 10 minutes, computes suitable insulin dose, and injects insulin to the patient's blood. High level safety approach for CIIP is depicted in <a class="elsevierStyleCrossRef" href="#tbl0010">Table 2</a>.<elsevierMultimedia ident="tbl0010"></elsevierMultimedia>For CIIP, the system requirements consist of realtime operating systems, some modeling tools, realtime programming languages and PCs. Hardware requirements consist of processors, memories, insulin reservoirs, sugar sampling equipment, insulin injection equipment, LCDs and power supplies. Functional requirements of CIIP are as follows:<ul class="elsevierStyleList" id="lis0005"><li class="elsevierStyleListItem" id="lsti0005">1.The system receives a sample of sugar blood every 10 minutes.</li><li class="elsevierStyleListItem" id="lsti0010">2.The system processes sugar blood and computes the sugar level.</li><li class="elsevierStyleListItem" id="lsti0015">3.The system computes insulin dose according to the last three sugar samples and injects insulin to the patient's blood.</li></ul>Nonfunctional requirements are usually data requirements extracted from medical documents. These requirements are the following:<ul class="elsevierStyleList" id="lis0010"><li class="elsevierStyleListItem" id="lsti0020">1.If the sugar level is smaller than the minimum value, the insulin dose is 0.</li><li class="elsevierStyleListItem" id="lsti0025">2.If the sugar level is between the minimum and the maximum value, then:<ul class="elsevierStyleList" id="lis0015"><li class="elsevierStyleListItem" id="lsti0030">•If the third sugar sample is smaller or equal to the second sample, insulin dose is 0.</li><li class="elsevierStyleListItem" id="lsti0035">•If the third sugar sample is greater than the second sample and the second sample is greater than the first one, and the difference between the third sample and the second one is smaller or equal than the difference between the second sample and the first one, insulin dose is 0.</li><li class="elsevierStyleListItem" id="lsti0040">•If the third sugar sample is greater than the second sample and the second sample is greater than the first one, and the difference between the third sample and the second one is smaller or equal than the difference between the second sample and the first one and the difference between the third and the second sample is smaller than 4, the insulin dose is the minimum value.</li><li class="elsevierStyleListItem" id="lsti0045">•If the third sugar sample is greater than the second sample and the second sample is greater than the first one, and the difference between the third sample and the second one is smaller or equal than the difference between the second sample and the first one and the difference between the third and the second sample is greater than 4, the insulin dose is the quotient of the difference between the third and the second sample by 4.<a name="p685"></a></li></ul></li><li class="elsevierStyleListItem" id="lsti0050">3.If the sugar level is greater than the maximum value, then:<ul class="elsevierStyleList" id="lis0020"><li class="elsevierStyleListItem" id="lsti0055">•If the third sugar sample is greater than the second sample and their difference is smaller than 4, the insulin dose is 0.</li><li class="elsevierStyleListItem" id="lsti0060">•If the third sugar sample is equal to the second sample, the insulin dose is 0.</li><li class="elsevierStyleListItem" id="lsti0065">•If the third sugar sample is smaller than the second sample and the difference between the third sample and the second one is smaller or equal than the difference between the second sample and the first one, the insulin dose is 0.</li><li class="elsevierStyleListItem" id="lsti0070">•If the third sugar sample is smaller than the second sample and the difference between the third sample and the second one is greater than the difference between the second sample and the first one, the insulin dose is the minimum value.</li></ul></li></ul>After specifying functional and nonfunctional requirements, we need to specify system hazards. Most of the hazard standards propose four hazard severity classes; catastrophic, critical, marginal, and negligible <a class="elsevierStyleCrossRef" href="#bib0060">[12]</a>. High level hazards for CIIP are shown in <a class="elsevierStyleCrossRef" href="#tbl0015">Table 3</a> according to this classification. The risk of each hazard can be determined using a combination of a digit and a letter which is shown in <a class="elsevierStyleCrossRef" href="#tbl0020">Table 4</a><a class="elsevierStyleCrossRef" href="#bib0065">[13]</a>.<elsevierMultimedia ident="tbl0015"></elsevierMultimedia><elsevierMultimedia ident="tbl0020"></elsevierMultimedia>FMEA is a technique used in combination of hazard analysis in the proposed approach. There are three FMEA classes: Structural FMEA used for hardware analysis, functional FMEA used for system functions analysis and Combined FMEA <a class="elsevierStyleCrossRef" href="#bib0065">[13]</a>. Structural FMEA worksheet and functional FMEA worksheet for CIIP are shown in Table 5 and Table 6, respectively. These tables are updated in the next phases of this step.Safety requirements may be defined in terms of constraints, chains of events, time constraints, fault tolerance equipment and warning interfaces. Safety requirements are classified as pure safety requirements, significant safety requirements, system safety requirements, and safety constraints <a class="elsevierStyleCrossRef" href="#bib0055">[11]</a>. This classification for CIIP is explained in detail in the following section. Each requirement must be mapped to at least one row of FMEA worksheets.Pure safety requirements:<ul class="elsevierStyleList" id="lis0025"><li class="elsevierStyleListItem" id="lsti0075">•System has not to have a risk in 1A rate</li></ul>Safety significant requirements:<ul class="elsevierStyleList" id="lis0030"><li class="elsevierStyleListItem" id="lsti0080">•If power is lower than the min level, a low power message has to be shown to the user and sampling operation must be suspended until power recharging takes place (rows 1, 2 from structural FMEA).</li><li class="elsevierStyleListItem" id="lsti0085">•Sampling equipment has to be tested automatically. Sampling operation must be stopped if this equipment does not work perfectly (row 3 from structural FMEA).</li><li class="elsevierStyleListItem" id="lsti0090">•Injecting equipment has to be tested automatically. Injecting operation must be stopped if this equipment does not work perfectly (row 6 from structural FMEA).<a name="p686"></a></li><li class="elsevierStyleListItem" id="lsti0095">•If the amount of insulin in the reservoir is smaller than the min insulin dose or specified injection dose, a low insulin message has to be shown to the user and injecting operation must be stopped (row 7 from structural FMEA).</li><li class="elsevierStyleListItem" id="lsti0100">•The amount of cumulative dose at the end of every 24 hours can be at most 25 doses (row 4 from structural FMEA, medical rules)</li></ul>Safety system requirements:<ul class="elsevierStyleList" id="lis0035"><li class="elsevierStyleListItem" id="lsti0105">•An electricity-current evaluator system equipped with current sensor, backup battery, and LCD (rows 1, 2 from structural FMEA).</li><li class="elsevierStyleListItem" id="lsti0110">•Insulin-level determinant system for insulin reservoir (row 7 from structural FMEA)</li><li class="elsevierStyleListItem" id="lsti0115">•Warning equipment (rows 1, 2 from structural FMEA and rows 1, 2 from functional FMEA)</li></ul><elsevierMultimedia ident="tbl0045"></elsevierMultimedia><a name="p687"></a>Safety constraints obtained from recommended reaction in FMEA worksheet with runtime management tag are as follows:<ul class="elsevierStyleList" id="lis0040"><li class="elsevierStyleListItem" id="lsti0120">•A sampling operation must be finished at most 10 seconds after sampling starts otherwise, a sampling failure message must be shown to the user and the system has to be turned off (row 1 from functional FMEA).</li><li class="elsevierStyleListItem" id="lsti0125">•An insulin injection is an atomic operation (row 2 from functional FMEA).</li><li class="elsevierStyleListItem" id="lsti0130">•If the sugar level is low, the system must avoid injecting insulin to the patient's blood (row 4 from functional FMEA).</li><li class="elsevierStyleListItem" id="lsti0135">•Insulin dose for injection must not exceed the max dose (row 4 from functional FMEA).</li><li class="elsevierStyleListItem" id="lsti0140">•Injecting operation must be finished at most 30 seconds after sampling starts otherwise, an injection failure message must be shown to the user and system has to be turned off (row 2 from functional FMEA).</li></ul>Step two: After identifying safety requirements, we model the system such that it satisfies all safety requirements <a class="elsevierStyleCrossRef" href="#bib0070">[14]</a>. We proposed two system units: operation unit that interacts with the environment (the patient) directly, and control unit that controls and supports the operation unit. Figure 1 shows this interactive model.We use timed transition Petri-net as the formal method because of its tractable behavior and its support of time. In addition, we use Z <a class="elsevierStyleCrossRef" href="#bib0085">[17]</a> to specify textual and mathematical specifications as a complement for Petri-net. A Petri-net model includes places, tokens, arcs and transitions. Each transition associates with a condition which, when holds, causes tokens on the transition to move to the next place. A Petri-net model for logical behavior of CIIP is shown in Figure 2.All transitions in Figure 2 are explained in <a class="elsevierStyleCrossRef" href="#tbl0025">Table 7</a> similar to the proposed model in <a class="elsevierStyleCrossRef" href="#bib0040">[8]</a>.<elsevierMultimedia ident="tbl0050"></elsevierMultimedia><a name="p688"></a><elsevierMultimedia ident="fig0005"></elsevierMultimedia><elsevierMultimedia ident="tbl0025"></elsevierMultimedia>As shown in Figure 2, the operation unit has four main states; Idle, Sampling, Computing, and Injecting. A token moves from Idle state to Injecting state when transitions are fired according to the conditions in <a class="elsevierStyleCrossRef" href="#tbl0025">Table 7</a>. Diagrams are not convenient tools to specify the requirements; instead, we use Z as a textual formal method to do so. Schemas 1 to 6 specify CIIP requirements similar to <a class="elsevierStyleCrossRef" href="#bib0040">[8]</a>. Each schema has a declaration part and a predicate part. For example schema 1 specifies states and their initial values. In this schema, insulinAvailable shows the available insulin in the reservoir. Also this schema has a predicate minimumDose that specifies the amount of minimum insulin for injection.the sugar level is high and low, respectively. Last three schemas specify computing state in the Petri-net model. Because the lack of space, we Schema 2 specifies the behavior of the system when running. Schema 3, specifies data requirements when the sugar level is normal. Schemas 4 and 5 specify data requirements when the sugar level is high and low, respectively. Last three schemas specify computing state in the Petri-net model. Because the lack of space, we ignore schemas for other states including sampling and injecting.<a name="p689"></a><a name="p690"></a><elsevierMultimedia ident="tbl0055"></elsevierMultimedia><elsevierMultimedia ident="tb0005"></elsevierMultimedia><elsevierMultimedia ident="tb0010"></elsevierMultimedia><elsevierMultimedia ident="tb0015"></elsevierMultimedia><elsevierMultimedia ident="tb0020"></elsevierMultimedia><a name="p693"></a>Step three: Even using the most sophisticated techniques for controlling the safety in both, requirements layer and design layer, it is always possible an unexpected error causes a system failure at runtime. Therefore, to avoid any system failure, we need to monitor the behavior of the system at runtime to identify and manage unexpected faults. In the proposed approach, all the main states of the system are monitored continuously in a structure which includes four units: Log management, change management, prevention management and disaster management which are based on information technology infrastructure library (ITIL) 20.Log management logs the main sates of the system when they change. As a result, all required states must be identified first. The main candidates for logging are those which changes may result in a critical behavior. Main critical behavior of CIIP is insulin injection; because incorrect insulin injection may hurt the patient seriously. Critical states that are in our concern shown in <a class="elsevierStyleCrossRef" href="#tbl0030">Table 8</a>. These states must be logged.<elsevierMultimedia ident="tbl0030"></elsevierMultimedia>Because critical behavior of the system may change over time, we need a change management unit to confirm that the change is safe. This unit is constructed from the high level constraints of the system and the environment conditions. Before giving permission to any critical behavior, required states are obtained from log management to ensure that all of them are safe. Change management unit plays a role in design, similar to the role of exception management in programming. <a class="elsevierStyleCrossRef" href="#tbl0035">Table 9</a> shows change permissions for the beginning of injecting critical behavior of CIIP. We can extend this table for other critical behaviors of CIIP which are in the second level of importance.<elsevierMultimedia ident="tbl0035"></elsevierMultimedia>To detect existing faults of the system before entering to critical states at runtime, a prevention management is required. Because CIIP is a real-time system, it is better to design prevention management such that it runs in parallel with the system. Schema 7 specifies prevention management in Z language for CIIP. When any condition in this schema fails, disaster management is called.Disaster management unit is a complement for the prevention unit. It tries to escape from faulty situations of the system, those which cannot be predicted in normal behavior and may lead to a catastrophic status. Disaster management can be as simple as showing a warning to the user, or as complex as replacing a redundant hardware, or as urgent as turning off the whole system. Disaster management for CIIP can be designed to turn off the system, show a message about system failure, and send a message to the patient's doctor through communication lines. <a class="elsevierStyleCrossRef" href="#tbl0040">Schema 8</a> specifies disaster management for CIIP in Z language.<a name="p694"></a>Emergency<elsevierMultimedia ident="tbl0040"></elsevierMultimedia>4ConclusionsAchieving a high degree of safety in safety-critical software requires that designers think about it carefully in each step of the software production. However, current approaches usually focus on safety in only one phase of the software production. In this paper, we proposed a multi-phase approach to achieve safety in safety-critical software. To describe the behavior of the system formally, we used timed transition Petri-net and the Z language. To show the proposed approach practically, we used CIIP as a sample model." "textoCompletoSecciones" => array:1 [ "secciones" => array:7 [ 0 => array:3 [ "identificador" => "xres498891" "titulo" => "Abstract" "secciones" => array:1 [ 0 => array:1 [ "identificador" => "abst0005" ] ] ] 1 => array:2 [ "identificador" => "xpalclavsec520380" "titulo" => "Keywords" ] 2 => array:2 [ "identificador" => "sec0005" "titulo" => "Introduction" ] 3 => array:2 [ "identificador" => "sec0010" "titulo" => "Continuous infusion insulin pump" ] 4 => array:3 [ "identificador" => "sec0015" "titulo" => "The proposed approach" "secciones" => array:1 [ 0 => array:2 [ "identificador" => "sec9005" "titulo" => "Emergency" ] ] ] 5 => array:2 [ "identificador" => "sec0020" "titulo" => "Conclusions" ] 6 => array:1 [ "titulo" => "References" ] ] ] "pdfFichero" => "main.pdf" "tienePdf" => true "PalabrasClave" => array:1 [ "en" => array:1 [ 0 => array:4 [ "clase" => "keyword" "titulo" => "Keywords" "identificador" => "xpalclavsec520380" "palabras" => array:4 [ 0 => "Safety-critical software" 1 => "hazard" 2 => "formal languages" 3 => "CIIP" ] ] ] ] "tieneResumen" => true "resumen" => array:1 [ "en" => array:2 [ "titulo" => "Abstract" "resumen" => "Safety is the most important factor when developing software for safety-critical systems. Traditional approaches attempted to achieve safety through testing the software. However, there might be some bugs in the software not revealed in the test procedure. Formal verification is a new trend in developing safe software. In this paper, we propose a multi-phase formal approach for safety management in safety-critical software. We use timed transition Petri-net as a formal means to specify the properties of the model and their relations in each component of the software. In addition, we use the Z language to specify textual and mathematical specifications of the model, as a representative model to evaluate the proposed approach; we chose continuous infusion insulin pump (CIIP)." ] ] "multimedia" => array:16 [ 0 => array:7 [ "identificador" => "tbl0005" "etiqueta" => "Table 1" "tipo" => "MULTIMEDIATABLA" "mostrarFloat" => true "mostrarDisplay" => false "tabla" => array:1 [ "tablatextoimagen" => array:1 [ 0 => array:2 [ "tabla" => array:1 [ 0 => """ <table border="0" frame="\n \t\t\t\t\tvoid\n \t\t\t\t" class=""><tbody title="tbody"><tr title="table-row"><td class="td" title="table-entry " align="center" valign="middle">Goals \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="left" valign="middle">To control sugar level in a diabetic patient and to inject automatically the correct insulin dose. \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="center" valign="middle">Environment \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="left" valign="middle">Patient's body \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="center" valign="middle">Users \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="left" valign="middle">Patient, doctor \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="center" valign="middle">Operators \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="left" valign="middle">– \t\t\t\t\t\t\n \t\t\t\t</td></tr></tbody></table> """ ] "imagenFichero" => array:1 [ 0 => "xTab796438.png" ] ] ] ] "descripcion" => array:1 [ "en" => "Preliminary information about CIIP." ] ] 1 => array:7 [ "identificador" => "tbl0010" "etiqueta" => "Table 2" "tipo" => "MULTIMEDIATABLA" "mostrarFloat" => true "mostrarDisplay" => false "tabla" => array:1 [ "tablatextoimagen" => array:1 [ 0 => array:2 [ "tabla" => array:1 [ 0 => """ <table border="0" frame="\n \t\t\t\t\tvoid\n \t\t\t\t" class=""><thead title="thead"><tr title="table-row"><th class="td" title="table-head " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black">No. \t\t\t\t\t\t\n \t\t\t\t</th><th class="td" title="table-head " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black">Road map \t\t\t\t\t\t\n \t\t\t\t</th></tr></thead><tbody title="tbody"><tr title="table-row"><td class="td" title="table-entry " align="center" valign="middle">1 \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="left" valign="middle">Sugar status have to be reported to the patient periodically \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="center" valign="middle">2 \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="left" valign="middle">Warn to the user before insulin resource gets empty \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="center" valign="middle">3 \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="left" valign="middle">Warn to the user when power is low \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="center" valign="middle">4 \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="left" valign="middle">System has not to hurt the patient \t\t\t\t\t\t\n \t\t\t\t</td></tr></tbody></table> """ ] "imagenFichero" => array:1 [ 0 => "xTab796436.png" ] ] ] ] "descripcion" => array:1 [ "en" => "Safety approach for CIIP." ] ] 2 => array:7 [ "identificador" => "tbl0015" "etiqueta" => "Table 3" "tipo" => "MULTIMEDIATABLA" "mostrarFloat" => true "mostrarDisplay" => false "tabla" => array:1 [ "tablatextoimagen" => array:1 [ 0 => array:2 [ "tabla" => array:1 [ 0 => """ <table border="0" frame="\n \t\t\t\t\tvoid\n \t\t\t\t" class=""><thead title="thead"><tr title="table-row"><th class="td" title="table-head " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black">Hazard \t\t\t\t\t\t\n \t\t\t\t</th><th class="td" title="table-head " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black">Severity \t\t\t\t\t\t\n \t\t\t\t</th></tr></thead><tbody title="tbody"><tr title="table-row"><td class="td" title="table-entry " align="center" valign="middle">Power supply fault \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Critical \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="center" valign="middle">Sampling equipment fault \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Critical \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="center" valign="middle">Insulin dose computing fault \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Catastrophic \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="center" valign="middle">Injection equipment fault \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Critical \t\t\t\t\t\t\n \t\t\t\t</td></tr></tbody></table> """ ] "imagenFichero" => array:1 [ 0 => "xTab796434.png" ] ] ] ] "descripcion" => array:1 [ "en" => "High level hazard classification for CIIP <a class="elsevierStyleCrossRef" href="#bib0060">[12]</a>." ] ] 3 => array:7 [ "identificador" => "tbl0020" "etiqueta" => "Table 4" "tipo" => "MULTIMEDIATABLA" "mostrarFloat" => true "mostrarDisplay" => false "tabla" => array:1 [ "tablatextoimagen" => array:1 [ 0 => array:2 [ "tabla" => array:1 [ 0 => """ <table border="0" frame="\n \t\t\t\t\tvoid\n \t\t\t\t" class=""><tbody title="tbody"><tr title="table-row"><td class="td" title="table-entry " rowspan="4" align="center" valign="middle" style="border-bottom: 2px solid black">Severity</td><td class="td" title="table-entry " align="left" valign="middle" style="border-bottom: 2px solid black">1. Catastrophic \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="left" valign="middle" style="border-bottom: 2px solid black">2. Critical \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="left" valign="middle" style="border-bottom: 2px solid black">3. Marginal \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="left" valign="middle" style="border-bottom: 2px solid black">4. Negligible \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " rowspan="5" align="center" valign="middle">Probability</td><td class="td" title="table-entry " align="left" valign="middle" style="border-bottom: 2px solid black">A. Frequent \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="left" valign="middle" style="border-bottom: 2px solid black">B. Probable \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="left" valign="middle" style="border-bottom: 2px solid black">C. Occasional \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="left" valign="middle" style="border-bottom: 2px solid black">D. Remote \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="left" valign="middle">E. Improbable \t\t\t\t\t\t\n \t\t\t\t</td></tr></tbody></table> """ ] "imagenFichero" => array:1 [ 0 => "xTab796437.png" ] ] ] ] "descripcion" => array:1 [ "en" => "Hazard risk factor 13." ] ] 4 => array:7 [ "identificador" => "tbl0025" "etiqueta" => "Table 7" "tipo" => "MULTIMEDIATABLA" "mostrarFloat" => true "mostrarDisplay" => false "tabla" => array:1 [ "tablatextoimagen" => array:1 [ 0 => array:2 [ "tabla" => array:1 [ 0 => """ <table border="0" frame="\n \t\t\t\t\tvoid\n \t\t\t\t" class=""><thead title="thead"><tr title="table-row"><th class="td" title="table-head " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black">Transition \t\t\t\t\t\t\n \t\t\t\t</th><th class="td" title="table-head " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black">Events or conditions \t\t\t\t\t\t\n \t\t\t\t</th></tr></thead><tbody title="tbody"><tr title="table-row"><td class="td" title="table-entry " align="center" valign="middle">T1 \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Sugar > SafeMax \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="center" valign="middle">T2 \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Sugar <=SafeMax \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="center" valign="middle">T3 \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Sugar < SafeMin \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="center" valign="middle">T4 \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Sugar >= SafeMin \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="center" valign="middle">T5 \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Time >= 10 \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="center" valign="middle">T6 \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">E1: EndSampling \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="center" valign="middle">T7 \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Time >= 10 \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="center" valign="middle">T8 \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">E1: EndSampling \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="center" valign="middle">T9 \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Time >= 10 \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="center" valign="middle">T10 \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">E1: EndSampling \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="center" valign="middle">T11 \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Time >= 10 \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="center" valign="middle">T12 \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">E1: EndSampling \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="center" valign="middle">T13 \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">E2: EndComputing \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="center" valign="middle">T14 \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">E3: EndInjecting \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="center" valign="middle">T15 \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Insulin < MinDose Or Insulin < ComputedDose OR Charge < MinCharge \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="center" valign="middle">T16 \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Insulin >= MinDose AND Insulin >= ComputedDose AND Charge >= MinCharge \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="center" valign="middle">T17 \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Charge < MinCharge \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="center" valign="middle">T18 \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Charge >= MinCharge \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="center" valign="middle">T19 \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Insulin < MinDose \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="center" valign="middle">T20 \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Insulin >= MinDose \t\t\t\t\t\t\n \t\t\t\t</td></tr></tbody></table> """ ] "imagenFichero" => array:1 [ 0 => "xTab796430.png" ] ] ] ] "descripcion" => array:1 [ "en" => "Transitions on the CIIP Petri-net model." ] ] 5 => array:7 [ "identificador" => "tbl0030" "etiqueta" => "Table 8" "tipo" => "MULTIMEDIATABLA" "mostrarFloat" => true "mostrarDisplay" => false "tabla" => array:1 [ "tablatextoimagen" => array:1 [ 0 => array:2 [ "tabla" => array:1 [ 0 => """ <table border="0" frame="\n \t\t\t\t\tvoid\n \t\t\t\t" class=""><thead title="thead"><tr title="table-row"><th class="td" title="table-head " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black">State name \t\t\t\t\t\t\n \t\t\t\t</th><th class="td" title="table-head " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black">Conception \t\t\t\t\t\t\n \t\t\t\t</th><th class="td" title="table-head " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black">Log times \t\t\t\t\t\t\n \t\t\t\t</th><th class="td" title="table-head " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black">Details \t\t\t\t\t\t\n \t\t\t\t</th></tr></thead><tbody title="tbody"><tr title="table-row"><td class="td" title="table-entry " align="center" valign="middle">Charge \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Power supply energy \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Every minute, after warning enabled or warning disabled \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">– \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="center" valign="middle">insulinAvailable \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Available insulin in reservoir \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Every minute, after warning enabled or warning disabled \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">– \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="center" valign="middle">computed Dose \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Computed dose \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Immediately after end of computing operation \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">After the end of the injecting operation the amount of this log become zero \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="center" valign="middle">cumulativ eDose \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Cumulative dose \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Immediately after the end of the injecting operation \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">After every 24 hours, the amount of this log become zero \t\t\t\t\t\t\n \t\t\t\t</td></tr></tbody></table> """ ] "imagenFichero" => array:1 [ 0 => "xTab796433.png" ] ] ] ] "descripcion" => array:1 [ "en" => "Critical states of CIIP." ] ] 6 => array:7 [ "identificador" => "tbl0035" "etiqueta" => "Table 9" "tipo" => "MULTIMEDIATABLA" "mostrarFloat" => true "mostrarDisplay" => false "tabla" => array:1 [ "tablatextoimagen" => array:1 [ 0 => array:2 [ "tabla" => array:1 [ 0 => """ <table border="0" frame="\n \t\t\t\t\tvoid\n \t\t\t\t" class=""><thead title="thead"><tr title="table-row"><th class="td" title="table-head " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black">Critical behavior \t\t\t\t\t\t\n \t\t\t\t</th><th class="td" title="table-head " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black">Conditions \t\t\t\t\t\t\n \t\t\t\t</th><th class="td" title="table-head " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black">Permission \t\t\t\t\t\t\n \t\t\t\t</th></tr></thead><tbody title="tbody"><tr title="table-row"><td class="td" title="table-entry " rowspan="2" align="center" valign="middle">Beginning of the injecting operation</td><td class="td" title="table-entry " align="center" valign="middle">Charge > minCharge AND insulinavailable > minDose AND ComputedDose > 0 AND cumulativeDose <=25 \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">True \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="center" valign="middle">∼( Charge > minCharge AND insulinavailable > minDose AND ComputedDose > 0 AND cumulativeDose <=25) \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">False \t\t\t\t\t\t\n \t\t\t\t</td></tr></tbody></table> """ ] "imagenFichero" => array:1 [ 0 => "xTab796432.png" ] ] ] ] "descripcion" => array:1 [ "en" => "Change permissions for critical behavior of CIIP" ] ] 7 => array:7 [ "identificador" => "tbl0040" "etiqueta" => "Schema 8" "tipo" => "MULTIMEDIATABLA" "mostrarFloat" => true "mostrarDisplay" => false "tabla" => array:1 [ "tablatextoimagen" => array:1 [ 0 => array:2 [ "tabla" => array:1 [ 0 => """ <table border="0" frame="\n \t\t\t\t\tvoid\n \t\t\t\t" class=""><tbody title="tbody"><tr title="table-row"><td class="td" title="table-entry " align="left" valign="middle">Δ PUBLIC_STATES \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="left" valign="middle">systemStatus = standby \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="left" valign="middle">systemState = sendingMessage \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="left" valign="middle">warnningAlarml! − on \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="left" valign="middle">warnningAlarm2! = on \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="left" valign="middle">messagel! = “System Failure” \t\t\t\t\t\t\n \t\t\t\t</td></tr></tbody></table> """ ] "imagenFichero" => array:1 [ 0 => "xTab796435.png" ] ] ] ] "descripcion" => array:1 [ "en" => "Disaster management for CIIP in the Z language." ] ] 8 => array:6 [ "identificador" => "fig0005" "tipo" => "MULTIMEDIAFIGURA" "mostrarFloat" => false "mostrarDisplay" => true "figura" => array:1 [ 0 => array:4 [ "imagen" => "gr1.jpeg" "Alto" => 774 "Ancho" => 1680 "Tamanyo" => 121344 ] ] "descripcion" => array:1 [ "en" => " " ] ] 9 => array:5 [ "identificador" => "tbl0045" "tipo" => "MULTIMEDIATABLA" "mostrarFloat" => false "mostrarDisplay" => true "tabla" => array:1 [ "tablatextoimagen" => array:1 [ 0 => array:2 [ "tabla" => array:1 [ 0 => """ <table border="0" frame="\n \t\t\t\t\tvoid\n \t\t\t\t" class=""><thead title="thead"><tr title="table-row"><th class="td" title="table-head " colspan="12" align="center" valign="middle" scope="col" style="border-bottom: 2px solid black">Fmea</th></tr><tr title="table-row"><th class="td" title="table-head " colspan="5" align="left" valign="middle" scope="col" style="border-bottom: 2px solid black">System: CIIP</th><th class="td" title="table-head " colspan="7" align="left" valign="middle" scope="col" style="border-bottom: 2px solid black">Subsystem: -</th></tr><tr title="table-row"><th class="td" title="table-head " colspan="12" align="left" valign="middle" scope="col">Mode/Phase: Operating</th></tr><tr title="table-row"><th class="td" title="table-head " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black">Component \t\t\t\t\t\t\n \t\t\t\t</th><th class="td" title="table-head " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black">Failure mode \t\t\t\t\t\t\n \t\t\t\t</th><th class="td" title="table-head " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black">Failure rate \t\t\t\t\t\t\n \t\t\t\t</th><th class="td" title="table-head " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black">Failure reasons \t\t\t\t\t\t\n \t\t\t\t</th><th class="td" title="table-head " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black">Suddenly effect \t\t\t\t\t\t\n \t\t\t\t</th><th class="td" title="table-head " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black">System effect \t\t\t\t\t\t\n \t\t\t\t</th><th class="td" title="table-head " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black">Detection method \t\t\t\t\t\t\n \t\t\t\t</th><th class="td" title="table-head " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black">Current control \t\t\t\t\t\t\n \t\t\t\t</th><th class="td" title="table-head " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black">Hazard \t\t\t\t\t\t\n \t\t\t\t</th><th class="td" title="table-head " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black">Hazard risk \t\t\t\t\t\t\n \t\t\t\t</th><th class="td" title="table-head " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black">Recommended action \t\t\t\t\t\t\n \t\t\t\t</th><th class="td" title="table-head " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black">row \t\t\t\t\t\t\n \t\t\t\t</th></tr></thead><tbody title="tbody"><tr title="table-row"><td class="td" title="table-entry " rowspan="2" align="center" valign="middle">Power supply</td><td class="td" title="table-entry " align="center" valign="middle">Failed \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">1.1 * 10–9 (manufacture information) \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Control circuit failed \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Electricity current disconnection \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">System downs \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Current test \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Quality control \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Sugar level increasing \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">2B \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Using from a current sensor with backup battery to warn user power supply is failed \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">1 \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="center" valign="middle">Energy decreasing \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Not available \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Battery energy decreasing \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Electricity current decreasing \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">System incorrect action \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Current test \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">– \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Sugar level increasing \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">2B \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Using from a current sensor with backup battery to warn user change the system battery \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">2 \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="center" valign="middle">Sampling subsystem \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Failed \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">5 * 10–4 (manufacture information) \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Hardware fault \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Not receiving sugar sample \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Not computing and injecting insulin dose \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Inspecting \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Quality control \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Sugar level increasing \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">2B \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Automatic test \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">3 \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " rowspan="2" align="center" valign="middle">Insulin dose computing subsystem</td><td class="td" title="table-entry " align="center" valign="middle">Failed \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Not available \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Hardware fault \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Not computing insulin dose \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Not injecting insulin dose \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">System testing \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">– \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">_Sugar level increasing \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">2B \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">– \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">4 \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="center" valign="middle">Computing fault \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">– \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Hardware fault, programming fault \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Not computing insulin dose \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Unsafe system behavior \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">System testing \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Software testing \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Serious hurt to patient \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">1A \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Hard testing \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">5 \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " rowspan="2" align="center" valign="middle">Injecting subsystem</td><td class="td" title="table-entry " align="center" valign="middle">Failed \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">5 * 10−4 (manufacture information) \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Hardware fault \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Not injecting insulin dose \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Not injecting insulin dose \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Inspection \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Quality control \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Sugar level increasing \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">2B \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Automatic test \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">6 \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="center" valign="middle">Not enough insulin \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">– \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Not charging insulin reservoir \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Not injecting insulin dose \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Not injecting insulin dose \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Resource inspection \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">– \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Sugar level increasing \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">2B \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Using from a sensor to assess reservoir insulin level \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">7 \t\t\t\t\t\t\n \t\t\t\t</td></tr></tbody></table> """ ] "imagenFichero" => array:1 [ 0 => "xTab796440.png" ] ] ] ] ] 10 => array:5 [ "identificador" => "tbl0050" "tipo" => "MULTIMEDIATABLA" "mostrarFloat" => false "mostrarDisplay" => true "tabla" => array:1 [ "tablatextoimagen" => array:1 [ 0 => array:2 [ "tabla" => array:1 [ 0 => """ <table border="0" frame="\n \t\t\t\t\tvoid\n \t\t\t\t" class=""><thead title="thead"><tr title="table-row"><th class="td" title="table-head " colspan="12" align="center" valign="middle" scope="col" style="border-bottom: 2px solid black">Fmea</th></tr><tr title="table-row"><th class="td" title="table-head " colspan="6" align="left" valign="middle" scope="col" style="border-bottom: 2px solid black">System: CIIP</th><th class="td" title="table-head " colspan="6" align="left" valign="middle" scope="col" style="border-bottom: 2px solid black">Subsystem: -</th></tr><tr title="table-row"><th class="td" title="table-head " colspan="12" align="left" valign="middle" scope="col">Mode/Phase: Operating</th></tr><tr title="table-row"><th class="td" title="table-head " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black">Function \t\t\t\t\t\t\n \t\t\t\t</th><th class="td" title="table-head " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black">Failure mode \t\t\t\t\t\t\n \t\t\t\t</th><th class="td" title="table-head " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black">Failure rate \t\t\t\t\t\t\n \t\t\t\t</th><th class="td" title="table-head " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black">Failure reasons \t\t\t\t\t\t\n \t\t\t\t</th><th class="td" title="table-head " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black">Suddenly effect \t\t\t\t\t\t\n \t\t\t\t</th><th class="td" title="table-head " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black">System effects \t\t\t\t\t\t\n \t\t\t\t</th><th class="td" title="table-head " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black">Detection method \t\t\t\t\t\t\n \t\t\t\t</th><th class="td" title="table-head " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black">Current control \t\t\t\t\t\t\n \t\t\t\t</th><th class="td" title="table-head " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black">Hazard \t\t\t\t\t\t\n \t\t\t\t</th><th class="td" title="table-head " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black">Hazard risk \t\t\t\t\t\t\n \t\t\t\t</th><th class="td" title="table-head " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black">Recommended action \t\t\t\t\t\t\n \t\t\t\t</th><th class="td" title="table-head " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black">Row \t\t\t\t\t\t\n \t\t\t\t</th></tr></thead><tbody title="tbody"><tr title="table-row"><td class="td" title="table-entry " align="center" valign="middle">Sampling \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Not happening \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Not available \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Hardware fault, software fault \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Not receiving sample \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Nor computing nor injecting insulin \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Not resetting new sample \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">– \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Face to unsafe status \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">2B \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Warn to user after 10 second (runtime safety management) \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">1 \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " rowspan="3" align="center" valign="middle">Insulin injecting</td><td class="td" title="table-entry " align="center" valign="middle">Not happening \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Not available \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Insulin reservoir is empty, hardware fault, software fault \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Not injecting insulin \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Injecting incorrect dose in the next injection \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Not resetting new sample \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">– \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Increasing sugar level \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">2B \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Warn the user after 30 second (runtime safety management) \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">2 \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="center" valign="middle">Injecting lower dose than specified \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Not available \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">leakage of insulin in reservoir, hardware fault, software fault \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">– \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Injecting incorrect dose in the next injection \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">– \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">– \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Increasing sugar level \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">2B \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Transactional injecting (runtime safety management) \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">3 \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="center" valign="middle">Injecting higher dose than specified \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Not available \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Hardware fault, software fault \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">– \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Injecting incorrect dose in the next injection \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">– \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">– \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Patient going to a coma \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">1A \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">Daily injection control, hard testing, injection guards (runtime safety management) \t\t\t\t\t\t\n \t\t\t\t</td><td class="td" title="table-entry " align="center" valign="middle">4 \t\t\t\t\t\t\n \t\t\t\t</td></tr></tbody></table> """ ] "imagenFichero" => array:1 [ 0 => "xTab796431.png" ] ] ] ] ] 11 => array:5 [ "identificador" => "tbl0055" "tipo" => "MULTIMEDIATABLA" "mostrarFloat" => false "mostrarDisplay" => true "tabla" => array:1 [ "tablatextoimagen" => array:1 [ 0 => array:2 [ "tabla" => array:1 [ 0 => """ <table border="0" frame="\n \t\t\t\t\tvoid\n \t\t\t\t" class=""><tbody title="tbody"><tr title="table-row"><td class="td" title="table-entry " align="left" valign="middle">insulinAvailable : N // amount of insulin in the reservoir \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="left" valign="middle">computedDose : N // amount of computed insulin dose \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="left" valign="middle">cumulativeDose : N // sum of insulin doses that were injected in current day \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="left" valign="middle">injectionDose : N // amount of insulin dose that must be injected \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="left" valign="middle">safeMin : N // one limit more or less than it means blood sugar is low \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="left" valign="middle">safeMax : N // one limit bigger than it means blood sugar is high \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="left" valign="middle">maxDailyDose : N // maximum insulin dose is legal to be injected in one day \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="left" valign="middle">maxSingleDose : N // maximum insulin dose is legal to be injected in a ten-minute cycle \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="left" valign="middle">minimumDose : N // minimum insulin dose can be injected \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="left" valign="middle">first_sample, second_sample, third_sample : N // three last blood sugar of diabetic \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="left" valign="middle">charge : {1, 2, 3, 4, 5, 6, 7, 8} // amount of the power charge \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="left" valign="middle">minCharge : {1, 2, 3, 4, 5, 6, 7, 8} // minimum allowed amount of the power charge \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="left" valign="middle">warningAlarm1! : {on, off} //to show a power warning to the diabetic \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="left" valign="middle">warningAlarm2! : {on, off} // to show a insulin warning to the diabetic \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="left" valign="middle">message1! : string // showing a warning about power charge \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="left" valign="middle">message2! : string // showing a warning about available insulin in the reservoir \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="left" valign="middle">systemStatus : { run, standby} // status of system running \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="left" valign="middle">systemState : {sampling, computing, injecting, sendingMessage} // states of system clock? : TIME //inputted time \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="left" valign="middle">clock! TIME //outputted time \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="left" valign="middle">// configuration parameters \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="left" valign="middle">minimumDose = 1 \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="left" valign="middle">safeMin = 6 \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="left" valign="middle">safeMax = 14 \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="left" valign="middle">maxDailyDose = 25 \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="left" valign="middle">maxSingleDose = 4 \t\t\t\t\t\t\n \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry " align="left" valign="middle">minCharge = 2 \t\t\t\t\t\t\n \t\t\t\t</td></tr></tbody></table> """ ] "imagenFichero" => array:1 [ 0 => "xTab796439.png" ] ] ] ] ] 12 => array:5 [ "identificador" => "tb0005" "tipo" => "MULTIMEDIATEXTO" "mostrarFloat" => false "mostrarDisplay" => true "texto" => array:1 [ "textoCompleto" => "ΔPUBLIC_STATESclock? = 001000 ➔ (clock! = 000000) ∧ (injectionDose' = 0) ∧ (computedDose' = 0) A (first_sample' =second_sample) ∧ (second _sample' = third_sample) ∧ (third _sample' = 0)systemStatus = run ∨ standby// dose of insulin is computed depending on the blood sugar levelSUGAR_NORMAL ∨ SUGAR_HIGH ∨ SUGAR_LOW// safety rulesSAFETYcumulativeDose' = cumulativeDose + injectionDose<a name="p691"></a>systemStatus = runsystemState = Computing(third_sample >= safeMin) ∧ (third_sample <= safeMax)// sugar level stable or falling(third_sample <= second_sample)➔(computedDose = 0)// sugar level increases but rate of increase falls(third_sample > second_sample) ∧(third_sample - second_sample) < (second_sample - first_sample)➔(computedDose = 0)// sugar level increases and rate of increase increases compute dose// a minimum dose must be delivered if rounded to zero(third_sample > second_sample) ∧(third_sample - second_sample) >= (second_sample - first_sample)∧(round((third_sample - second_sample)/4) = 0) ➔(computedDose = minimumDose)(third_sample > second_sample) A(third_sample - second_sample) >= (second_sample - first_sample)∧(round((third_sample - second_sample)/4) > 0) ➔(computedDose = round((third_sample -second_sample)/4)" ] ] 13 => array:5 [ "identificador" => "tb0010" "tipo" => "MULTIMEDIATEXTO" "mostrarFloat" => false "mostrarDisplay" => true "texto" => array:1 [ "textoCompleto" => "S ystemStatus = runsystemState = Computingthird_sample > safeMax// sugar level increasing. Round down if below 1 unit(third_sample > second_sample) ∧(round((third_sample- second_sample)/4) = 0) ➔(computedDose =minimumDose)(third_sample > second_sample) ∧(round((third_sample-second_sample)/4) > 0) ∧(computedDose =round((third_sample - second_sample)/4))// sugarlevel stable(third_sample = second_sample) ➔(computedDose = minimumDose)// sugar level falling and rate of increase decreasing(third_sample < second_sample) ∧(third_sample - second_sample) <= (second_sample - first_sample)➔(computedDose = 0)// sugar level falling and rate of increase increasing(third_sample < second_sample) ∧(third_sample - second_sample) > (second_sample - first_sample)➔(computedDose = minimumDose)<a name="p692"></a>systemStatus = runsystemState = Computingthird_sample < safeMincomputedDose = 0warningAlarm! = onmessage! = “Your sugar is very low. Please call your doctor.”" ] ] 14 => array:5 [ "identificador" => "tb0015" "tipo" => "MULTIMEDIATEXTO" "mostrarFloat" => false "mostrarDisplay" => true "texto" => array:1 [ "textoCompleto" => "charge < minCharge ➔ (warningAlarm1! = on) ∧ (messag e1!= “Low charge.”) A (systemStatus = standby)charge >= minCharge ➔ (warningAlarm1! = off) ∧ (message1! = “”) ➔ (systemStatus = run)(insulinAvailable < minDose ) ∨ (insulinAvailable < injectionDose) ➔ (warningAlarm2! = on) A (message2! =“Low insulin.”) ∧ (systemStatus = standby)(insulinAvailable > minDose ) ∨ (insulinAvailable > injectionDose) ➔ (warningAlarm2! = off) A (message2! =’”) A (systemStatus = run)cumulativeDose <= 25 ➔ injectionDose = computedDosecumulativeDose > 25 ➔ injectionDose = 0" ] ] 15 => array:5 [ "identificador" => "tb0020" "tipo" => "MULTIMEDIATEXTO" "mostrarFloat" => false "mostrarDisplay" => true "texto" => array:1 [ "textoCompleto" => "Δ PUBLIC_STATESsystemState = sampling ➔ clock? <= 000010systemState = injecting ➔ (injectionDose > 0) ∧ (insulinAvailable >= injectionDose) ∧ (charge >=minCharge)third_sample < safeMin ➔ injectionDose = 0injectionDose <= maxDosesystemState = injecting ➔ clock? <= 000030" ] ] ] "bibliografia" => array:2 [ "titulo" => "References" "seccion" => array:1 [ 0 => array:2 [ "identificador" => "bibs0005" "bibliografiaReferencia" => array:20 [ 0 => array:3 [ "identificador" => "bib0005" "etiqueta" => "[1]" "referencia" => array:1 [ 0 => array:2 [ "contribucion" => array:1 [ 0 => array:1 [ "autores" => array:1 [ 0 => array:2 [ "etal" => false "autores" => array:2 [ 0 => "J. Slagle" 1 => "S. Shankar" ] ] ] ] ] "host" => array:1 [ 0 => array:1 [ "Libro" => array:4 [ "titulo" => "Theorem proving" "fecha" => "2003" "editorial" => "John Wiley and Sons Ltd" "editorialLocalizacion" => "Chichester, UK" ] ] ] ] ] ] 1 => array:3 [ "identificador" => "bib0010" "etiqueta" => "[2]" "referencia" => array:1 [ 0 => array:2 [ "contribucion" => array:1 [ 0 => array:1 [ "autores" => array:1 [ 0 => array:2 [ "etal" => false "autores" => array:2 [ 0 => "C. Baier" 1 => "J. Katoen" ] ] ] ] ] "host" => array:1 [ 0 => array:1 [ "Libro" => array:4 [ "titulo" => "Principles of Model Checking" "fecha" => "2008" "editorial" => "MIT Press" "editorialLocalizacion" => "London, England: Cambridge, Mass" ] ] ] ] ] ] 2 => array:3 [ "identificador" => "bib0015" "etiqueta" => "[3]" "referencia" => array:1 [ 0 => array:2 [ "contribucion" => array:1 [ 0 => array:2 [ "titulo" => "Checking and Enforcing Safety: Runtime Verification and Runtime Reflection" "autores" => array:1 [ 0 => array:2 [ "etal" => false "autores" => array:1 [ 0 => "M. Leucker" ] ] ] ] ] "host" => array:1 [ 0 => array:1 [ "Revista" => array:5 [ "tituloSerie" => "ERCIM News" "fecha" => "2008" "volumen" => "75" "paginaInicial" => "35" "paginaFinal" => "36" ] ] ] ] ] ] 3 => array:3 [ "identificador" => "bib0020" "etiqueta" => "[4]" "referencia" => array:1 [ 0 => array:2 [ "contribucion" => array:1 [ 0 => array:2 [ "titulo" => "LaQuSo: Using Formal Methods for Analysis, Verification and Improvement of Safety-Critical Software" "autores" => array:1 [ 0 => array:2 [ "etal" => false "autores" => array:2 [ 0 => "S. Smetsers" 1 => "M. Eekelen" ] ] ] ] ] "host" => array:1 [ 0 => array:1 [ "Revista" => array:5 [ "tituloSerie" => "ERCIM News" "fecha" => "2008" "volumen" => "75" "paginaInicial" => "36" "paginaFinal" => "37" ] ] ] ] ] ] 4 => array:3 [ "identificador" => "bib0025" "etiqueta" => "[5]" "referencia" => array:1 [ 0 => array:2 [ "contribucion" => array:1 [ 0 => array:2 [ "titulo" => "A Design Choices for High-Confidence Distributed Real-Time Software" "autores" => array:1 [ 0 => array:2 [ "etal" => false "autores" => array:2 [ 0 => "S Fischmeister" 1 => "Azim" ] ] ] ] ] "host" => array:1 [ 0 => array:1 [ "Revista" => array:5 [ "tituloSerie" => "Leveraging Applications of Formal Methods, Verification, and Validation, Lecture Notes in Computer Science" "fecha" => "2010" "volumen" => "6416" "paginaInicial" => "97" "paginaFinal" => "111" ] ] ] ] ] ] 5 => array:3 [ "identificador" => "bib0030" "etiqueta" => "[6]" "referencia" => array:1 [ 0 => array:2 [ "contribucion" => array:1 [ 0 => array:2 [ "titulo" => "Trustable Formal Specification for Software Certification" "autores" => array:1 [ 0 => array:2 [ "etal" => false "autores" => array:2 [ 0 => "D Mery" 1 => "N.K Singh" ] ] ] ] ] "host" => array:1 [ 0 => array:1 [ "Revista" => array:5 [ "tituloSerie" => "Leveraging Applications of Formal Methods, Verification, and Validation, Lecture Notes in Computer Science" "fecha" => "2010" "volumen" => "6416" "paginaInicial" => "312" "paginaFinal" => "326" ] ] ] ] ] ] 6 => array:3 [ "identificador" => "bib0035" "etiqueta" => "[7]" "referencia" => array:1 [ 0 => array:2 [ "contribucion" => array:1 [ 0 => array:1 [ "autores" => array:1 [ 0 => array:2 [ "etal" => false "autores" => array:1 [ 0 => "I. Sommerville" ] ] ] ] ] "host" => array:1 [ 0 => array:1 [ "Libro" => array:5 [ "edicion" => "8th" "titulo" => "Software Engineering" "fecha" => "2007" "editorial" => "Pearson Education" "editorialLocalizacion" => "China" ] ] ] ] ] ] 7 => array:3 [ "identificador" => "bib0040" "etiqueta" => "[8]" "referencia" => array:1 [ 0 => array:1 [ "referenciaCompleta" => "S.M. Babamir and M. Borhani, “Formal Verification of Medical Monitoring Software Using Z Language: A Representative Sample,” Journal of Medical Systems, 2011, Springer, DOI: 10.1007/s10916-011-9739-5." ] ] ] 8 => array:3 [ "identificador" => "bib0045" "etiqueta" => "[9]" "referencia" => array:1 [ 0 => array:2 [ "contribucion" => array:1 [ 0 => array:2 [ "titulo" => "Practical Ways of Improving Product Safety in Industry" "autores" => array:1 [ 0 => array:2 [ "etal" => false "autores" => array:2 [ 0 => "S. Gabriele" 1 => "W. Werner" ] ] ] ] ] "host" => array:1 [ 0 => array:1 [ "Revista" => array:5 [ "tituloSerie" => "Improvements In system Safety" "fecha" => "2008" "numero" => "6" "paginaInicial" => "177" "paginaFinal" => "193" ] ] ] ] ] ] 9 => array:3 [ "identificador" => "bib0050" "etiqueta" => "[10]" "referencia" => array:1 [ 0 => array:2 [ "contribucion" => array:1 [ 0 => array:2 [ "titulo" => "Engineering Safety-and Security-Related Requirements: Tutorial,” in 15" "autores" => array:1 [ 0 => array:2 [ "etal" => false "autores" => array:1 [ 0 => "D.G. Firesmith" ] ] ] ] ] "host" => array:1 [ 0 => array:1 [ "LibroEditado" => array:3 [ "titulo" => "IEEE International Requirements Engineering Confencee" "conferencia" => "New Delhi, India" "serieFecha" => "2007" ] ] ] ] ] ] 10 => array:3 [ "identificador" => "bib0055" "etiqueta" => "[11]" "referencia" => array:1 [ 0 => array:2 [ "contribucion" => array:1 [ 0 => array:2 [ "titulo" => "Engineering Safety-Related Requirements for Software-Intensive Systems: Tutorial" "autores" => array:1 [ 0 => array:2 [ "etal" => false "autores" => array:1 [ 0 => "D.G. Firesmith" ] ] ] ] ] "host" => array:1 [ 0 => array:1 [ "Libro" => array:4 [ "titulo" => "27th International Conference on Software Engineering (ICSE'2005)" "fecha" => "2005" "editorial" => "Louis" "editorialLocalizacion" => "Missouri, USA" ] ] ] ] ] ] 11 => array:3 [ "identificador" => "bib0060" "etiqueta" => "[12]" "referencia" => array:1 [ 0 => array:2 [ "contribucion" => array:1 [ 0 => array:2 [ "titulo" => "Risk Assessment for M42 Active Traffic Management" "autores" => array:1 [ 0 => array:2 [ "etal" => false "autores" => array:2 [ 0 => "S. Tucker" 1 => "M. Halbert" ] ] ] ] ] "host" => array:1 [ 0 => array:1 [ "Revista" => array:5 [ "tituloSerie" => "Developments in Risk- Based Approaches to Safety" "fecha" => "2006" "numero" => "2" "paginaInicial" => "25" "paginaFinal" => "45" ] ] ] ] ] ] 12 => array:3 [ "identificador" => "bib0065" "etiqueta" => "[13]" "referencia" => array:1 [ 0 => array:2 [ "contribucion" => array:1 [ 0 => array:1 [ "autores" => array:1 [ 0 => array:2 [ "etal" => false "autores" => array:1 [ 0 => "C.A. Ericson" ] ] ] ] ] "host" => array:1 [ 0 => array:1 [ "Libro" => array:4 [ "titulo" => "Hazard analysis techniques for system safety" "fecha" => "2005" "editorial" => "Wiley-Interscience" "editorialLocalizacion" => "Hoboken, New Jersey, USA" ] ] ] ] ] ] 13 => array:3 [ "identificador" => "bib0070" "etiqueta" => "[14]" "referencia" => array:1 [ 0 => array:2 [ "contribucion" => array:1 [ 0 => array:2 [ "titulo" => "An Approach to Modeling Software Safety in Safety-Critical Systems" "autores" => array:1 [ 0 => array:2 [ "etal" => false "autores" => array:2 [ 0 => "M.B. Swarup" 1 => "P.S. Ramaiah" ] ] ] ] ] "host" => array:1 [ 0 => array:1 [ "Revista" => array:6 [ "tituloSerie" => "Journal of Computer Science" "fecha" => "2009" "volumen" => "5" "numero" => "4" "paginaInicial" => "311" "paginaFinal" => "322" ] ] ] ] ] ] 14 => array:3 [ "identificador" => "bib0075" "etiqueta" => "[15]" "referencia" => array:1 [ 0 => array:2 [ "contribucion" => array:1 [ 0 => array:1 [ "autores" => array:1 [ 0 => array:2 [ "etal" => false "autores" => array:1 [ 0 => "R. Patton" ] ] ] ] ] "host" => array:1 [ 0 => array:1 [ "Libro" => array:4 [ "titulo" => "Software Testing" "fecha" => "2001" "editorial" => "Sams" "editorialLocalizacion" => "Indianapolis, Indiana, USA" ] ] ] ] ] ] 15 => array:3 [ "identificador" => "bib0080" "etiqueta" => "[16]" "referencia" => array:1 [ 0 => array:2 [ "contribucion" => array:1 [ 0 => array:2 [ "titulo" => "A Comprative Study of Formal Methods for Safety Critical Software in Nuclear Power Plant" "autores" => array:1 [ 0 => array:2 [ "etal" => false "autores" => array:2 [ 0 => "S. Sohn" 1 => "P. Seong" ] ] ] ] ] "host" => array:1 [ 0 => array:1 [ "Revista" => array:6 [ "tituloSerie" => "Journal of the Korean Nuclear Society" "fecha" => "2000" "volumen" => "32" "numero" => "6" "paginaInicial" => "537" "paginaFinal" => "548" ] ] ] ] ] ] 16 => array:3 [ "identificador" => "bib0085" "etiqueta" => "[17]" "referencia" => array:1 [ 0 => array:2 [ "contribucion" => array:1 [ 0 => array:1 [ "autores" => array:1 [ 0 => array:2 [ "etal" => false "autores" => array:1 [ 0 => "J.M. Spivey" ] ] ] ] ] "host" => array:1 [ 0 => array:1 [ "Libro" => array:5 [ "edicion" => "2nd" "titulo" => "The Z Notation: A Reference Manual" "fecha" => "2001" "editorial" => "Prentice Hall" "editorialLocalizacion" => "Oxford, UK" ] ] ] ] ] ] 17 => array:3 [ "identificador" => "bib0090" "etiqueta" => "[18]" "referencia" => array:1 [ 0 => array:2 [ "contribucion" => array:1 [ 0 => array:1 [ "autores" => array:1 [ 0 => array:2 [ "colaboracion" => "National Aeronautics and Space Administration" "etal" => false ] ] ] ] "host" => array:1 [ 0 => array:1 [ "Libro" => array:4 [ "titulo" => "NASA Software Safety Guidebook" "fecha" => "2004" "editorial" => "NASA" "editorialLocalizacion" => "USA" ] ] ] ] ] ] 18 => array:3 [ "identificador" => "bib0095" "etiqueta" => "[19]" "referencia" => array:1 [ 0 => array:2 [ "contribucion" => array:1 [ 0 => array:1 [ "autores" => array:1 [ 0 => array:2 [ "etal" => false "autores" => array:3 [ 0 => "J.D. Gahl" 1 => "J.E. DijKstra" 2 => "C.A.R. Hoare" ] ] ] ] ] "host" => array:1 [ 0 => array:1 [ "Libro" => array:4 [ "titulo" => "Notes on Structured Programming" "fecha" => "1972" "editorial" => "Academic Press London" "editorialLocalizacion" => "London, England" ] ] ] ] ] ] 19 => array:3 [ "identificador" => "bib0100" "etiqueta" => "[20]" "referencia" => array:1 [ 0 => array:2 [ "contribucion" => array:1 [ 0 => array:1 [ "autores" => array:1 [ 0 => array:2 [ "colaboracion" => "Office of Government Commerce" "etal" => false ] ] ] ] "host" => array:1 [ 0 => array:1 [ "Libro" => array:4 [ "titulo" => "Intruduction to ITIL" "fecha" => "2006" "editorial" => "London, Britain" "editorialLocalizacion" => "TSO" ] ] ] ] ] ] ] ] ] ] ] "idiomaDefecto" => "en" "url" => "/16656423/0000001100000005/v2_201505081700/S1665642313715761/v2_201505081700/en/main.assets" "Apartado" => null "PDF" => "https://static.elsevier.es/multimedia/16656423/0000001100000005/v2_201505081700/S1665642313715761/v2_201505081700/en/main.pdf?idApp=UINPBA00004N&text.app=https://www.elsevier.es/" "EPUB" => "https://multimedia.elsevier.es/PublicationsMultimediaV1/item/epub/S1665642313715761?idApp=UINPBA00004N"]

Statistics

Towards the Design of Safety-Critical Software

R. Rafeh1, A. Rabiee1,2

1,2 Department of Computer Engineering Arak University Arak, Iran

2 Department of IT, Education Organization Arak, Iran

Read

3402

Times
was read the article

754

Total PDF

2648

Total HTML

Share statistics

 array:23 [
  "pii" => "S1665642313715761"
  "issn" => "16656423"
  "doi" => "10.1016/S1665-6423(13)71576-1"
  "estado" => "S300"
  "fechaPublicacion" => "2013-10-01"
  "aid" => "71576"
  "copyright" => "Universidad Nacional Aut&#243;noma de M&#233;xico"
  "copyrightAnyo" => "2013"
  "documento" => "article"
  "licencia" => "http://creativecommons.org/licenses/by-nc-nd/4.0/"
  "subdocumento" => "fla"
  "cita" => "Journal of Applied Research and Technology. 2013;11:683-94"
  "abierto" => array:3 [
    "ES" => true
    "ES2" => true
    "LATM" => true
  ]
  "gratuito" => true
  "lecturas" => array:2 [
    "total" => 947
    "formatos" => array:3 [
      "EPUB" => 29
      "HTML" => 608
      "PDF" => 310
    ]
  ]
  "itemSiguiente" => array:18 [
    "pii" => "S1665642313715773"
    "issn" => "16656423"
    "doi" => "10.1016/S1665-6423(13)71577-3"
    "estado" => "S300"
    "fechaPublicacion" => "2013-10-01"
    "aid" => "71577"
    "copyright" => "Universidad Nacional Aut&#243;noma de M&#233;xico"
    "documento" => "article"
    "licencia" => "http://creativecommons.org/licenses/by-nc-nd/4.0/"
    "subdocumento" => "fla"
    "cita" => "Journal of Applied Research and Technology. 2013;11:695-701"
    "abierto" => array:3 [
      "ES" => true
      "ES2" => true
      "LATM" => true
    ]
    "gratuito" => true
    "lecturas" => array:2 [
      "total" => 1267
      "formatos" => array:3 [
        "EPUB" => 35
        "HTML" => 831
        "PDF" => 401
      ]
    ]
    "en" => array:11 [
      "idiomaDefecto" => true
      "titulo" => "Fiber Optic Pressure Sensor of 0&#8211;0&#46;36 psi by Multimode Interference Technique"
      "tienePdf" => "en"
      "tieneTextoCompleto" => "en"
      "tieneResumen" => array:2 [
        0 => "en"
        1 => "es"
      ]
      "paginas" => array:1 [
        0 => array:2 [
          "paginaInicial" => "695"
          "paginaFinal" => "701"
        ]
      ]
      "contieneResumen" => array:2 [
        "en" => true
        "es" => true
      ]
      "contieneTextoCompleto" => array:1 [
        "en" => true
      ]
      "contienePdf" => array:1 [
        "en" => true
      ]
      "resumenGrafico" => array:2 [
        "original" => 0
        "multimedia" => array:7 [
          "identificador" => "fig0025"
          "etiqueta" => "Figure 5"
          "tipo" => "MULTIMEDIAFIGURA"
          "mostrarFloat" => true
          "mostrarDisplay" => false
          "figura" => array:1 [
            0 => array:4 [
              "imagen" => "gr5.jpeg"
              "Alto" => 579
              "Ancho" => 616
              "Tamanyo" => 53011
            ]
          ]
          "descripcion" => array:1 [
            "en" => "<p id="spar0025" class="elsevierStyleSimplePara elsevierViewall">Sensor body&#46;</p>"
          ]
        ]
      ]
      "autores" => array:1 [
        0 => array:2 [
          "autoresLista" => "A&#46;R&#46; Mejia-Aranda, M&#46;A&#46; Basurto-Pensado, E&#46;E&#46; Antunez-Ceron, L&#46;L&#46; Castro-G&#243;mez, G&#46; Urquiza-Beltran, J&#46;A&#46; Rodriguez, J&#46;C&#46; Garc&#237;a, J&#46;J&#46; S&#225;nchez-Mondrag&#243;n, V&#46;I&#46; Ruiz-P&#233;rez"
          "autores" => array:9 [
            0 => array:2 [
              "nombre" => "A&#46;R&#46;"
              "apellidos" => "Mejia-Aranda"
            ]
            1 => array:2 [
              "nombre" => "M&#46;A&#46;"
              "apellidos" => "Basurto-Pensado"
            ]
            2 => array:2 [
              "nombre" => "E&#46;E&#46;"
              "apellidos" => "Antunez-Ceron"
            ]
            3 => array:2 [
              "nombre" => "L&#46;L&#46;"
              "apellidos" => "Castro-G&#243;mez"
            ]
            4 => array:2 [
              "nombre" => "G&#46;"
              "apellidos" => "Urquiza-Beltran"
            ]
            5 => array:2 [
              "nombre" => "J&#46;A&#46;"
              "apellidos" => "Rodriguez"
            ]
            6 => array:2 [
              "nombre" => "J&#46;C&#46;"
              "apellidos" => "Garc&#237;a"
            ]
            7 => array:2 [
              "nombre" => "J&#46;J&#46;"
              "apellidos" => "S&#225;nchez-Mondrag&#243;n"
            ]
            8 => array:2 [
              "nombre" => "V&#46;I&#46;"
              "apellidos" => "Ruiz-P&#233;rez"
            ]
          ]
        ]
      ]
    ]
    "idiomaDefecto" => "en"
    "EPUB" => "https://multimedia.elsevier.es/PublicationsMultimediaV1/item/epub/S1665642313715773?idApp=UINPBA00004N"
    "url" => "/16656423/0000001100000005/v2_201505081700/S1665642313715773/v2_201505081700/en/main.assets"
  ]
  "itemAnterior" => array:18 [
    "pii" => "S166564231371575X"
    "issn" => "16656423"
    "doi" => "10.1016/S1665-6423(13)71575-X"
    "estado" => "S300"
    "fechaPublicacion" => "2013-10-01"
    "aid" => "71575"
    "copyright" => "Universidad Nacional Aut&#243;noma de M&#233;xico"
    "documento" => "article"
    "licencia" => "http://creativecommons.org/licenses/by-nc-nd/4.0/"
    "subdocumento" => "fla"
    "cita" => "Journal of Applied Research and Technology. 2013;11:674-82"
    "abierto" => array:3 [
      "ES" => true
      "ES2" => true
      "LATM" => true
    ]
    "gratuito" => true
    "lecturas" => array:2 [
      "total" => 3304
      "formatos" => array:3 [
        "EPUB" => 44
        "HTML" => 2575
        "PDF" => 685
      ]
    ]
    "en" => array:11 [
      "idiomaDefecto" => true
      "titulo" => "Temperature and Thermal Stresses of Vehicles Gray Cast Brake"
      "tienePdf" => "en"
      "tieneTextoCompleto" => "en"
      "tieneResumen" => "en"
      "paginas" => array:1 [
        0 => array:2 [
          "paginaInicial" => "674"
          "paginaFinal" => "682"
        ]
      ]
      "contieneResumen" => array:1 [
        "en" => true
      ]
      "contieneTextoCompleto" => array:1 [
        "en" => true
      ]
      "contienePdf" => array:1 [
        "en" => true
      ]
      "resumenGrafico" => array:2 [
        "original" => 0
        "multimedia" => array:7 [
          "identificador" => "fig0005"
          "etiqueta" => "Figure 1"
          "tipo" => "MULTIMEDIAFIGURA"
          "mostrarFloat" => true
          "mostrarDisplay" => false
          "figura" => array:1 [
            0 => array:4 [
              "imagen" => "gr1.jpeg"
              "Alto" => 493
              "Ancho" => 806
              "Tamanyo" => 72953
            ]
          ]
          "descripcion" => array:1 [
            "en" => "<p id="spar0005" class="elsevierStyleSimplePara elsevierViewall">Disc-pads assembly with forces applied to the disc&#46;</p>"
          ]
        ]
      ]
      "autores" => array:1 [
        0 => array:2 [
          "autoresLista" => "A&#46; Belhocine, M&#46; Bouchetara"
          "autores" => array:2 [
            0 => array:2 [
              "nombre" => "A&#46;"
              "apellidos" => "Belhocine"
            ]
            1 => array:2 [
              "nombre" => "M&#46;"
              "apellidos" => "Bouchetara"
            ]
          ]
        ]
      ]
    ]
    "idiomaDefecto" => "en"
    "EPUB" => "https://multimedia.elsevier.es/PublicationsMultimediaV1/item/epub/S166564231371575X?idApp=UINPBA00004N"
    "url" => "/16656423/0000001100000005/v2_201505081700/S166564231371575X/v2_201505081700/en/main.assets"
  ]
  "en" => array:14 [
    "idiomaDefecto" => true
    "titulo" => "Towards the Design of Safety-Critical Software"
    "tieneTextoCompleto" => true
    "paginas" => array:1 [
      0 => array:2 [
        "paginaInicial" => "683"
        "paginaFinal" => "694"
      ]
    ]
    "autores" => array:1 [
      0 => array:3 [
        "autoresLista" => "R&#46; Rafeh, A&#46; Rabiee"
        "autores" => array:2 [
          0 => array:4 [
            "nombre" => "R&#46;"
            "apellidos" => "Rafeh"
            "email" => array:1 [
              0 => "r-rafeh&#64;araku&#46;ac&#46;ir"
            ]
            "referencia" => array:1 [
              0 => array:2 [
                "etiqueta" => "<span class="elsevierStyleSup">1</span>"
                "identificador" => "aff0010"
              ]
            ]
          ]
          1 => array:4 [
            "nombre" => "A&#46;"
            "apellidos" => "Rabiee"
            "email" => array:1 [
              0 => "arvand&#46;rabiee&#64;gmail&#46;com"
            ]
            "referencia" => array:1 [
              0 => array:2 [
                "etiqueta" => "<span class="elsevierStyleSup">1&#44;2</span>"
                "identificador" => "aff0005"
              ]
            ]
          ]
        ]
        "afiliaciones" => array:2 [
          0 => array:3 [
            "entidad" => "Department of Computer Engineering Arak University Arak&#44; Iran"
            "etiqueta" => "1&#44;2"
            "identificador" => "aff0005"
          ]
          1 => array:3 [
            "entidad" => "Department of IT&#44; Education Organization Arak&#44; Iran"
            "etiqueta" => "2"
            "identificador" => "aff0010"
          ]
        ]
      ]
    ]
    "textoCompleto" => "<span class="elsevierStyleSections"><span id="sec0005" class="elsevierStyleSection elsevierViewall"><span class="elsevierStyleLabel">1</span><span class="elsevierStyleSectionTitle" id="sect0015">Introduction</span><p id="par0005" class="elsevierStylePara elsevierViewall">Computers play a significant role in operating many modern systems some of which are classified as safety-critical&#46; Any failure in safety-critical systems may result in loss of life or significant damage to the environment&#46; Examples include medical systems&#44; aircraft flight control systems&#44; weapons and nuclear systems&#46; When designing such systems&#44; which usually include both software and hardware&#44; the most important factor is safety&#46; In this paper&#44; we focus on the design of safety-critical software&#46;</p><p id="par0010" class="elsevierStylePara elsevierViewall">The main approaches to improve the safety are divided into three classes&#58; Theorem proving <a class="elsevierStyleCrossRef" href="#bib0005">&#91;1&#93;</a>&#44; model checking <a class="elsevierStyleCrossRef" href="#bib0010">&#91;2&#93;</a> and runtime verification <a class="elsevierStyleCrossRef" href="#bib0015">&#91;3&#93;</a>&#46; Current safety paradigms usually use one of the aforementioned approaches or a combination of them&#46; For example&#44; runtime reflection <a class="elsevierStyleCrossRef" href="#bib0015">&#91;3&#93;</a> employs runtime verification and the approach proposed in <a class="elsevierStyleCrossRef" href="#bib0020">&#91;4&#93;</a> uses a combination of theorem proving and model checking&#46; Safety approaches like timed automata <a class="elsevierStyleCrossRef" href="#bib0025">&#91;5&#93;</a> and Event-B <a class="elsevierStyleCrossRef" href="#bib0030">&#91;6&#93;</a> usually use formal methods to specify the system requirements or monitor the system behavior&#46; Formal languages such as Z <a class="elsevierStyleCrossRef" href="#bib0035">&#91;7&#93;</a>&#44; is usually used to specify the system&#46; For example&#44; the approach proposed in <a class="elsevierStyleCrossRef" href="#bib0040">&#91;8&#93;</a> uses a combination of Petri-net and the Z language to verify medical software&#46;</p><p id="par0015" class="elsevierStylePara elsevierViewall">However&#44; the main issue with current approaches is that they are not taking into consideration all safety angles&#46; We believe safety must be observed in all software production phases&#46; Therefore&#44; we propose a formal approach which takes into account all software production phases including planning&#44; requirements specification&#44; designing&#44; and implementation <a class="elsevierStyleCrossRef" href="#bib0045">&#91;9&#93;</a>&#46; We explain the proposed approach step by step using continuous infusion insulin pump &#40;CIIP&#41; which is a familiar safety-critical system&#46;</p><p id="par0020" class="elsevierStylePara elsevierViewall">The paper is organized as follows&#58; In <a class="elsevierStyleCrossRef" href="#sec0010">Section 2</a>&#44; we explain briefly CIIP&#46; In <a class="elsevierStyleCrossRef" href="#sec0015">Section 3</a>&#44; we explain the steps that must be taken for achieving safety in CIIP based on the proposed approach&#46; Finally&#44; <a class="elsevierStyleCrossRef" href="#sec0020">Section 4</a> concludes the paper&#46;</p></span><span id="sec0010" class="elsevierStyleSection elsevierViewall"><span class="elsevierStyleLabel">2</span><span class="elsevierStyleSectionTitle" id="sect0020">Continuous infusion insulin pump</span><p id="par0025" class="elsevierStylePara elsevierViewall">Diabetes is a disease originated when the human body cannot produce enough insulin hormones&#46; Insulin metabolizes the available sugar in the blood&#46; The known therapy for diabetes consists in injecting enough insulin to the patient&#39;s blood&#46; High blood sugar levels may hurt kidney&#44; heart and eyes&#46; Low blood sugar levels may paralyze brain and cause diabetic death&#46; CIIP is a modern medical system for<a name="p684"></a> controlling the blood sugar levels by injecting the adequate doses of insulin to the patient&#39;s blood&#46; This system takes blood samples every 10 minutes and checks its sugar level&#46; Then the amount of necessary insulin is computed for injection in the blood <a class="elsevierStyleCrossRef" href="#bib0035">&#91;7&#93;</a>&#46;</p></span><span id="sec0015" class="elsevierStyleSection elsevierViewall"><span class="elsevierStyleLabel">3</span><span class="elsevierStyleSectionTitle" id="sect0025">The proposed approach</span><p id="par0030" class="elsevierStylePara elsevierViewall">In this section&#44; we explain our approach in detail and use CIIP as an example&#46; Our proposed approach consists of three steps as follows&#58;</p><p id="par0035" class="elsevierStylePara elsevierViewall"><span class="elsevierStyleBold">Step one</span>&#58; In the first Step&#44; we specify all safety requirements&#46; For safety requirements we need to investigate the system in detail which includes the goals of the system&#44; environments&#44; users&#44; operators&#44; and preliminary resources&#46; These goals are shown in <a class="elsevierStyleCrossRef" href="#tbl0005">Table 1</a> for CIIP&#46;</p><elsevierMultimedia ident="tbl0005"></elsevierMultimedia><p id="par0040" class="elsevierStylePara elsevierViewall">Some of the equipment needed in CIIP are sampling and injecting equipment&#44; insulin resource&#44; processor&#44; LCD&#44; and warning systems&#46; A high level description of CIIP behavior is as follows&#58; The system takes a sample of patient blood every 10 minutes&#44; computes suitable insulin dose&#44; and injects insulin to the patient&#39;s blood&#46; High level safety approach for CIIP is depicted in <a class="elsevierStyleCrossRef" href="#tbl0010">Table 2</a>&#46;</p><elsevierMultimedia ident="tbl0010"></elsevierMultimedia><p id="par0045" class="elsevierStylePara elsevierViewall">For CIIP&#44; the system requirements consist of realtime operating systems&#44; some modeling tools&#44; realtime programming languages and PCs&#46; Hardware requirements consist of processors&#44; memories&#44; insulin reservoirs&#44; sugar sampling equipment&#44; insulin injection equipment&#44; LCDs and power supplies&#46; Functional requirements of CIIP are as follows&#58;<ul class="elsevierStyleList" id="lis0005"><li class="elsevierStyleListItem" id="lsti0005"><span class="elsevierStyleLabel">1&#46;</span><p id="par0050" class="elsevierStylePara elsevierViewall">The system receives a sample of sugar blood every 10 minutes&#46;</p></li><li class="elsevierStyleListItem" id="lsti0010"><span class="elsevierStyleLabel">2&#46;</span><p id="par0055" class="elsevierStylePara elsevierViewall">The system processes sugar blood and computes the sugar level&#46;</p></li><li class="elsevierStyleListItem" id="lsti0015"><span class="elsevierStyleLabel">3&#46;</span><p id="par0060" class="elsevierStylePara elsevierViewall">The system computes insulin dose according to the last three sugar samples and injects insulin to the patient&#39;s blood&#46;</p></li></ul></p><p id="par0065" class="elsevierStylePara elsevierViewall">Nonfunctional requirements are usually data requirements extracted from medical documents&#46; These requirements are the following&#58;<ul class="elsevierStyleList" id="lis0010"><li class="elsevierStyleListItem" id="lsti0020"><span class="elsevierStyleLabel">1&#46;</span><p id="par0070" class="elsevierStylePara elsevierViewall">If the sugar level is smaller than the minimum value&#44; the insulin dose is 0&#46;</p></li><li class="elsevierStyleListItem" id="lsti0025"><span class="elsevierStyleLabel">2&#46;</span><p id="par0075" class="elsevierStylePara elsevierViewall">If the sugar level is between the minimum and the maximum value&#44; then&#58;<ul class="elsevierStyleList" id="lis0015"><li class="elsevierStyleListItem" id="lsti0030"><span class="elsevierStyleLabel">&#8226;</span><p id="par0080" class="elsevierStylePara elsevierViewall">If the third sugar sample is smaller or equal to the second sample&#44; insulin dose is 0&#46;</p></li><li class="elsevierStyleListItem" id="lsti0035"><span class="elsevierStyleLabel">&#8226;</span><p id="par0085" class="elsevierStylePara elsevierViewall">If the third sugar sample is greater than the second sample and the second sample is greater than the first one&#44; and the difference between the third sample and the second one is smaller or equal than the difference between the second sample and the first one&#44; insulin dose is 0&#46;</p></li><li class="elsevierStyleListItem" id="lsti0040"><span class="elsevierStyleLabel">&#8226;</span><p id="par0090" class="elsevierStylePara elsevierViewall">If the third sugar sample is greater than the second sample and the second sample is greater than the first one&#44; and the difference between the third sample and the second one is smaller or equal than the difference between the second sample and the first one and the difference between the third and the second sample is smaller than 4&#44; the insulin dose is the minimum value&#46;</p></li><li class="elsevierStyleListItem" id="lsti0045"><span class="elsevierStyleLabel">&#8226;</span><p id="par0095" class="elsevierStylePara elsevierViewall">If the third sugar sample is greater than the second sample and the second sample is greater than the first one&#44; and the difference between the third sample and the second one is smaller or equal than the difference between the second sample and the first one and the difference between the third and the second sample is greater than 4&#44; the insulin dose is the quotient of the <span class="elsevierStyleItalic">difference between the third and the second sample by 4</span>&#46;<a name="p685"></a></p></li></ul></p></li><li class="elsevierStyleListItem" id="lsti0050"><span class="elsevierStyleLabel">3&#46;</span><p id="par0100" class="elsevierStylePara elsevierViewall">If the sugar level is greater than the maximum value&#44; then&#58;<ul class="elsevierStyleList" id="lis0020"><li class="elsevierStyleListItem" id="lsti0055"><span class="elsevierStyleLabel">&#8226;</span><p id="par0105" class="elsevierStylePara elsevierViewall">If the third sugar sample is greater than the second sample and their difference is smaller than 4&#44; the insulin dose is 0&#46;</p></li><li class="elsevierStyleListItem" id="lsti0060"><span class="elsevierStyleLabel">&#8226;</span><p id="par0110" class="elsevierStylePara elsevierViewall">If the third sugar sample is equal to the second sample&#44; the insulin dose is 0&#46;</p></li><li class="elsevierStyleListItem" id="lsti0065"><span class="elsevierStyleLabel">&#8226;</span><p id="par0115" class="elsevierStylePara elsevierViewall">If the third sugar sample is smaller than the second sample and the difference between the third sample and the second one is smaller or equal than the difference between the second sample and the first one&#44; the insulin dose is 0&#46;</p></li><li class="elsevierStyleListItem" id="lsti0070"><span class="elsevierStyleLabel">&#8226;</span><p id="par0120" class="elsevierStylePara elsevierViewall">If the third sugar sample is smaller than the second sample and the difference between the third sample and the second one is greater than the difference between the second sample and the first one&#44; the insulin dose is the minimum value&#46;</p></li></ul></p></li></ul></p><p id="par0125" class="elsevierStylePara elsevierViewall">After specifying functional and nonfunctional requirements&#44; we need to specify system hazards&#46; Most of the hazard standards propose four hazard severity classes&#59; catastrophic&#44; critical&#44; marginal&#44; and negligible <a class="elsevierStyleCrossRef" href="#bib0060">&#91;12&#93;</a>&#46; High level hazards for CIIP are shown in <a class="elsevierStyleCrossRef" href="#tbl0015">Table 3</a> according to this classification&#46; The risk of each hazard can be determined using a combination of a digit and a letter which is shown in <a class="elsevierStyleCrossRef" href="#tbl0020">Table 4</a><a class="elsevierStyleCrossRef" href="#bib0065">&#91;13&#93;</a>&#46;</p><elsevierMultimedia ident="tbl0015"></elsevierMultimedia><elsevierMultimedia ident="tbl0020"></elsevierMultimedia><p id="par0130" class="elsevierStylePara elsevierViewall">FMEA is a technique used in combination of hazard analysis in the proposed approach&#46; There are three FMEA classes&#58; Structural FMEA used for hardware analysis&#44; functional FMEA used for system functions analysis and Combined FMEA <a class="elsevierStyleCrossRef" href="#bib0065">&#91;13&#93;</a>&#46; Structural FMEA worksheet and functional FMEA worksheet for CIIP are shown in Table 5 and Table 6&#44; respectively&#46; These tables are updated in the next phases of this step&#46;</p><p id="par0135" class="elsevierStylePara elsevierViewall">Safety requirements may be defined in terms of constraints&#44; chains of events&#44; time constraints&#44; fault tolerance equipment and warning interfaces&#46; Safety requirements are classified as pure safety requirements&#44; significant safety requirements&#44; system safety requirements&#44; and safety constraints <a class="elsevierStyleCrossRef" href="#bib0055">&#91;11&#93;</a>&#46; This classification for CIIP is explained in detail in the following section&#46; Each requirement must be mapped to at least one row of FMEA worksheets&#46;</p><p id="par0140" class="elsevierStylePara elsevierViewall">Pure safety requirements&#58;<ul class="elsevierStyleList" id="lis0025"><li class="elsevierStyleListItem" id="lsti0075"><span class="elsevierStyleLabel">&#8226;</span><p id="par0145" class="elsevierStylePara elsevierViewall">System has not to have a risk in 1A rate</p></li></ul></p><p id="par0585" class="elsevierStylePara elsevierViewall">Safety significant requirements&#58;<ul class="elsevierStyleList" id="lis0030"><li class="elsevierStyleListItem" id="lsti0080"><span class="elsevierStyleLabel">&#8226;</span><p id="par0150" class="elsevierStylePara elsevierViewall">If power is lower than the min level&#44; a low power message has to be shown to the user and sampling operation must be suspended until power recharging takes place &#40;rows 1&#44; 2 from structural FMEA&#41;&#46;</p></li><li class="elsevierStyleListItem" id="lsti0085"><span class="elsevierStyleLabel">&#8226;</span><p id="par0155" class="elsevierStylePara elsevierViewall">Sampling equipment has to be tested automatically&#46; Sampling operation must be stopped if this equipment does not work perfectly &#40;row 3 from structural FMEA&#41;&#46;</p></li><li class="elsevierStyleListItem" id="lsti0090"><span class="elsevierStyleLabel">&#8226;</span><p id="par0160" class="elsevierStylePara elsevierViewall">Injecting equipment has to be tested automatically&#46; Injecting operation must be stopped if this equipment does not work perfectly &#40;row 6 from structural FMEA&#41;&#46;<a name="p686"></a></p></li><li class="elsevierStyleListItem" id="lsti0095"><span class="elsevierStyleLabel">&#8226;</span><p id="par0165" class="elsevierStylePara elsevierViewall">If the amount of insulin in the reservoir is smaller than the min insulin dose or specified injection dose&#44; a low insulin message has to be shown to the user and injecting operation must be stopped &#40;row 7 from structural FMEA&#41;&#46;</p></li><li class="elsevierStyleListItem" id="lsti0100"><span class="elsevierStyleLabel">&#8226;</span><p id="par0170" class="elsevierStylePara elsevierViewall">The amount of cumulative dose at the end of every 24 hours can be at most 25 doses &#40;row 4 from structural FMEA&#44; medical rules&#41;</p></li></ul></p><p id="par0175" class="elsevierStylePara elsevierViewall">Safety system requirements&#58;<ul class="elsevierStyleList" id="lis0035"><li class="elsevierStyleListItem" id="lsti0105"><span class="elsevierStyleLabel">&#8226;</span><p id="par0180" class="elsevierStylePara elsevierViewall">An electricity-current evaluator system equipped with current sensor&#44; backup battery&#44; and LCD &#40;rows 1&#44; 2 from structural FMEA&#41;&#46;</p></li><li class="elsevierStyleListItem" id="lsti0110"><span class="elsevierStyleLabel">&#8226;</span><p id="par0185" class="elsevierStylePara elsevierViewall">Insulin-level determinant system for insulin reservoir &#40;row 7 from structural FMEA&#41;</p></li><li class="elsevierStyleListItem" id="lsti0115"><span class="elsevierStyleLabel">&#8226;</span><p id="par0190" class="elsevierStylePara elsevierViewall">Warning equipment &#40;rows 1&#44; 2 from structural FMEA and rows 1&#44; 2 from functional FMEA&#41;</p></li></ul><elsevierMultimedia ident="tbl0045"></elsevierMultimedia><a name="p687"></a></p><p id="par0195" class="elsevierStylePara elsevierViewall">Safety constraints obtained from recommended reaction in FMEA worksheet with runtime management tag are as follows&#58;<ul class="elsevierStyleList" id="lis0040"><li class="elsevierStyleListItem" id="lsti0120"><span class="elsevierStyleLabel">&#8226;</span><p id="par0200" class="elsevierStylePara elsevierViewall">A sampling operation must be finished at most 10 seconds after sampling starts otherwise&#44; a sampling failure message must be shown to the user and the system has to be turned off &#40;row 1 from functional FMEA&#41;&#46;</p></li><li class="elsevierStyleListItem" id="lsti0125"><span class="elsevierStyleLabel">&#8226;</span><p id="par0205" class="elsevierStylePara elsevierViewall">An insulin injection is an atomic operation &#40;row 2 from functional FMEA&#41;&#46;</p></li><li class="elsevierStyleListItem" id="lsti0130"><span class="elsevierStyleLabel">&#8226;</span><p id="par0210" class="elsevierStylePara elsevierViewall">If the sugar level is low&#44; the system must avoid injecting insulin to the patient&#39;s blood &#40;row 4 from functional FMEA&#41;&#46;</p></li><li class="elsevierStyleListItem" id="lsti0135"><span class="elsevierStyleLabel">&#8226;</span><p id="par0215" class="elsevierStylePara elsevierViewall">Insulin dose for injection must not exceed the max dose &#40;row 4 from functional FMEA&#41;&#46;</p></li><li class="elsevierStyleListItem" id="lsti0140"><span class="elsevierStyleLabel">&#8226;</span><p id="par0220" class="elsevierStylePara elsevierViewall">Injecting operation must be finished at most 30 seconds after sampling starts otherwise&#44; an injection failure message must be shown to the user and system has to be turned off &#40;row 2 from functional FMEA&#41;&#46;</p></li></ul></p><p id="par0225" class="elsevierStylePara elsevierViewall"><span class="elsevierStyleBold">Step two&#58;</span> After identifying safety requirements&#44; we model the system such that it satisfies all safety requirements <a class="elsevierStyleCrossRef" href="#bib0070">&#91;14&#93;</a>&#46; We proposed two system units&#58; operation unit that interacts with the environment &#40;the patient&#41; directly&#44; and control unit that controls and supports the operation unit&#46; Figure 1 shows this interactive model&#46;</p><p id="par0230" class="elsevierStylePara elsevierViewall">We use timed transition Petri-net as the formal method because of its tractable behavior and its support of time&#46; In addition&#44; we use Z <a class="elsevierStyleCrossRef" href="#bib0085">&#91;17&#93;</a> to specify textual and mathematical specifications as a complement for Petri-net&#46; A Petri-net model includes places&#44; tokens&#44; arcs and transitions&#46; Each transition associates with a condition which&#44; when holds&#44; causes tokens on the transition to move to the next place&#46; A Petri-net model for logical behavior of CIIP is shown in Figure 2&#46;</p><p id="par0235" class="elsevierStylePara elsevierViewall">All transitions in Figure 2 are explained in <a class="elsevierStyleCrossRef" href="#tbl0025">Table 7</a> similar to the proposed model in <a class="elsevierStyleCrossRef" href="#bib0040">&#91;8&#93;</a>&#46;<elsevierMultimedia ident="tbl0050"></elsevierMultimedia><a name="p688"></a><elsevierMultimedia ident="fig0005"></elsevierMultimedia></p><elsevierMultimedia ident="tbl0025"></elsevierMultimedia><p id="par0240" class="elsevierStylePara elsevierViewall">As shown in Figure 2&#44; the operation unit has four main states&#59; <span class="elsevierStyleItalic">Idle&#44; Sampling&#44; Computing&#44;</span> and <span class="elsevierStyleItalic">Injecting</span>&#46; A token moves from <span class="elsevierStyleItalic">Idle</span> state to <span class="elsevierStyleItalic">Injecting</span> state when transitions are fired according to the conditions in <a class="elsevierStyleCrossRef" href="#tbl0025">Table 7</a>&#46; Diagrams are not convenient tools to specify the requirements&#59; instead&#44; we use Z as a textual formal method to do so&#46; Schemas 1 to 6 specify CIIP requirements similar to <a class="elsevierStyleCrossRef" href="#bib0040">&#91;8&#93;</a>&#46; Each schema has a declaration part and a predicate part&#46; For example schema 1 specifies states and their initial values&#46; In this schema&#44; <span class="elsevierStyleItalic">insulinAvailable</span> shows the available insulin in the reservoir&#46; Also this schema has a predicate <span class="elsevierStyleItalic">minimumDose</span> that specifies the amount of minimum insulin for injection&#46;</p><p id="par0245" class="elsevierStylePara elsevierViewall">the sugar level is high and low&#44; respectively&#46; Last three schemas specify computing state in the Petri-net model&#46; Because the lack of space&#44; we Schema 2 specifies the behavior of the system when running&#46; Schema 3&#44; specifies data requirements when the sugar level is normal&#46; Schemas 4 and 5 specify data requirements when the sugar level is high and low&#44; respectively&#46; Last three schemas specify computing state in the Petri-net model&#46; Because the lack of space&#44; we ignore schemas for other states including sampling and injecting&#46;<a name="p689"></a><a name="p690"></a><elsevierMultimedia ident="tbl0055"></elsevierMultimedia><elsevierMultimedia ident="tb0005"></elsevierMultimedia><elsevierMultimedia ident="tb0010"></elsevierMultimedia><elsevierMultimedia ident="tb0015"></elsevierMultimedia><elsevierMultimedia ident="tb0020"></elsevierMultimedia><a name="p693"></a></p><p id="par0555" class="elsevierStylePara elsevierViewall"><span class="elsevierStyleBold">Step three&#58;</span> Even using the most sophisticated techniques for controlling the safety in both&#44; requirements layer and design layer&#44; it is always possible an unexpected error causes a system failure at runtime&#46; Therefore&#44; to avoid any system failure&#44; we need to monitor the behavior of the system at runtime to identify and manage unexpected faults&#46; In the proposed approach&#44; all the main states of the system are monitored continuously in a structure which includes four units&#58; Log management&#44; change management&#44; prevention management and disaster management which are based on information technology infrastructure library &#40;ITIL&#41; 20&#46;</p><p id="par0560" class="elsevierStylePara elsevierViewall">Log management logs the main sates of the system when they change&#46; As a result&#44; all required states must be identified first&#46; The main candidates for logging are those which changes may result in a critical behavior&#46; Main critical behavior of CIIP is insulin injection&#59; because incorrect insulin injection may hurt the patient seriously&#46; Critical states that are in our concern shown in <a class="elsevierStyleCrossRef" href="#tbl0030">Table 8</a>&#46; These states must be logged&#46;</p><elsevierMultimedia ident="tbl0030"></elsevierMultimedia><p id="par0565" class="elsevierStylePara elsevierViewall">Because critical behavior of the system may change over time&#44; we need a change management unit to confirm that the change is safe&#46; This unit is constructed from the high level constraints of the system and the environment conditions&#46; Before giving permission to any critical behavior&#44; required states are obtained from log management to ensure that all of them are safe&#46; Change management unit plays a role in design&#44; similar to the role of exception management in programming&#46; <a class="elsevierStyleCrossRef" href="#tbl0035">Table 9</a> shows change permissions for the <span class="elsevierStyleItalic">beginning of injecting</span> critical behavior of CIIP&#46; We can extend this table for other critical behaviors of CIIP which are in the second level of importance&#46;</p><elsevierMultimedia ident="tbl0035"></elsevierMultimedia><p id="par0570" class="elsevierStylePara elsevierViewall">To detect existing faults of the system before entering to critical states at runtime&#44; a prevention management is required&#46; Because CIIP is a real-time system&#44; it is better to design prevention management such that it runs in parallel with the system&#46; Schema 7 specifies prevention management in Z language for CIIP&#46; When any condition in this schema fails&#44; disaster management is called&#46;</p><p id="par0575" class="elsevierStylePara elsevierViewall">Disaster management unit is a complement for the prevention unit&#46; It tries to escape from faulty situations of the system&#44; those which cannot be predicted in normal behavior and may lead to a catastrophic status&#46; Disaster management can be as simple as showing a warning to the user&#44; or as complex as replacing a redundant hardware&#44; or as urgent as turning off the whole system&#46; Disaster management for CIIP can be designed to turn off the system&#44; show a message about system failure&#44; and send a message to the patient&#39;s doctor through communication lines&#46; <a class="elsevierStyleCrossRef" href="#tbl0040">Schema 8</a> specifies disaster management for CIIP in Z language&#46;<a name="p694"></a></p><span id="sec9005" class="elsevierStyleSection elsevierViewall"><span class="elsevierStyleSectionTitle" id="sect9015">Emergency</span><p id="par9575" class="elsevierStylePara elsevierViewall"></p><elsevierMultimedia ident="tbl0040"></elsevierMultimedia></span></span><span id="sec0020" class="elsevierStyleSection elsevierViewall"><span class="elsevierStyleLabel">4</span><span class="elsevierStyleSectionTitle" id="sect0030">Conclusions</span><p id="par0580" class="elsevierStylePara elsevierViewall">Achieving a high degree of safety in safety-critical software requires that designers think about it carefully in each step of the software production&#46; However&#44; current approaches usually focus on safety in only one phase of the software production&#46; In this paper&#44; we proposed a multi-phase approach to achieve safety in safety-critical software&#46; To describe the behavior of the system formally&#44; we used timed transition Petri-net and the Z language&#46; To show the proposed approach practically&#44; we used CIIP as a sample model&#46;</p></span></span>"
    "textoCompletoSecciones" => array:1 [
      "secciones" => array:7 [
        0 => array:3 [
          "identificador" => "xres498891"
          "titulo" => "Abstract"
          "secciones" => array:1 [
            0 => array:1 [
              "identificador" => "abst0005"
            ]
          ]
        ]
        1 => array:2 [
          "identificador" => "xpalclavsec520380"
          "titulo" => "Keywords"
        ]
        2 => array:2 [
          "identificador" => "sec0005"
          "titulo" => "Introduction"
        ]
        3 => array:2 [
          "identificador" => "sec0010"
          "titulo" => "Continuous infusion insulin pump"
        ]
        4 => array:3 [
          "identificador" => "sec0015"
          "titulo" => "The proposed approach"
          "secciones" => array:1 [
            0 => array:2 [
              "identificador" => "sec9005"
              "titulo" => "Emergency"
            ]
          ]
        ]
        5 => array:2 [
          "identificador" => "sec0020"
          "titulo" => "Conclusions"
        ]
        6 => array:1 [
          "titulo" => "References"
        ]
      ]
    ]
    "pdfFichero" => "main.pdf"
    "tienePdf" => true
    "PalabrasClave" => array:1 [
      "en" => array:1 [
        0 => array:4 [
          "clase" => "keyword"
          "titulo" => "Keywords"
          "identificador" => "xpalclavsec520380"
          "palabras" => array:4 [
            0 => "Safety-critical software"
            1 => "hazard"
            2 => "formal languages"
            3 => "CIIP"
          ]
        ]
      ]
    ]
    "tieneResumen" => true
    "resumen" => array:1 [
      "en" => array:2 [
        "titulo" => "Abstract"
        "resumen" => "<span id="abst0005" class="elsevierStyleSection elsevierViewall"><p id="spar0045" class="elsevierStyleSimplePara elsevierViewall">Safety is the most important factor when developing software for safety-critical systems&#46; Traditional approaches attempted to achieve safety through testing the software&#46; However&#44; there might be some bugs in the software not revealed in the test procedure&#46; Formal verification is a new trend in developing safe software&#46; In this paper&#44; we propose a multi-phase formal approach for safety management in safety-critical software&#46; We use timed transition Petri-net as a formal means to specify the properties of the model and their relations in each component of the software&#46; In addition&#44; we use the Z language to specify textual and mathematical specifications of the model&#44; as a representative model to evaluate the proposed approach&#59; we chose continuous infusion insulin pump &#40;CIIP&#41;&#46;</p></span>"
      ]
    ]
    "multimedia" => array:16 [
      0 => array:7 [
        "identificador" => "tbl0005"
        "etiqueta" => "Table 1"
        "tipo" => "MULTIMEDIATABLA"
        "mostrarFloat" => true
        "mostrarDisplay" => false
        "tabla" => array:1 [
          "tablatextoimagen" => array:1 [
            0 => array:2 [
              "tabla" => array:1 [
                0 => """
                  <table border="0" frame="\n
                  \t\t\t\t\tvoid\n
                  \t\t\t\t" class=""><tbody title="tbody"><tr title="table-row"><td class="td" title="table-entry  " align="center" valign="middle"><span class="elsevierStyleBold">Goals</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="left" valign="middle">To control sugar level in a diabetic patient and to inject automatically the correct insulin dose&#46;&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="center" valign="middle"><span class="elsevierStyleBold">Environment</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="left" valign="middle">Patient&#39;s body&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="center" valign="middle"><span class="elsevierStyleBold">Users</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="left" valign="middle">Patient&#44; doctor&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="center" valign="middle"><span class="elsevierStyleBold">Operators</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="left" valign="middle">&#8211;&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr></tbody></table>
                  """
              ]
              "imagenFichero" => array:1 [
                0 => "xTab796438.png"
              ]
            ]
          ]
        ]
        "descripcion" => array:1 [
          "en" => "<p id="spar0005" class="elsevierStyleSimplePara elsevierViewall">Preliminary information about CIIP&#46;</p>"
        ]
      ]
      1 => array:7 [
        "identificador" => "tbl0010"
        "etiqueta" => "Table 2"
        "tipo" => "MULTIMEDIATABLA"
        "mostrarFloat" => true
        "mostrarDisplay" => false
        "tabla" => array:1 [
          "tablatextoimagen" => array:1 [
            0 => array:2 [
              "tabla" => array:1 [
                0 => """
                  <table border="0" frame="\n
                  \t\t\t\t\tvoid\n
                  \t\t\t\t" class=""><thead title="thead"><tr title="table-row"><th class="td" title="table-head  " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black"><span class="elsevierStyleBold">No&#46;</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</th><th class="td" title="table-head  " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black"><span class="elsevierStyleBold">Road map</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</th></tr></thead><tbody title="tbody"><tr title="table-row"><td class="td" title="table-entry  " align="center" valign="middle">1&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="left" valign="middle">Sugar status have to be reported to the patient periodically&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="center" valign="middle">2&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="left" valign="middle">Warn to the user before insulin resource gets empty&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="center" valign="middle">3&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="left" valign="middle">Warn to the user when power is low&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="center" valign="middle">4&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="left" valign="middle">System has not to hurt the patient&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr></tbody></table>
                  """
              ]
              "imagenFichero" => array:1 [
                0 => "xTab796436.png"
              ]
            ]
          ]
        ]
        "descripcion" => array:1 [
          "en" => "<p id="spar0010" class="elsevierStyleSimplePara elsevierViewall">Safety approach for CIIP&#46;</p>"
        ]
      ]
      2 => array:7 [
        "identificador" => "tbl0015"
        "etiqueta" => "Table 3"
        "tipo" => "MULTIMEDIATABLA"
        "mostrarFloat" => true
        "mostrarDisplay" => false
        "tabla" => array:1 [
          "tablatextoimagen" => array:1 [
            0 => array:2 [
              "tabla" => array:1 [
                0 => """
                  <table border="0" frame="\n
                  \t\t\t\t\tvoid\n
                  \t\t\t\t" class=""><thead title="thead"><tr title="table-row"><th class="td" title="table-head  " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black"><span class="elsevierStyleBold">Hazard</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</th><th class="td" title="table-head  " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black"><span class="elsevierStyleBold">Severity</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</th></tr></thead><tbody title="tbody"><tr title="table-row"><td class="td" title="table-entry  " align="center" valign="middle">Power supply fault&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Critical&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="center" valign="middle">Sampling equipment fault&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Critical&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="center" valign="middle">Insulin dose computing fault&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Catastrophic&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="center" valign="middle">Injection equipment fault&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Critical&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr></tbody></table>
                  """
              ]
              "imagenFichero" => array:1 [
                0 => "xTab796434.png"
              ]
            ]
          ]
        ]
        "descripcion" => array:1 [
          "en" => "<p id="spar0015" class="elsevierStyleSimplePara elsevierViewall">High level hazard classification for CIIP <a class="elsevierStyleCrossRef" href="#bib0060">&#91;12&#93;</a>&#46;</p>"
        ]
      ]
      3 => array:7 [
        "identificador" => "tbl0020"
        "etiqueta" => "Table 4"
        "tipo" => "MULTIMEDIATABLA"
        "mostrarFloat" => true
        "mostrarDisplay" => false
        "tabla" => array:1 [
          "tablatextoimagen" => array:1 [
            0 => array:2 [
              "tabla" => array:1 [
                0 => """
                  <table border="0" frame="\n
                  \t\t\t\t\tvoid\n
                  \t\t\t\t" class=""><tbody title="tbody"><tr title="table-row"><td class="td" title="table-entry  " rowspan="4" align="center" valign="middle" style="border-bottom: 2px solid black"><span class="elsevierStyleBold">Severity</span></td><td class="td" title="table-entry  " align="left" valign="middle" style="border-bottom: 2px solid black">1&#46; Catastrophic&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="left" valign="middle" style="border-bottom: 2px solid black">2&#46; Critical&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="left" valign="middle" style="border-bottom: 2px solid black">3&#46; Marginal&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="left" valign="middle" style="border-bottom: 2px solid black">4&#46; Negligible&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " rowspan="5" align="center" valign="middle"><span class="elsevierStyleBold">Probability</span></td><td class="td" title="table-entry  " align="left" valign="middle" style="border-bottom: 2px solid black">A&#46; Frequent&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="left" valign="middle" style="border-bottom: 2px solid black">B&#46; Probable&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="left" valign="middle" style="border-bottom: 2px solid black">C&#46; Occasional&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="left" valign="middle" style="border-bottom: 2px solid black">D&#46; Remote&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="left" valign="middle">E&#46; Improbable&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr></tbody></table>
                  """
              ]
              "imagenFichero" => array:1 [
                0 => "xTab796437.png"
              ]
            ]
          ]
        ]
        "descripcion" => array:1 [
          "en" => "<p id="spar0020" class="elsevierStyleSimplePara elsevierViewall">Hazard risk factor 13&#46;</p>"
        ]
      ]
      4 => array:7 [
        "identificador" => "tbl0025"
        "etiqueta" => "Table 7"
        "tipo" => "MULTIMEDIATABLA"
        "mostrarFloat" => true
        "mostrarDisplay" => false
        "tabla" => array:1 [
          "tablatextoimagen" => array:1 [
            0 => array:2 [
              "tabla" => array:1 [
                0 => """
                  <table border="0" frame="\n
                  \t\t\t\t\tvoid\n
                  \t\t\t\t" class=""><thead title="thead"><tr title="table-row"><th class="td" title="table-head  " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black"><span class="elsevierStyleBold">Transition</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</th><th class="td" title="table-head  " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black"><span class="elsevierStyleBold">Events or conditions</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</th></tr></thead><tbody title="tbody"><tr title="table-row"><td class="td" title="table-entry  " align="center" valign="middle">T1&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Sugar &#62; SafeMax&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="center" valign="middle">T2&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Sugar &#60;&#61;SafeMax&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="center" valign="middle">T3&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Sugar &#60; SafeMin&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="center" valign="middle">T4&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Sugar &#62;&#61; SafeMin&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="center" valign="middle">T5&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Time &#62;&#61; 10&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="center" valign="middle">T6&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">E1&#58; EndSampling&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="center" valign="middle">T7&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Time &#62;&#61; 10&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="center" valign="middle">T8&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">E1&#58; EndSampling&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="center" valign="middle">T9&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Time &#62;&#61; 10&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="center" valign="middle">T10&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">E1&#58; EndSampling&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="center" valign="middle">T11&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Time &#62;&#61; 10&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="center" valign="middle">T12&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">E1&#58; EndSampling&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="center" valign="middle">T13&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">E2&#58; EndComputing&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="center" valign="middle">T14&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">E3&#58; EndInjecting&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="center" valign="middle">T15&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Insulin &#60; MinDose Or Insulin &#60; ComputedDose OR Charge &#60; MinCharge&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="center" valign="middle">T16&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Insulin &#62;&#61; MinDose AND Insulin &#62;&#61; ComputedDose AND Charge &#62;&#61; MinCharge&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="center" valign="middle">T17&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Charge &#60; MinCharge&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="center" valign="middle">T18&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Charge &#62;&#61; MinCharge&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="center" valign="middle">T19&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Insulin &#60; MinDose&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="center" valign="middle">T20&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Insulin &#62;&#61; MinDose&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr></tbody></table>
                  """
              ]
              "imagenFichero" => array:1 [
                0 => "xTab796430.png"
              ]
            ]
          ]
        ]
        "descripcion" => array:1 [
          "en" => "<p id="spar0025" class="elsevierStyleSimplePara elsevierViewall">Transitions on the CIIP Petri-net model&#46;</p>"
        ]
      ]
      5 => array:7 [
        "identificador" => "tbl0030"
        "etiqueta" => "Table 8"
        "tipo" => "MULTIMEDIATABLA"
        "mostrarFloat" => true
        "mostrarDisplay" => false
        "tabla" => array:1 [
          "tablatextoimagen" => array:1 [
            0 => array:2 [
              "tabla" => array:1 [
                0 => """
                  <table border="0" frame="\n
                  \t\t\t\t\tvoid\n
                  \t\t\t\t" class=""><thead title="thead"><tr title="table-row"><th class="td" title="table-head  " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black"><span class="elsevierStyleBold">State name</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</th><th class="td" title="table-head  " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black"><span class="elsevierStyleBold">Conception</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</th><th class="td" title="table-head  " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black"><span class="elsevierStyleBold">Log times</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</th><th class="td" title="table-head  " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black"><span class="elsevierStyleBold">Details</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</th></tr></thead><tbody title="tbody"><tr title="table-row"><td class="td" title="table-entry  " align="center" valign="middle">Charge&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Power supply energy&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Every minute&#44; after warning enabled or warning disabled&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">&#8211;&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="center" valign="middle">insulinAvailable&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Available insulin in reservoir&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Every minute&#44; after warning enabled or warning disabled&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">&#8211;&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="center" valign="middle">computed Dose&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Computed dose&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Immediately after end of computing operation&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">After the end of the injecting operation the amount of this log become zero&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="center" valign="middle">cumulativ eDose&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Cumulative dose&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Immediately after the end of the injecting operation&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">After every 24 hours&#44; the amount of this log become zero&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr></tbody></table>
                  """
              ]
              "imagenFichero" => array:1 [
                0 => "xTab796433.png"
              ]
            ]
          ]
        ]
        "descripcion" => array:1 [
          "en" => "<p id="spar0030" class="elsevierStyleSimplePara elsevierViewall">Critical states of CIIP&#46;</p>"
        ]
      ]
      6 => array:7 [
        "identificador" => "tbl0035"
        "etiqueta" => "Table 9"
        "tipo" => "MULTIMEDIATABLA"
        "mostrarFloat" => true
        "mostrarDisplay" => false
        "tabla" => array:1 [
          "tablatextoimagen" => array:1 [
            0 => array:2 [
              "tabla" => array:1 [
                0 => """
                  <table border="0" frame="\n
                  \t\t\t\t\tvoid\n
                  \t\t\t\t" class=""><thead title="thead"><tr title="table-row"><th class="td" title="table-head  " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black"><span class="elsevierStyleBold">Critical behavior</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</th><th class="td" title="table-head  " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black"><span class="elsevierStyleBold">Conditions</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</th><th class="td" title="table-head  " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black"><span class="elsevierStyleBold">Permission</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</th></tr></thead><tbody title="tbody"><tr title="table-row"><td class="td" title="table-entry  " rowspan="2" align="center" valign="middle">Beginning of the injecting operation</td><td class="td" title="table-entry  " align="center" valign="middle">Charge &#62; minCharge AND insulinavailable &#62; minDose AND ComputedDose &#62; 0 AND cumulativeDose &#60;&#61;25&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">True&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="center" valign="middle">&#8764;&#40; Charge &#62; minCharge AND insulinavailable &#62; minDose AND ComputedDose &#62; 0 AND cumulativeDose &#60;&#61;25&#41;&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">False&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr></tbody></table>
                  """
              ]
              "imagenFichero" => array:1 [
                0 => "xTab796432.png"
              ]
            ]
          ]
        ]
        "descripcion" => array:1 [
          "en" => "<p id="spar0035" class="elsevierStyleSimplePara elsevierViewall">Change permissions for critical behavior of CIIP</p>"
        ]
      ]
      7 => array:7 [
        "identificador" => "tbl0040"
        "etiqueta" => "Schema 8"
        "tipo" => "MULTIMEDIATABLA"
        "mostrarFloat" => true
        "mostrarDisplay" => false
        "tabla" => array:1 [
          "tablatextoimagen" => array:1 [
            0 => array:2 [
              "tabla" => array:1 [
                0 => """
                  <table border="0" frame="\n
                  \t\t\t\t\tvoid\n
                  \t\t\t\t" class=""><tbody title="tbody"><tr title="table-row"><td class="td" title="table-entry  " align="left" valign="middle">&#916; PUBLIC&#95;STATES&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="left" valign="middle">systemStatus &#61; standby&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="left" valign="middle">systemState &#61; sendingMessage&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="left" valign="middle">warnningAlarml&#33; &#8722; on&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="left" valign="middle">warnningAlarm2&#33; &#61; on&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="left" valign="middle">messagel&#33; &#61; &#8220;System Failure&#8221;&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr></tbody></table>
                  """
              ]
              "imagenFichero" => array:1 [
                0 => "xTab796435.png"
              ]
            ]
          ]
        ]
        "descripcion" => array:1 [
          "en" => "<p id="spar0040" class="elsevierStyleSimplePara elsevierViewall">Disaster management for CIIP in the Z language&#46;</p>"
        ]
      ]
      8 => array:6 [
        "identificador" => "fig0005"
        "tipo" => "MULTIMEDIAFIGURA"
        "mostrarFloat" => false
        "mostrarDisplay" => true
        "figura" => array:1 [
          0 => array:4 [
            "imagen" => "gr1.jpeg"
            "Alto" => 774
            "Ancho" => 1680
            "Tamanyo" => 121344
          ]
        ]
        "descripcion" => array:1 [
          "en" => "<p id="spar0050" class="elsevierStyleSimplePara elsevierViewall">&#8195;</p>"
        ]
      ]
      9 => array:5 [
        "identificador" => "tbl0045"
        "tipo" => "MULTIMEDIATABLA"
        "mostrarFloat" => false
        "mostrarDisplay" => true
        "tabla" => array:1 [
          "tablatextoimagen" => array:1 [
            0 => array:2 [
              "tabla" => array:1 [
                0 => """
                  <table border="0" frame="\n
                  \t\t\t\t\tvoid\n
                  \t\t\t\t" class=""><thead title="thead"><tr title="table-row"><th class="td" title="table-head  " colspan="12" align="center" valign="middle" scope="col" style="border-bottom: 2px solid black"><span class="elsevierStyleBold">Fmea</span></th></tr><tr title="table-row"><th class="td" title="table-head  " colspan="5" align="left" valign="middle" scope="col" style="border-bottom: 2px solid black"><span class="elsevierStyleBold">System&#58; CIIP</span></th><th class="td" title="table-head  " colspan="7" align="left" valign="middle" scope="col" style="border-bottom: 2px solid black"><span class="elsevierStyleBold">Subsystem</span>&#58; -</th></tr><tr title="table-row"><th class="td" title="table-head  " colspan="12" align="left" valign="middle" scope="col"><span class="elsevierStyleBold">Mode&#47;Phase&#58; Operating</span></th></tr><tr title="table-row"><th class="td" title="table-head  " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black"><span class="elsevierStyleBold">Component</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</th><th class="td" title="table-head  " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black"><span class="elsevierStyleBold">Failure mode</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</th><th class="td" title="table-head  " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black"><span class="elsevierStyleBold">Failure rate</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</th><th class="td" title="table-head  " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black"><span class="elsevierStyleBold">Failure reasons</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</th><th class="td" title="table-head  " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black"><span class="elsevierStyleBold">Suddenly effect</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</th><th class="td" title="table-head  " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black"><span class="elsevierStyleBold">System effect</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</th><th class="td" title="table-head  " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black"><span class="elsevierStyleBold">Detection method</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</th><th class="td" title="table-head  " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black"><span class="elsevierStyleBold">Current control</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</th><th class="td" title="table-head  " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black"><span class="elsevierStyleBold">Hazard</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</th><th class="td" title="table-head  " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black"><span class="elsevierStyleBold">Hazard risk</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</th><th class="td" title="table-head  " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black"><span class="elsevierStyleBold">Recommended action</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</th><th class="td" title="table-head  " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black"><span class="elsevierStyleBold">row</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</th></tr></thead><tbody title="tbody"><tr title="table-row"><td class="td" title="table-entry  " rowspan="2" align="center" valign="middle">Power supply</td><td class="td" title="table-entry  " align="center" valign="middle">Failed&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">1&#46;1 &#42; 10&#8211;9 &#40;manufacture information&#41;&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Control circuit failed&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Electricity current disconnection&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">System downs&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Current test&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Quality control&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Sugar level increasing&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">2B&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Using from a current sensor with backup battery to warn user power supply is failed&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">1&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="center" valign="middle">Energy decreasing&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Not available&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Battery energy decreasing&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Electricity current decreasing&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">System incorrect action&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Current test&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">&#8211;&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Sugar level increasing&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">2B&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Using from a current sensor with backup battery to warn user change the system battery&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">2&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="center" valign="middle">Sampling subsystem&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Failed&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">5 &#42; 10&#8211;4 &#40;manufacture information&#41;&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Hardware fault&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Not receiving sugar sample&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Not computing and injecting insulin dose&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Inspecting&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Quality control&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Sugar level increasing&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">2B&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Automatic test&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">3&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " rowspan="2" align="center" valign="middle">Insulin dose computing subsystem</td><td class="td" title="table-entry  " align="center" valign="middle">Failed&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Not available&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Hardware fault&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Not computing insulin dose&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Not injecting insulin dose&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">System testing&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">&#8211;&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">&#95;Sugar level increasing&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">2B&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">&#8211;&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">4&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="center" valign="middle">Computing fault&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">&#8211;&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Hardware fault&#44; programming fault&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Not computing insulin dose&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Unsafe system behavior&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">System testing&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Software testing&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Serious hurt to patient&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">1A&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Hard testing&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">5&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " rowspan="2" align="center" valign="middle">Injecting subsystem</td><td class="td" title="table-entry  " align="center" valign="middle">Failed&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">5 &#42; 10<span class="elsevierStyleSup">&#8722;4</span> &#40;manufacture information&#41;&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Hardware fault&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Not injecting insulin dose&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Not injecting insulin dose&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Inspection&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Quality control&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Sugar level increasing&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">2B&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Automatic test&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">6&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="center" valign="middle">Not enough insulin&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">&#8211;&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Not charging insulin reservoir&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Not injecting insulin dose&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Not injecting insulin dose&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Resource inspection&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">&#8211;&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Sugar level increasing&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">2B&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Using from a sensor to assess reservoir insulin level&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">7&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr></tbody></table>
                  """
              ]
              "imagenFichero" => array:1 [
                0 => "xTab796440.png"
              ]
            ]
          ]
        ]
      ]
      10 => array:5 [
        "identificador" => "tbl0050"
        "tipo" => "MULTIMEDIATABLA"
        "mostrarFloat" => false
        "mostrarDisplay" => true
        "tabla" => array:1 [
          "tablatextoimagen" => array:1 [
            0 => array:2 [
              "tabla" => array:1 [
                0 => """
                  <table border="0" frame="\n
                  \t\t\t\t\tvoid\n
                  \t\t\t\t" class=""><thead title="thead"><tr title="table-row"><th class="td" title="table-head  " colspan="12" align="center" valign="middle" scope="col" style="border-bottom: 2px solid black"><span class="elsevierStyleBold">Fmea</span></th></tr><tr title="table-row"><th class="td" title="table-head  " colspan="6" align="left" valign="middle" scope="col" style="border-bottom: 2px solid black"><span class="elsevierStyleBold">System&#58; CIIP</span></th><th class="td" title="table-head  " colspan="6" align="left" valign="middle" scope="col" style="border-bottom: 2px solid black"><span class="elsevierStyleBold">Subsystem</span>&#58; -</th></tr><tr title="table-row"><th class="td" title="table-head  " colspan="12" align="left" valign="middle" scope="col"><span class="elsevierStyleBold">Mode&#47;Phase&#58; Operating</span></th></tr><tr title="table-row"><th class="td" title="table-head  " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black"><span class="elsevierStyleBold">Function</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</th><th class="td" title="table-head  " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black"><span class="elsevierStyleBold">Failure mode</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</th><th class="td" title="table-head  " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black"><span class="elsevierStyleBold">Failure rate</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</th><th class="td" title="table-head  " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black"><span class="elsevierStyleBold">Failure reasons</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</th><th class="td" title="table-head  " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black"><span class="elsevierStyleBold">Suddenly effect</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</th><th class="td" title="table-head  " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black"><span class="elsevierStyleBold">System effects</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</th><th class="td" title="table-head  " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black"><span class="elsevierStyleBold">Detection method</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</th><th class="td" title="table-head  " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black"><span class="elsevierStyleBold">Current control</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</th><th class="td" title="table-head  " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black"><span class="elsevierStyleBold">Hazard</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</th><th class="td" title="table-head  " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black"><span class="elsevierStyleBold">Hazard risk</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</th><th class="td" title="table-head  " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black"><span class="elsevierStyleBold">Recommended action</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</th><th class="td" title="table-head  " align="center" valign="middle" scope="col" style="border-bottom: 2px solid black"><span class="elsevierStyleBold">Row</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</th></tr></thead><tbody title="tbody"><tr title="table-row"><td class="td" title="table-entry  " align="center" valign="middle">Sampling&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Not happening&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Not available&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Hardware fault&#44; software fault&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Not receiving sample&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Nor computing nor injecting insulin&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Not resetting new sample&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">&#8211;&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Face to unsafe status&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">2B&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Warn to user after 10 second &#40;runtime safety management&#41;&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">1&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " rowspan="3" align="center" valign="middle">Insulin injecting</td><td class="td" title="table-entry  " align="center" valign="middle">Not happening&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Not available&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Insulin reservoir is empty&#44; hardware fault&#44; software fault&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Not injecting insulin&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Injecting incorrect dose in the next injection&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Not resetting new sample&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">&#8211;&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Increasing sugar level&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">2B&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Warn the user after 30 second &#40;runtime safety management&#41;&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">2&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="center" valign="middle">Injecting lower dose than specified&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Not available&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">leakage of insulin in reservoir&#44; hardware fault&#44; software fault&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">&#8211;&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Injecting incorrect dose in the next injection&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">&#8211;&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">&#8211;&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Increasing sugar level&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">2B&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Transactional injecting &#40;runtime safety management&#41;&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">3&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="center" valign="middle">Injecting higher dose than specified&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Not available&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Hardware fault&#44; software fault&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">&#8211;&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Injecting incorrect dose in the next injection&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">&#8211;&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">&#8211;&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Patient going to a coma&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">1A&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">Daily injection control&#44; hard testing&#44; injection guards &#40;runtime safety management&#41;&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td><td class="td" title="table-entry  " align="center" valign="middle">4&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr></tbody></table>
                  """
              ]
              "imagenFichero" => array:1 [
                0 => "xTab796431.png"
              ]
            ]
          ]
        ]
      ]
      11 => array:5 [
        "identificador" => "tbl0055"
        "tipo" => "MULTIMEDIATABLA"
        "mostrarFloat" => false
        "mostrarDisplay" => true
        "tabla" => array:1 [
          "tablatextoimagen" => array:1 [
            0 => array:2 [
              "tabla" => array:1 [
                0 => """
                  <table border="0" frame="\n
                  \t\t\t\t\tvoid\n
                  \t\t\t\t" class=""><tbody title="tbody"><tr title="table-row"><td class="td" title="table-entry  " align="left" valign="middle">insulinAvailable &#58; N &#47;&#47; <span class="elsevierStyleItalic">amount of insulin in the reservoir</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="left" valign="middle">computedDose &#58; N &#47;&#47; <span class="elsevierStyleItalic">amount of computed insulin dose</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="left" valign="middle">cumulativeDose &#58; N &#47;&#47; <span class="elsevierStyleItalic">sum of insulin doses that were injected in current day</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="left" valign="middle">injectionDose &#58; N &#47;&#47; <span class="elsevierStyleItalic">amount of insulin dose that must be injected</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="left" valign="middle">safeMin &#58; N &#47;&#47; <span class="elsevierStyleItalic">one limit more or less than it means blood sugar is low</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="left" valign="middle">safeMax &#58; N &#47;&#47; <span class="elsevierStyleItalic">one limit bigger than it means blood sugar is high</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="left" valign="middle">maxDailyDose &#58; N &#47;&#47; <span class="elsevierStyleItalic">maximum insulin dose is legal to be injected in one day</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="left" valign="middle">maxSingleDose &#58; N &#47;&#47; <span class="elsevierStyleItalic">maximum insulin dose is legal to be injected in a ten-minute cycle</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="left" valign="middle">minimumDose &#58; N &#47;&#47; <span class="elsevierStyleItalic">minimum insulin dose can be injected</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="left" valign="middle">first&#95;sample&#44; second&#95;sample&#44; third&#95;sample &#58; N &#47;&#47; <span class="elsevierStyleItalic">three last blood sugar of diabetic</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="left" valign="middle">charge &#58; &#123;1&#44; 2&#44; 3&#44; 4&#44; 5&#44; 6&#44; 7&#44; 8&#125; &#47;&#47; <span class="elsevierStyleItalic">amount of the power charge</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="left" valign="middle">minCharge &#58; &#123;1&#44; 2&#44; 3&#44; 4&#44; 5&#44; 6&#44; 7&#44; 8&#125; &#47;&#47; <span class="elsevierStyleItalic">minimum allowed amount of the power charge</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="left" valign="middle">warningAlarm1&#33; &#58; &#123;on&#44; off&#125; &#47;&#47;<span class="elsevierStyleItalic">to show a power warning to the diabetic</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="left" valign="middle">warningAlarm2&#33; &#58; &#123;on&#44; off&#125; &#47;&#47; <span class="elsevierStyleItalic">to show a insulin warning to the diabetic</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="left" valign="middle">message1&#33; &#58; string &#47;&#47; <span class="elsevierStyleItalic">showing a warning about power charge</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="left" valign="middle">message2&#33; &#58; string &#47;&#47; <span class="elsevierStyleItalic">showing a warning about available insulin in the reservoir</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="left" valign="middle">systemStatus &#58; &#123; run&#44; standby&#125; &#47;&#47; <span class="elsevierStyleItalic">status of system running</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="left" valign="middle">systemState &#58; &#123;sampling&#44; computing&#44; injecting&#44; sendingMessage&#125; &#47;&#47; <span class="elsevierStyleItalic">states of system</span> clock&#63; &#58; TIME &#47;&#47;inputted time&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="left" valign="middle">clock&#33; TIME &#47;&#47;outputted time&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="left" valign="middle">&#47;&#47; <span class="elsevierStyleItalic">configuration parameters</span>&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="left" valign="middle">minimumDose &#61; 1&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="left" valign="middle">safeMin &#61; 6&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="left" valign="middle">safeMax &#61; 14&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="left" valign="middle">maxDailyDose &#61; 25&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="left" valign="middle">maxSingleDose &#61; 4&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr><tr title="table-row"><td class="td" title="table-entry  " align="left" valign="middle">minCharge &#61; 2&nbsp;\t\t\t\t\t\t\n
                  \t\t\t\t</td></tr></tbody></table>
                  """
              ]
              "imagenFichero" => array:1 [
                0 => "xTab796439.png"
              ]
            ]
          ]
        ]
      ]
      12 => array:5 [
        "identificador" => "tb0005"
        "tipo" => "MULTIMEDIATEXTO"
        "mostrarFloat" => false
        "mostrarDisplay" => true
        "texto" => array:1 [
          "textoCompleto" => "<span class="elsevierStyleSections"><p id="par0250" class="elsevierStylePara elsevierViewall">&#916;PUBLIC&#95;STATES</p><p id="par0255" class="elsevierStylePara elsevierViewall">clock&#63; &#61; 001000 &#10132; &#40;clock&#33; &#61; 000000&#41; &#8743; &#40;injectionDose&#39; &#61; 0&#41; &#8743; &#40;computedDose&#39; &#61; 0&#41; A &#40;first&#95;sample&#39; &#61;</p><p id="par0260" class="elsevierStylePara elsevierViewall">second&#95;sample&#41; &#8743; &#40;second &#95;sample&#39; &#61; third&#95;sample&#41; &#8743; &#40;third &#95;sample&#39; &#61; 0&#41;</p><p id="par0265" class="elsevierStylePara elsevierViewall">systemStatus &#61; run &#8744; standby</p><p id="par0270" class="elsevierStylePara elsevierViewall">&#47;&#47; <span class="elsevierStyleItalic">dose of insulin is computed depending on the blood sugar level</span></p><p id="par0275" class="elsevierStylePara elsevierViewall">SUGAR&#95;NORMAL &#8744; SUGAR&#95;HIGH &#8744; SUGAR&#95;LOW</p><p id="par0280" class="elsevierStylePara elsevierViewall"><span class="elsevierStyleItalic">&#47;&#47; safety rules</span></p><p id="par0285" class="elsevierStylePara elsevierViewall">SAFETY</p><p id="par0290" class="elsevierStylePara elsevierViewall">cumulativeDose&#39; &#61; cumulativeDose &#43; injectionDose<a name="p691"></a></p><p id="par0295" class="elsevierStylePara elsevierViewall">systemStatus &#61; run</p><p id="par0300" class="elsevierStylePara elsevierViewall">systemState &#61; Computing</p><p id="par0305" class="elsevierStylePara elsevierViewall">&#40;third&#95;sample &#62;&#61; safeMin&#41; &#8743; &#40;third&#95;sample &#60;&#61; safeMax&#41;</p><p id="par0310" class="elsevierStylePara elsevierViewall">&#47;&#47; sugar level stable or falling</p><p id="par0315" class="elsevierStylePara elsevierViewall">&#40;third&#95;sample &#60;&#61; second&#95;sample&#41;&#10132;&#40;computedDose &#61; 0&#41;</p><p id="par0320" class="elsevierStylePara elsevierViewall">&#47;&#47; <span class="elsevierStyleItalic">sugar level increases but rate of increase falls</span></p><p id="par0325" class="elsevierStylePara elsevierViewall">&#40;third&#95;sample &#62; second&#95;sample&#41; &#8743;&#40;third&#95;sample - second&#95;sample&#41; &#60; &#40;second&#95;sample - first&#95;sample&#41;</p><p id="par0330" class="elsevierStylePara elsevierViewall">&#10132;&#40;computedDose &#61; 0&#41;</p><p id="par0335" class="elsevierStylePara elsevierViewall">&#47;&#47; <span class="elsevierStyleItalic">sugar level increases and rate of increase increases compute dose</span></p><p id="par0340" class="elsevierStylePara elsevierViewall">&#47;&#47; <span class="elsevierStyleItalic">a minimum dose must be delivered if rounded to zero</span></p><p id="par0345" class="elsevierStylePara elsevierViewall">&#40;third&#95;sample &#62; second&#95;sample&#41; &#8743;&#40;third&#95;sample - second&#95;sample&#41; &#62;&#61; &#40;second&#95;sample - first&#95;sample&#41;</p><p id="par0350" class="elsevierStylePara elsevierViewall">&#8743;&#40;round&#40;&#40;third&#95;sample - second&#95;sample&#41;&#47;4&#41; &#61; 0&#41; &#10132;&#40;computedDose &#61; minimumDose&#41;</p><p id="par0355" class="elsevierStylePara elsevierViewall">&#40;third&#95;sample &#62; second&#95;sample&#41; A&#40;third&#95;sample - second&#95;sample&#41; &#62;&#61; &#40;second&#95;sample - first&#95;sample&#41;</p><p id="par0360" class="elsevierStylePara elsevierViewall">&#8743;&#40;round&#40;&#40;third&#95;sample - second&#95;sample&#41;&#47;4&#41; &#62; 0&#41; &#10132;&#40;computedDose &#61; round&#40;&#40;third&#95;sample -</p><p id="par0365" class="elsevierStylePara elsevierViewall">second&#95;sample&#41;&#47;4&#41;</p></span>"
        ]
      ]
      13 => array:5 [
        "identificador" => "tb0010"
        "tipo" => "MULTIMEDIATEXTO"
        "mostrarFloat" => false
        "mostrarDisplay" => true
        "texto" => array:1 [
          "textoCompleto" => "<span class="elsevierStyleSections"><p id="par0370" class="elsevierStylePara elsevierViewall">S ystemStatus &#61; run</p><p id="par0375" class="elsevierStylePara elsevierViewall">systemState &#61; Computing</p><p id="par0380" class="elsevierStylePara elsevierViewall">third&#95;sample &#62; safeMax</p><p id="par0385" class="elsevierStylePara elsevierViewall"><span class="elsevierStyleItalic">&#47;&#47; sugar level increasing&#46; Round down if below 1 unit</span></p><p id="par0390" class="elsevierStylePara elsevierViewall">&#40;third&#95;sample &#62; second&#95;sample&#41; &#8743;&#40;round&#40;&#40;third&#95;sample- second&#95;sample&#41;&#47;4&#41; &#61; 0&#41; &#10132;&#40;computedDose &#61;</p><p id="par0395" class="elsevierStylePara elsevierViewall">minimumDose&#41;</p><p id="par0400" class="elsevierStylePara elsevierViewall">&#40;third&#95;sample &#62; second&#95;sample&#41; &#8743;&#40;round&#40;&#40;third&#95;sample-second&#95;sample&#41;&#47;4&#41; &#62; 0&#41; &#8743;&#40;computedDose &#61;</p><p id="par0405" class="elsevierStylePara elsevierViewall">round&#40;&#40;third&#95;sample - second&#95;sample&#41;&#47;4&#41;&#41;</p><p id="par0410" class="elsevierStylePara elsevierViewall"><span class="elsevierStyleItalic">&#47;&#47; sugarlevel stable</span></p><p id="par0415" class="elsevierStylePara elsevierViewall">&#40;third&#95;sample &#61; second&#95;sample&#41; &#10132;&#40;computedDose &#61; minimumDose&#41;</p><p id="par0420" class="elsevierStylePara elsevierViewall"><span class="elsevierStyleItalic">&#47;&#47; sugar level falling and rate of increase decreasing</span></p><p id="par0425" class="elsevierStylePara elsevierViewall">&#40;third&#95;sample &#60; second&#95;sample&#41; &#8743;&#40;third&#95;sample - second&#95;sample&#41; &#60;&#61; &#40;second&#95;sample - first&#95;sample&#41;</p><p id="par0430" class="elsevierStylePara elsevierViewall">&#10132;&#40;computedDose &#61; 0&#41;</p><p id="par0435" class="elsevierStylePara elsevierViewall"><span class="elsevierStyleItalic">&#47;&#47; sugar level falling and rate of increase increasing</span></p><p id="par0440" class="elsevierStylePara elsevierViewall">&#40;third&#95;sample &#60; second&#95;sample&#41; &#8743;&#40;third&#95;sample - second&#95;sample&#41; &#62; &#40;second&#95;sample - first&#95;sample&#41;</p><p id="par0445" class="elsevierStylePara elsevierViewall">&#10132;&#40;computedDose &#61; minimumDose&#41;<a name="p692"></a></p><p id="par0450" class="elsevierStylePara elsevierViewall">systemStatus &#61; run</p><p id="par0455" class="elsevierStylePara elsevierViewall">systemState &#61; Computing</p><p id="par0460" class="elsevierStylePara elsevierViewall">third&#95;sample &#60; safeMin</p><p id="par0465" class="elsevierStylePara elsevierViewall">computedDose &#61; 0</p><p id="par0470" class="elsevierStylePara elsevierViewall">warningAlarm&#33; &#61; on</p><p id="par0475" class="elsevierStylePara elsevierViewall">message&#33; &#61; &#8220;Your sugar is very low&#46; Please call your doctor&#46;&#8221;</p></span>"
        ]
      ]
      14 => array:5 [
        "identificador" => "tb0015"
        "tipo" => "MULTIMEDIATEXTO"
        "mostrarFloat" => false
        "mostrarDisplay" => true
        "texto" => array:1 [
          "textoCompleto" => "<span class="elsevierStyleSections"><p id="par0480" class="elsevierStylePara elsevierViewall">charge &#60; minCharge &#10132; &#40;warningAlarm1&#33; &#61; on&#41; &#8743; &#40;messag e1&#33;&#61; &#8220;Low charge&#46;&#8221;&#41; A &#40;systemStatus &#61; standby&#41;</p><p id="par0485" class="elsevierStylePara elsevierViewall">charge &#62;&#61; minCharge &#10132; &#40;warningAlarm1&#33; &#61; off&#41; &#8743; &#40;message1&#33; &#61; &#8220;&#8221;&#41; &#10132; &#40;systemStatus &#61; run&#41;</p><p id="par0490" class="elsevierStylePara elsevierViewall">&#40;insulinAvailable &#60; minDose &#41; &#8744; &#40;insulinAvailable &#60; injectionDose&#41; &#10132; &#40;warningAlarm2&#33; &#61; on&#41; A &#40;message2&#33; &#61;</p><p id="par0495" class="elsevierStylePara elsevierViewall">&#8220;Low insulin&#46;&#8221;&#41; &#8743; &#40;systemStatus &#61; standby&#41;</p><p id="par0500" class="elsevierStylePara elsevierViewall">&#40;insulinAvailable &#62; minDose &#41; &#8744; &#40;insulinAvailable &#62; injectionDose&#41; &#10132; &#40;warningAlarm2&#33; &#61; off&#41; A &#40;message2&#33; &#61;</p><p id="par0505" class="elsevierStylePara elsevierViewall">&#8217;&#8221;&#41; A &#40;systemStatus &#61; run&#41;</p><p id="par0510" class="elsevierStylePara elsevierViewall">cumulativeDose &#60;&#61; 25 &#10132; injectionDose &#61; computedDose</p><p id="par0515" class="elsevierStylePara elsevierViewall">cumulativeDose &#62; 25 &#10132; injectionDose &#61; 0</p></span>"
        ]
      ]
      15 => array:5 [
        "identificador" => "tb0020"
        "tipo" => "MULTIMEDIATEXTO"
        "mostrarFloat" => false
        "mostrarDisplay" => true
        "texto" => array:1 [
          "textoCompleto" => "<span class="elsevierStyleSections"><p id="par0520" class="elsevierStylePara elsevierViewall">&#916; PUBLIC&#95;STATES</p><p id="par0525" class="elsevierStylePara elsevierViewall">systemState &#61; sampling &#10132; clock&#63; &#60;&#61; 000010</p><p id="par0530" class="elsevierStylePara elsevierViewall">systemState &#61; injecting &#10132; &#40;injectionDose &#62; 0&#41; &#8743; &#40;insulinAvailable &#62;&#61; injectionDose&#41; &#8743; &#40;charge &#62;&#61;</p><p id="par0535" class="elsevierStylePara elsevierViewall">minCharge&#41;</p><p id="par0540" class="elsevierStylePara elsevierViewall">third&#95;sample &#60; safeMin &#10132; injectionDose &#61; 0</p><p id="par0545" class="elsevierStylePara elsevierViewall">injectionDose &#60;&#61; maxDose</p><p id="par0550" class="elsevierStylePara elsevierViewall">systemState &#61; injecting &#10132; clock&#63; &#60;&#61; 000030</p></span>"
        ]
      ]
    ]
    "bibliografia" => array:2 [
      "titulo" => "References"
      "seccion" => array:1 [
        0 => array:2 [
          "identificador" => "bibs0005"
          "bibliografiaReferencia" => array:20 [
            0 => array:3 [
              "identificador" => "bib0005"
              "etiqueta" => "&#91;1&#93;"
              "referencia" => array:1 [
                0 => array:2 [
                  "contribucion" => array:1 [
                    0 => array:1 [
                      "autores" => array:1 [
                        0 => array:2 [
                          "etal" => false
                          "autores" => array:2 [
                            0 => "J&#46; Slagle"
                            1 => "S&#46; Shankar"
                          ]
                        ]
                      ]
                    ]
                  ]
                  "host" => array:1 [
                    0 => array:1 [
                      "Libro" => array:4 [
                        "titulo" => "Theorem proving"
                        "fecha" => "2003"
                        "editorial" => "John Wiley and Sons Ltd"
                        "editorialLocalizacion" => "Chichester&#44; UK"
                      ]
                    ]
                  ]
                ]
              ]
            ]
            1 => array:3 [
              "identificador" => "bib0010"
              "etiqueta" => "&#91;2&#93;"
              "referencia" => array:1 [
                0 => array:2 [
                  "contribucion" => array:1 [
                    0 => array:1 [
                      "autores" => array:1 [
                        0 => array:2 [
                          "etal" => false
                          "autores" => array:2 [
                            0 => "C&#46; Baier"
                            1 => "J&#46; Katoen"
                          ]
                        ]
                      ]
                    ]
                  ]
                  "host" => array:1 [
                    0 => array:1 [
                      "Libro" => array:4 [
                        "titulo" => "Principles of Model Checking"
                        "fecha" => "2008"
                        "editorial" => "MIT Press"
                        "editorialLocalizacion" => "London&#44; England&#58; Cambridge&#44; Mass"
                      ]
                    ]
                  ]
                ]
              ]
            ]
            2 => array:3 [
              "identificador" => "bib0015"
              "etiqueta" => "&#91;3&#93;"
              "referencia" => array:1 [
                0 => array:2 [
                  "contribucion" => array:1 [
                    0 => array:2 [
                      "titulo" => "Checking and Enforcing Safety&#58; Runtime Verification and Runtime Reflection"
                      "autores" => array:1 [
                        0 => array:2 [
                          "etal" => false
                          "autores" => array:1 [
                            0 => "M&#46; Leucker"
                          ]
                        ]
                      ]
                    ]
                  ]
                  "host" => array:1 [
                    0 => array:1 [
                      "Revista" => array:5 [
                        "tituloSerie" => "ERCIM News"
                        "fecha" => "2008"
                        "volumen" => "75"
                        "paginaInicial" => "35"
                        "paginaFinal" => "36"
                      ]
                    ]
                  ]
                ]
              ]
            ]
            3 => array:3 [
              "identificador" => "bib0020"
              "etiqueta" => "&#91;4&#93;"
              "referencia" => array:1 [
                0 => array:2 [
                  "contribucion" => array:1 [
                    0 => array:2 [
                      "titulo" => "LaQuSo&#58; Using Formal Methods for Analysis&#44; Verification and Improvement of Safety-Critical Software"
                      "autores" => array:1 [
                        0 => array:2 [
                          "etal" => false
                          "autores" => array:2 [
                            0 => "S&#46; Smetsers"
                            1 => "M&#46; Eekelen"
                          ]
                        ]
                      ]
                    ]
                  ]
                  "host" => array:1 [
                    0 => array:1 [
                      "Revista" => array:5 [
                        "tituloSerie" => "ERCIM News"
                        "fecha" => "2008"
                        "volumen" => "75"
                        "paginaInicial" => "36"
                        "paginaFinal" => "37"
                      ]
                    ]
                  ]
                ]
              ]
            ]
            4 => array:3 [
              "identificador" => "bib0025"
              "etiqueta" => "&#91;5&#93;"
              "referencia" => array:1 [
                0 => array:2 [
                  "contribucion" => array:1 [
                    0 => array:2 [
                      "titulo" => "A Design Choices for High-Confidence Distributed Real-Time Software"
                      "autores" => array:1 [
                        0 => array:2 [
                          "etal" => false
                          "autores" => array:2 [
                            0 => "S Fischmeister"
                            1 => "Azim"
                          ]
                        ]
                      ]
                    ]
                  ]
                  "host" => array:1 [
                    0 => array:1 [
                      "Revista" => array:5 [
                        "tituloSerie" => "Leveraging Applications of Formal Methods&#44; Verification&#44; and Validation&#44; Lecture Notes in Computer Science"
                        "fecha" => "2010"
                        "volumen" => "6416"
                        "paginaInicial" => "97"
                        "paginaFinal" => "111"
                      ]
                    ]
                  ]
                ]
              ]
            ]
            5 => array:3 [
              "identificador" => "bib0030"
              "etiqueta" => "&#91;6&#93;"
              "referencia" => array:1 [
                0 => array:2 [
                  "contribucion" => array:1 [
                    0 => array:2 [
                      "titulo" => "Trustable Formal Specification for Software Certification"
                      "autores" => array:1 [
                        0 => array:2 [
                          "etal" => false
                          "autores" => array:2 [
                            0 => "D Mery"
                            1 => "N&#46;K Singh"
                          ]
                        ]
                      ]
                    ]
                  ]
                  "host" => array:1 [
                    0 => array:1 [
                      "Revista" => array:5 [
                        "tituloSerie" => "Leveraging Applications of Formal Methods&#44; Verification&#44; and Validation&#44; Lecture Notes in Computer Science"
                        "fecha" => "2010"
                        "volumen" => "6416"
                        "paginaInicial" => "312"
                        "paginaFinal" => "326"
                      ]
                    ]
                  ]
                ]
              ]
            ]
            6 => array:3 [
              "identificador" => "bib0035"
              "etiqueta" => "&#91;7&#93;"
              "referencia" => array:1 [
                0 => array:2 [
                  "contribucion" => array:1 [
                    0 => array:1 [
                      "autores" => array:1 [
                        0 => array:2 [
                          "etal" => false
                          "autores" => array:1 [
                            0 => "I&#46; Sommerville"
                          ]
                        ]
                      ]
                    ]
                  ]
                  "host" => array:1 [
                    0 => array:1 [
                      "Libro" => array:5 [
                        "edicion" => "8th"
                        "titulo" => "Software Engineering"
                        "fecha" => "2007"
                        "editorial" => "Pearson Education"
                        "editorialLocalizacion" => "China"
                      ]
                    ]
                  ]
                ]
              ]
            ]
            7 => array:3 [
              "identificador" => "bib0040"
              "etiqueta" => "&#91;8&#93;"
              "referencia" => array:1 [
                0 => array:1 [
                  "referenciaCompleta" => "S&#46;M&#46; Babamir and M&#46; Borhani&#44; &#8220;Formal Verification of Medical Monitoring Software Using Z Language&#58; A Representative Sample&#44;&#8221; Journal of Medical Systems&#44; 2011&#44; Springer&#44; DOI&#58; 10&#46;1007&#47;s10916-011-9739-5&#46;"
                ]
              ]
            ]
            8 => array:3 [
              "identificador" => "bib0045"
              "etiqueta" => "&#91;9&#93;"
              "referencia" => array:1 [
                0 => array:2 [
                  "contribucion" => array:1 [
                    0 => array:2 [
                      "titulo" => "Practical Ways of Improving Product Safety in Industry"
                      "autores" => array:1 [
                        0 => array:2 [
                          "etal" => false
                          "autores" => array:2 [
                            0 => "S&#46; Gabriele"
                            1 => "W&#46; Werner"
                          ]
                        ]
                      ]
                    ]
                  ]
                  "host" => array:1 [
                    0 => array:1 [
                      "Revista" => array:5 [
                        "tituloSerie" => "Improvements In system Safety"
                        "fecha" => "2008"
                        "numero" => "6"
                        "paginaInicial" => "177"
                        "paginaFinal" => "193"
                      ]
                    ]
                  ]
                ]
              ]
            ]
            9 => array:3 [
              "identificador" => "bib0050"
              "etiqueta" => "&#91;10&#93;"
              "referencia" => array:1 [
                0 => array:2 [
                  "contribucion" => array:1 [
                    0 => array:2 [
                      "titulo" => "Engineering Safety-and Security-Related Requirements&#58; Tutorial&#44;&#8221; in 15"
                      "autores" => array:1 [
                        0 => array:2 [
                          "etal" => false
                          "autores" => array:1 [
                            0 => "D&#46;G&#46; Firesmith"
                          ]
                        ]
                      ]
                    ]
                  ]
                  "host" => array:1 [
                    0 => array:1 [
                      "LibroEditado" => array:3 [
                        "titulo" => "IEEE International Requirements Engineering Confencee"
                        "conferencia" => "New Delhi&#44; India"
                        "serieFecha" => "2007"
                      ]
                    ]
                  ]
                ]
              ]
            ]
            10 => array:3 [
              "identificador" => "bib0055"
              "etiqueta" => "&#91;11&#93;"
              "referencia" => array:1 [
                0 => array:2 [
                  "contribucion" => array:1 [
                    0 => array:2 [
                      "titulo" => "Engineering Safety-Related Requirements for Software-Intensive Systems&#58; Tutorial"
                      "autores" => array:1 [
                        0 => array:2 [
                          "etal" => false
                          "autores" => array:1 [
                            0 => "D&#46;G&#46; Firesmith"
                          ]
                        ]
                      ]
                    ]
                  ]
                  "host" => array:1 [
                    0 => array:1 [
                      "Libro" => array:4 [
                        "titulo" => "27th International Conference on Software Engineering &#40;ICSE&#39;2005&#41;"
                        "fecha" => "2005"
                        "editorial" => "Louis"
                        "editorialLocalizacion" => "Missouri&#44; USA"
                      ]
                    ]
                  ]
                ]
              ]
            ]
            11 => array:3 [
              "identificador" => "bib0060"
              "etiqueta" => "&#91;12&#93;"
              "referencia" => array:1 [
                0 => array:2 [
                  "contribucion" => array:1 [
                    0 => array:2 [
                      "titulo" => "Risk Assessment for M42 Active Traffic Management"
                      "autores" => array:1 [
                        0 => array:2 [
                          "etal" => false
                          "autores" => array:2 [
                            0 => "S&#46; Tucker"
                            1 => "M&#46; Halbert"
                          ]
                        ]
                      ]
                    ]
                  ]
                  "host" => array:1 [
                    0 => array:1 [
                      "Revista" => array:5 [
                        "tituloSerie" => "Developments in Risk- Based Approaches to Safety"
                        "fecha" => "2006"
                        "numero" => "2"
                        "paginaInicial" => "25"
                        "paginaFinal" => "45"
                      ]
                    ]
                  ]
                ]
              ]
            ]
            12 => array:3 [
              "identificador" => "bib0065"
              "etiqueta" => "&#91;13&#93;"
              "referencia" => array:1 [
                0 => array:2 [
                  "contribucion" => array:1 [
                    0 => array:1 [
                      "autores" => array:1 [
                        0 => array:2 [
                          "etal" => false
                          "autores" => array:1 [
                            0 => "C&#46;A&#46; Ericson"
                          ]
                        ]
                      ]
                    ]
                  ]
                  "host" => array:1 [
                    0 => array:1 [
                      "Libro" => array:4 [
                        "titulo" => "Hazard analysis techniques for system safety"
                        "fecha" => "2005"
                        "editorial" => "Wiley-Interscience"
                        "editorialLocalizacion" => "Hoboken&#44; New Jersey&#44; USA"
                      ]
                    ]
                  ]
                ]
              ]
            ]
            13 => array:3 [
              "identificador" => "bib0070"
              "etiqueta" => "&#91;14&#93;"
              "referencia" => array:1 [
                0 => array:2 [
                  "contribucion" => array:1 [
                    0 => array:2 [
                      "titulo" => "An Approach to Modeling Software Safety in Safety-Critical Systems"
                      "autores" => array:1 [
                        0 => array:2 [
                          "etal" => false
                          "autores" => array:2 [
                            0 => "M&#46;B&#46; Swarup"
                            1 => "P&#46;S&#46; Ramaiah"
                          ]
                        ]
                      ]
                    ]
                  ]
                  "host" => array:1 [
                    0 => array:1 [
                      "Revista" => array:6 [
                        "tituloSerie" => "Journal of Computer Science"
                        "fecha" => "2009"
                        "volumen" => "5"
                        "numero" => "4"
                        "paginaInicial" => "311"
                        "paginaFinal" => "322"
                      ]
                    ]
                  ]
                ]
              ]
            ]
            14 => array:3 [
              "identificador" => "bib0075"
              "etiqueta" => "&#91;15&#93;"
              "referencia" => array:1 [
                0 => array:2 [
                  "contribucion" => array:1 [
                    0 => array:1 [
                      "autores" => array:1 [
                        0 => array:2 [
                          "etal" => false
                          "autores" => array:1 [
                            0 => "R&#46; Patton"
                          ]
                        ]
                      ]
                    ]
                  ]
                  "host" => array:1 [
                    0 => array:1 [
                      "Libro" => array:4 [
                        "titulo" => "Software Testing"
                        "fecha" => "2001"
                        "editorial" => "Sams"
                        "editorialLocalizacion" => "Indianapolis&#44; Indiana&#44; USA"
                      ]
                    ]
                  ]
                ]
              ]
            ]
            15 => array:3 [
              "identificador" => "bib0080"
              "etiqueta" => "&#91;16&#93;"
              "referencia" => array:1 [
                0 => array:2 [
                  "contribucion" => array:1 [
                    0 => array:2 [
                      "titulo" => "A Comprative Study of Formal Methods for Safety Critical Software in Nuclear Power Plant"
                      "autores" => array:1 [
                        0 => array:2 [
                          "etal" => false
                          "autores" => array:2 [
                            0 => "S&#46; Sohn"
                            1 => "P&#46; Seong"
                          ]
                        ]
                      ]
                    ]
                  ]
                  "host" => array:1 [
                    0 => array:1 [
                      "Revista" => array:6 [
                        "tituloSerie" => "Journal of the Korean Nuclear Society"
                        "fecha" => "2000"
                        "volumen" => "32"
                        "numero" => "6"
                        "paginaInicial" => "537"
                        "paginaFinal" => "548"
                      ]
                    ]
                  ]
                ]
              ]
            ]
            16 => array:3 [
              "identificador" => "bib0085"
              "etiqueta" => "&#91;17&#93;"
              "referencia" => array:1 [
                0 => array:2 [
                  "contribucion" => array:1 [
                    0 => array:1 [
                      "autores" => array:1 [
                        0 => array:2 [
                          "etal" => false
                          "autores" => array:1 [
                            0 => "J&#46;M&#46; Spivey"
                          ]
                        ]
                      ]
                    ]
                  ]
                  "host" => array:1 [
                    0 => array:1 [
                      "Libro" => array:5 [
                        "edicion" => "2nd"
                        "titulo" => "The Z Notation&#58; A Reference Manual"
                        "fecha" => "2001"
                        "editorial" => "Prentice Hall"
                        "editorialLocalizacion" => "Oxford&#44; UK"
                      ]
                    ]
                  ]
                ]
              ]
            ]
            17 => array:3 [
              "identificador" => "bib0090"
              "etiqueta" => "&#91;18&#93;"
              "referencia" => array:1 [
                0 => array:2 [
                  "contribucion" => array:1 [
                    0 => array:1 [
                      "autores" => array:1 [
                        0 => array:2 [
                          "colaboracion" => "National Aeronautics and Space Administration"
                          "etal" => false
                        ]
                      ]
                    ]
                  ]
                  "host" => array:1 [
                    0 => array:1 [
                      "Libro" => array:4 [
                        "titulo" => "NASA Software Safety Guidebook"
                        "fecha" => "2004"
                        "editorial" => "NASA"
                        "editorialLocalizacion" => "USA"
                      ]
                    ]
                  ]
                ]
              ]
            ]
            18 => array:3 [
              "identificador" => "bib0095"
              "etiqueta" => "&#91;19&#93;"
              "referencia" => array:1 [
                0 => array:2 [
                  "contribucion" => array:1 [
                    0 => array:1 [
                      "autores" => array:1 [
                        0 => array:2 [
                          "etal" => false
                          "autores" => array:3 [
                            0 => "J&#46;D&#46; Gahl"
                            1 => "J&#46;E&#46; DijKstra"
                            2 => "C&#46;A&#46;R&#46; Hoare"
                          ]
                        ]
                      ]
                    ]
                  ]
                  "host" => array:1 [
                    0 => array:1 [
                      "Libro" => array:4 [
                        "titulo" => "Notes on Structured Programming"
                        "fecha" => "1972"
                        "editorial" => "Academic Press London"
                        "editorialLocalizacion" => "London&#44; England"
                      ]
                    ]
                  ]
                ]
              ]
            ]
            19 => array:3 [
              "identificador" => "bib0100"
              "etiqueta" => "&#91;20&#93;"
              "referencia" => array:1 [
                0 => array:2 [
                  "contribucion" => array:1 [
                    0 => array:1 [
                      "autores" => array:1 [
                        0 => array:2 [
                          "colaboracion" => "Office of Government Commerce"
                          "etal" => false
                        ]
                      ]
                    ]
                  ]
                  "host" => array:1 [
                    0 => array:1 [
                      "Libro" => array:4 [
                        "titulo" => "Intruduction to ITIL"
                        "fecha" => "2006"
                        "editorial" => "London&#44; Britain"
                        "editorialLocalizacion" => "TSO"
                      ]
                    ]
                  ]
                ]
              ]
            ]
          ]
        ]
      ]
    ]
  ]
  "idiomaDefecto" => "en"
  "url" => "/16656423/0000001100000005/v2_201505081700/S1665642313715761/v2_201505081700/en/main.assets"
  "Apartado" => null
  "PDF" => "https://static.elsevier.es/multimedia/16656423/0000001100000005/v2_201505081700/S1665642313715761/v2_201505081700/en/main.pdf?idApp=UINPBA00004N&text.app=https://www.elsevier.es/"
  "EPUB" => "https://multimedia.elsevier.es/PublicationsMultimediaV1/item/epub/S1665642313715761?idApp=UINPBA00004N"
]

Article information

ISSN: 16656423
Original language: English

DOI:10.1016/S1665-6423(13)71576-1

The statistics are updated each day

Year/Month	Html	Pdf	Total

2024 October	23	1	24
2024 September	29	1	30
2024 August	36	2	38
2024 July	33	2	35
2024 June	24	3	27
2024 May	77	5	82
2024 April	61	8	69
2024 March	106	12	118
2024 February	110	23	133
2024 January	129	19	148
2023 December	59	13	72
2023 November	95	21	116
2023 October	133	20	153
2023 September	63	3	66
2023 August	60	9	69
2023 July	48	4	52
2023 June	38	6	44
2023 May	26	5	31
2023 April	18	4	22
2023 March	22	6	28
2023 February	23	2	25
2023 January	17	4	21
2022 December	24	2	26
2022 November	17	11	28
2022 October	35	8	43
2022 September	15	5	20
2022 August	23	7	30
2022 July	8	6	14
2022 June	24	3	27
2022 May	27	7	34
2022 April	34	7	41
2022 March	16	5	21
2022 February	24	9	33
2022 January	37	7	44
2021 December	20	6	26
2021 November	17	8	25
2021 October	18	9	27
2021 September	14	6	20
2021 August	18	7	25
2021 July	21	6	27
2021 June	16	7	23
2021 May	25	19	44
2021 April	33	14	47
2021 March	30	6	36
2021 February	24	4	28
2021 January	37	22	59
2020 December	33	11	44
2020 November	28	6	34
2020 October	12	5	17
2020 September	16	6	22
2020 August	23	14	37
2020 July	22	8	30
2020 June	22	3	25
2020 May	27	6	33
2020 April	43	8	51
2020 March	25	13	38
2020 February	9	6	15
2020 January	30	1	31
2019 December	47	5	52
2019 November	9	4	13
2019 October	5	1	6
2019 September	11	5	16
2019 August	8	6	14
2019 July	8	12	20
2019 June	26	15	41
2019 May	65	33	98
2019 April	43	20	63
2019 March	11	3	14
2019 February	9	1	10
2019 January	3	4	7
2018 December	7	2	9
2018 November	13	0	13
2018 October	8	9	17
2018 September	22	2	24
2018 August	1	3	4
2018 July	8	2	10
2018 June	4	5	9
2018 May	8	3	11
2018 April	1	3	4
2018 March	6	0	6
2018 February	3	2	5
2018 January	5	0	5
2017 December	7	0	7
2017 November	6	2	8
2017 October	10	0	10
2017 September	7	13	20
2017 August	10	1	11
2017 July	10	0	10
2017 June	18	19	37
2017 May	21	12	33
2017 April	13	3	16
2017 March	17	14	31
2017 February	11	3	14
2017 January	10	2	12
2016 December	7	1	8
2016 November	6	2	8
2016 October	13	2	15
2016 September	4	6	10
2016 July	3	2	5
2016 June	4	6	10
2016 May	3	6	9
2016 April	7	7	14
2016 March	9	8	17
2016 February	3	8	11
2016 January	5	9	14
2015 December	2	6	8
2015 November	5	7	12
2015 October	11	11	22
2015 September	9	6	15
2015 August	3	1	4
2015 July	3	2	5
2015 June	0	1	1
2015 May	1	2	3
2015 April	2	1	3

Show all

Indexed in:

Follow us:

Statistics

Indexed in:

Follow us:

Statistics

Subscribe to our newsletter