Técnicas de Descripción Formal - Historial de revisiones

Carlos idict: Texto reemplazado: «
» por «»

2019-09-04T16:44:26Z

Texto reemplazado: «<div align="justify">» por «»

Enrryjccmg: /* Características */

2011-06-28T13:59:51Z

‎Características

Enrryjccmg: /* Características */

2011-06-28T13:57:57Z

‎Características

Linnet1103ad jc.hlg: /* Referencias */

2011-06-13T15:47:10Z

‎Referencias

Linnet1103ad jc.hlg en 15:37 13 jun 2011

2011-06-13T15:37:38Z

Arian.Perez jc en 18:44 26 may 2011

2011-05-26T18:44:25Z

Maria ciget.cienfuegos en 14:30 23 may 2011

2011-05-23T14:30:31Z

Gloria ciget.hol en 15:39 6 may 2011

2011-05-06T15:39:05Z

Linnet1103ad jc.hlg: Página creada con '{{Materia}} == Técnicas de Descripción Formal
== Los métodos de especificación formal, son métodos formales dedicados a escribir especificaciones de sistemas. La may...'

2011-05-06T13:26:27Z

Página creada con '{{Materia}} == Técnicas de Descripción Formal == Los métodos de especificación formal, son métodos formales dedicados a escribir especificaciones de sistemas. La may...'

Página nueva

{{Materia}}

== Técnicas de Descripción Formal ==

Los métodos de especificación formal, son métodos formales dedicados a escribir especificaciones de sistemas. La mayor parte de los métodos de especificación formal son notaciones que permiten especificar y razonar sobre el comportamiento de sistemas. Esta característica hace necesaria la experiencia y adecuada formación del equipo de desarrollo para trabajar con abstracciones y modelos de sistemas.[DUQUE 2000] Una especificación formal es una expresión matemática que contiene la descripción de un sistema. Una característica deseable, y en algunos casos necesaria en la especificación de normas, es que la especificación sea independiente de la implementación; es decir, los detalles de implementación deben incorporarse en fases posteriores. [MUÑOZ 2008] En la actualidad, existe un amplio consenso en considerar las técnicas de descripción formal , como una forma adecuada de describir el comportamiento de sistemas reactivos de procesamiento de la información. Las principales mejoras que se persiguen con el empleo de las TDF son: corrección del sistema construido respecto a una especificación formal; mejora de [[Estándares_y_Modelos_Internacionales_para_la_calidad_del_software|la calidad ]]del sistema (entendiendo calidad como el grado de cumplimiento de los requisitos y expectativas planteadas); y aumento de la productividad. Las características deseables de una TDF dependen de la fase del proceso de desarrollo en la que ésta se aplique [DUQUE 2000]: En la fase inicial, de captura y especificación de requisitos, es preferible obtener una especificación flexible del sistema en función de sus propiedades más importantes. En la fase de diseño de la arquitectura es necesario poder describir los componentes del sistema, su interfaz y como interactúan entre ellos. Es decir, es necesario poder expresar la estructura del sistema especificado. En la fase de implementación los componentes tienen que describirse de forma que su comportamiento pueda ser generado por máquinas, y por tanto, es necesario utilizar un lenguaje de programación. El proceso de traducción de un lenguaje de especificación a un lenguaje de implementación se puede automatizar en gran medida. Por tanto, si se emplean TDF, podemos decir que esta fase es semiautomática. 

== Verificación Formal ==

Las TDF contribuyen a reducir el riesgo inherente a la fase de captura y especificación de requisitos del sistema. No obstante, es importante ser consciente de que una especificación de un sistema escrita en una notación formal puede contener también errores. Para aumentar la confianza del diseñador en la corrección del método es preciso realizar operaciones de verificación sobre la especificación. Muchas veces esta verificación se realiza de manera informal a través de inspecciones y reuniones de revisión. Sin embargo, la base matemática de los métodos de especificación formal posibilita la verificación formal en dos aspectos: verificación formal de propiedades formuladas sobre la especificación, y verificación formal de que la implementación satisface la especificación.[DUQUE 2000] Una de las más importantes motivaciones que impulsó el desarrollo de las TDF fue la posibilidad de realizar una verificación formal del sistema obtenido. No obstante, es en este último punto donde surgen más controversias sobre la utilidad de las mismas. Por una parte, la experiencia ha demostrado que la verificación formal de grandes especificaciones es, en muchos casos, inviable por el alto coste de recursos que es necesario invertir. Por lo que entonces es necesario limitar o concentrar las verificaciones a partes del sistema que por su naturaleza se consideren más críticas. Un método alternativo [DUQUE 2000] a la verificación formal citada –verificación formal de que la implementación satisface la especificación-, lo constituye un proceso de refinamiento iterativo donde la especificación formal de un sistema se obtiene tras la aplicación sucesiva de un conjunto de simples refinamientos o transformaciones aplicadas a una especificación inicial del sistema con un elevado nivel de abstracción. Cada una de las fases de este proceso toma como entrada la especificación resultante del refinamiento anterior y produce como salida otra especificación con mayor cantidad de detalles de implementación. Éste proceso continúa hasta que se dispone de una especificación con el nivel de detalle suficiente como para poder traducirla a un lenguaje de programación convencional. Las especificaciones de entrada y salida de un refinamiento se pueden relacionar mediante relaciones de equivalencia o de orden. Las ventajas, a priori, de este método es que las verificaciones que se hacen son mucho más simples. 

== Referencias ==

DUQUE, J. G. Especificación, verificación y mantenimiento de requisitos funcionales con técnicas de descripción formal. España, Universidad de Vigo, Departamento de Tecnologías de las Comunicaciones, ETSI de Telecomunicación, 2000. p.

MUÑOZ, C. “Métodos Formales, por ejemplo” Computer Science Laboratory, SRI International. En sitio: “NIA: National Institute of Aerospace” Publicado: 1998. , 1998. [Disponible en: Disponible en: <http://www.csl.sri.com/users/munoz/Papers/mfhtml/mfhtml.html > 

 

== Categoría ==

 

[[Category:Metodologías_de_desarrollo_de_software]]

@@ Línea 5: / Línea 5: @@
 |concepto=
 }}
-<div align="justify">
 ''' Métodos de especificación formal'''. Son métodos formales dedicados a  escribir especificaciones de sistemas. La mayor parte de los métodos de  especificación formal son notaciones que permiten especificar y razonar  sobre el comportamiento de sistemas.

@@ Línea 10: / Línea 10: @@
 == Características <br> ==
-Una especificación formal es una expresión matemática que contiene la [[Descripció|ndescripción]] de un sistema. Una característica deseable, y en algunos casos necesaria en la especificación de normas, es que la especificación sea independiente de la implementación; es decir, los detalles de implementación deben incorporarse en fases posteriores. [MUÑOZ 2008]<br>En la actualidad, existe un amplio consenso en considerar las técnicas de descripción formal , como una forma adecuada de describir el comportamiento de sistemas reactivos de procesamiento de la información. Las principales mejoras que se persiguen con el empleo de las TDF son: corrección del sistema construido respecto a una especificación formal; mejora de [[Estándares_y_Modelos_Internacionales_para_la_calidad_del_software|la calidad ]]del sistema (entendiendo calidad como el grado de cumplimiento de los requisitos y expectativas planteadas); y aumento de la productividad. <br>Las características deseables de una TDF dependen de la fase del proceso de desarrollo en la que ésta se aplique [DUQUE 2000]:<br>En la fase inicial, de captura y especificación de requisitos, es preferible obtener una especificación flexible del sistema en función de sus propiedades más importantes.<br>En la fase de diseño de la arquitectura es necesario poder describir los componentes del sistema, su interfaz y como interactúan entre ellos. Es decir, es necesario poder expresar la estructura del sistema especificado.<br>En la fase de implementación los componentes tienen que describirse de forma que su comportamiento pueda ser generado por máquinas, y por tanto, es necesario utilizar un lenguaje de programación. El proceso de traducción de un lenguaje de especificación a un lenguaje de implementación se puede automatizar en gran medida. Por tanto, si se emplean TDF, podemos decir que esta fase es semiautomática.<br><br>
+Una especificación formal es una expresión matemática que contiene la [[Descripción|descripción]] de un sistema. Una característica deseable, y en algunos casos necesaria en la especificación de normas, es que la especificación sea independiente de la implementación; es decir, los detalles de implementación deben incorporarse en fases posteriores. [MUÑOZ 2008]<br>En la actualidad, existe un amplio consenso en considerar las técnicas de descripción formal , como una forma adecuada de describir el comportamiento de sistemas reactivos de procesamiento de la información. Las principales mejoras que se persiguen con el empleo de las TDF son: corrección del sistema construido respecto a una especificación formal; mejora de [[Estándares_y_Modelos_Internacionales_para_la_calidad_del_software|la calidad ]]del sistema (entendiendo calidad como el grado de cumplimiento de los requisitos y expectativas planteadas); y aumento de la productividad. <br>Las características deseables de una TDF dependen de la fase del proceso de desarrollo en la que ésta se aplique [DUQUE 2000]:<br>En la fase inicial, de captura y especificación de requisitos, es preferible obtener una especificación flexible del sistema en función de sus propiedades más importantes.<br>En la fase de diseño de la arquitectura es necesario poder describir los componentes del sistema, su interfaz y como interactúan entre ellos. Es decir, es necesario poder expresar la estructura del sistema especificado.<br>En la fase de implementación los componentes tienen que describirse de forma que su comportamiento pueda ser generado por máquinas, y por tanto, es necesario utilizar un lenguaje de programación. El proceso de traducción de un lenguaje de especificación a un lenguaje de implementación se puede automatizar en gran medida. Por tanto, si se emplean TDF, podemos decir que esta fase es semiautomática.<br><br>
 == Verificación Formal<br> ==

@@ Línea 10: / Línea 10: @@
 == Características <br> ==
-Una especificación formal es una expresión matemática que contiene la descripción de un sistema. Una característica deseable, y en algunos casos necesaria en la especificación de normas, es que la especificación sea independiente de la implementación; es decir, los detalles de implementación deben incorporarse en fases posteriores. [MUÑOZ 2008]<br>En la actualidad, existe un amplio consenso en considerar las técnicas de descripción formal , como una forma adecuada de describir el comportamiento de sistemas reactivos de procesamiento de la información. Las principales mejoras que se persiguen con el empleo de las TDF son: corrección del sistema construido respecto a una especificación formal; mejora de [[Estándares_y_Modelos_Internacionales_para_la_calidad_del_software|la calidad ]]del sistema (entendiendo calidad como el grado de cumplimiento de los requisitos y expectativas planteadas); y aumento de la productividad. <br>Las características deseables de una TDF dependen de la fase del proceso de desarrollo en la que ésta se aplique [DUQUE 2000]:<br>En la fase inicial, de captura y especificación de requisitos, es preferible obtener una especificación flexible del sistema en función de sus propiedades más importantes.<br>En la fase de diseño de la arquitectura es necesario poder describir los componentes del sistema, su interfaz y como interactúan entre ellos. Es decir, es necesario poder expresar la estructura del sistema especificado.<br>En la fase de implementación los componentes tienen que describirse de forma que su comportamiento pueda ser generado por máquinas, y por tanto, es necesario utilizar un lenguaje de programación. El proceso de traducción de un lenguaje de especificación a un lenguaje de implementación se puede automatizar en gran medida. Por tanto, si se emplean TDF, podemos decir que esta fase es semiautomática.<br><br>
+Una especificación formal es una expresión matemática que contiene la [[Descripció|ndescripción]] de un sistema. Una característica deseable, y en algunos casos necesaria en la especificación de normas, es que la especificación sea independiente de la implementación; es decir, los detalles de implementación deben incorporarse en fases posteriores. [MUÑOZ 2008]<br>En la actualidad, existe un amplio consenso en considerar las técnicas de descripción formal , como una forma adecuada de describir el comportamiento de sistemas reactivos de procesamiento de la información. Las principales mejoras que se persiguen con el empleo de las TDF son: corrección del sistema construido respecto a una especificación formal; mejora de [[Estándares_y_Modelos_Internacionales_para_la_calidad_del_software|la calidad ]]del sistema (entendiendo calidad como el grado de cumplimiento de los requisitos y expectativas planteadas); y aumento de la productividad. <br>Las características deseables de una TDF dependen de la fase del proceso de desarrollo en la que ésta se aplique [DUQUE 2000]:<br>En la fase inicial, de captura y especificación de requisitos, es preferible obtener una especificación flexible del sistema en función de sus propiedades más importantes.<br>En la fase de diseño de la arquitectura es necesario poder describir los componentes del sistema, su interfaz y como interactúan entre ellos. Es decir, es necesario poder expresar la estructura del sistema especificado.<br>En la fase de implementación los componentes tienen que describirse de forma que su comportamiento pueda ser generado por máquinas, y por tanto, es necesario utilizar un lenguaje de programación. El proceso de traducción de un lenguaje de especificación a un lenguaje de implementación se puede automatizar en gran medida. Por tanto, si se emplean TDF, podemos decir que esta fase es semiautomática.<br><br>
 == Verificación Formal<br> ==

@@ Línea 18: / Línea 18: @@
 == Referencias<br> ==
-DUQUE, J. G. Especificación, verificación y mantenimiento de requisitos funcionales con técnicas de descripción formal. España, Universidad de Vigo, Departamento de Tecnologías de las Comunicaciones, ETSI de Telecomunicación, 2000. p.
+*DUQUE, J. G. Especificación, verificación y mantenimiento de requisitos funcionales con técnicas de descripción formal. España, Universidad de Vigo, Departamento de Tecnologías de las Comunicaciones, ETSI de Telecomunicación, 2000. p.
-MUÑOZ, C. “Métodos Formales, por ejemplo” Computer Science Laboratory, SRI International. En sitio: “NIA: National Institute of Aerospace”<br>Publicado: 1998. , 1998. [Disponible en: Disponible en:<br>&lt;http://www.csl.sri.com/users/munoz/Papers/mfhtml/mfhtml.html &gt; <br><br>
+*MUÑOZ, C. “Métodos Formales, por ejemplo” Computer Science Laboratory, SRI International. En sitio: “NIA: National Institute of Aerospace”<br>Publicado: 1998. , 1998. [Disponible en: Disponible en:<br>&lt;http://www.csl.sri.com/users/munoz/Papers/mfhtml/mfhtml.html &gt; <br><br>
 </div>
 [[Category:Metodologías_de_desarrollo_de_software]]

@@ Línea 1: / Línea 1: @@
-{{Normalizar}}
+{{Definición
-== Técnicas de Descripción Formal <br> ==
+== Características <br> ==
-Los métodos de especificación formal, son métodos formales dedicados a escribir especificaciones de sistemas. La mayor parte de los métodos de especificación formal son notaciones que permiten especificar y razonar sobre el comportamiento de sistemas. Esta característica hace necesaria la experiencia y adecuada formación del equipo de desarrollo para trabajar con abstracciones y modelos de sistemas.[DUQUE 2000]<br>Una especificación formal es una expresión matemática que contiene la descripción de un sistema. Una característica deseable, y en algunos casos necesaria en la especificación de normas, es que la especificación sea independiente de la implementación; es decir, los detalles de implementación deben incorporarse en fases posteriores. [MUÑOZ 2008]<br>En la actualidad, existe un amplio consenso en considerar las técnicas de descripción formal , como una forma adecuada de describir el comportamiento de sistemas reactivos de procesamiento de la información. Las principales mejoras que se persiguen con el empleo de las TDF son: corrección del sistema construido respecto a una especificación formal; mejora de [[Estándares_y_Modelos_Internacionales_para_la_calidad_del_software|la calidad ]]del sistema (entendiendo calidad como el grado de cumplimiento de los requisitos y expectativas planteadas); y aumento de la productividad. <br>Las características deseables de una TDF dependen de la fase del proceso de desarrollo en la que ésta se aplique [DUQUE 2000]:<br>En la fase inicial, de captura y especificación de requisitos, es preferible obtener una especificación flexible del sistema en función de sus propiedades más importantes.<br>En la fase de diseño de la arquitectura es necesario poder describir los componentes del sistema, su interfaz y como interactúan entre ellos. Es decir, es necesario poder expresar la estructura del sistema especificado.<br>En la fase de implementación los componentes tienen que describirse de forma que su comportamiento pueda ser generado por máquinas, y por tanto, es necesario utilizar un lenguaje de programación. El proceso de traducción de un lenguaje de especificación a un lenguaje de implementación se puede automatizar en gran medida. Por tanto, si se emplean TDF, podemos decir que esta fase es semiautomática.<br><br>
+Una especificación formal es una expresión matemática que contiene la descripción de un sistema. Una característica deseable, y en algunos casos necesaria en la especificación de normas, es que la especificación sea independiente de la implementación; es decir, los detalles de implementación deben incorporarse en fases posteriores. [MUÑOZ 2008]<br>En la actualidad, existe un amplio consenso en considerar las técnicas de descripción formal , como una forma adecuada de describir el comportamiento de sistemas reactivos de procesamiento de la información. Las principales mejoras que se persiguen con el empleo de las TDF son: corrección del sistema construido respecto a una especificación formal; mejora de [[Estándares_y_Modelos_Internacionales_para_la_calidad_del_software|la calidad ]]del sistema (entendiendo calidad como el grado de cumplimiento de los requisitos y expectativas planteadas); y aumento de la productividad. <br>Las características deseables de una TDF dependen de la fase del proceso de desarrollo en la que ésta se aplique [DUQUE 2000]:<br>En la fase inicial, de captura y especificación de requisitos, es preferible obtener una especificación flexible del sistema en función de sus propiedades más importantes.<br>En la fase de diseño de la arquitectura es necesario poder describir los componentes del sistema, su interfaz y como interactúan entre ellos. Es decir, es necesario poder expresar la estructura del sistema especificado.<br>En la fase de implementación los componentes tienen que describirse de forma que su comportamiento pueda ser generado por máquinas, y por tanto, es necesario utilizar un lenguaje de programación. El proceso de traducción de un lenguaje de especificación a un lenguaje de implementación se puede automatizar en gran medida. Por tanto, si se emplean TDF, podemos decir que esta fase es semiautomática.<br><br>
 == Verificación Formal<br> ==
@@ Línea 14: / Línea 21: @@
 MUÑOZ, C. “Métodos Formales, por ejemplo” Computer Science Laboratory, SRI International. En sitio: “NIA: National Institute of Aerospace”<br>Publicado: 1998. , 1998. [Disponible en: Disponible en:<br>&lt;http://www.csl.sri.com/users/munoz/Papers/mfhtml/mfhtml.html &gt; <br><br>
+</div>
 [[Category:Metodologías_de_desarrollo_de_software]]

← Revisión anterior		Revisión del 18:44 26 may 2011
Línea 1:		Línea 1:
−	~~{{ Mejorar\|motivo=Falta plantilla, resumen introductorio}}~~ {{Normalizar~~\|motivo=Separación entre párrafos, hipervincular~~}}	+	{{Normalizar}}

	== Técnicas de Descripción Formal <br> ==		== Técnicas de Descripción Formal <br> ==

← Revisión anterior		Revisión del 15:39 6 may 2011
Línea 1:		Línea 1:
−	{{Materia}}	+	{{ Mejorar}} {{Normalizar}}
		+	{{Materia\|nombre=\|imagen=\|campo a que pertenece=\|principales exponentes=}}

	== Técnicas de Descripción Formal <br> ==		== Técnicas de Descripción Formal <br> ==

Técnicas de Descripción Formal - Historial de revisiones

Carlos idict: Texto reemplazado: «» por «»

Enrryjccmg: /* Características */

Enrryjccmg: /* Características */

Linnet1103ad jc.hlg: /* Referencias */

Linnet1103ad jc.hlg en 15:37 13 jun 2011

Arian.Perez jc en 18:44 26 may 2011

Maria ciget.cienfuegos en 14:30 23 may 2011

Gloria ciget.hol en 15:39 6 may 2011

Linnet1103ad jc.hlg: Página creada con '{{Materia}} == Técnicas de Descripción Formal == Los métodos de especificación formal, son métodos formales dedicados a escribir especificaciones de sistemas. La may...'

Carlos idict: Texto reemplazado: «
» por «»

Linnet1103ad jc.hlg: Página creada con '{{Materia}} == Técnicas de Descripción Formal
== Los métodos de especificación formal, son métodos formales dedicados a escribir especificaciones de sistemas. La may...'