Finalmente: IronFleet

Ver el tema anterior Ver el tema siguiente Ir abajo

Finalmente: IronFleet

Mensaje por yvory_saavedra el Dom Mayo 15, 2016 1:36 am

Microsoft anuncia el Santo Grial de la programación: el software infalible


Científicos de Microsoft anuncian un hito informático que podría tener gran relevancia para entornos de programación: la verificación automática de fiabilidad del software.
La división de Investigación y Desarrollo de Microsoft, Microsoft Research, anuncia que un grupo de sus científicos ha alcanzado un importante hito, que consiste en el desarrollo de un método que hace posible crear sistemas de software distribuido, con la capacidad de verificar y garantizar su infalibilidad.

Brian Parno, científicos de Microsoft participante del proyecto escribió:“La verificación de software ha sido un Santo Grial para la informática durante 40 o 50 años”


IronFleet


El proyecto es denominado IronFleet, y está concebido para sistemas multiplataforma, susceptibles de errores cuando los desarrolladores descuidan la compleja forma en que los distintos sistemas operativos interactúan entre sí.

Como ejemplo de lo anterior, los científicos mencionan un banco con un sistema distribuido que permite a los numerosos servidores de la entidad coordinarse entre sí. Un sistema bancario no admite margen de error, debido a que la transacción de un cliente puede ingresar mediante un servidor, mientras que otra transacción hecha posteriormente puede ser recibida mediante otro servidor. Para el banco es imprescindible saber que ambas transacciones han sido registradas de manera consistente.

Los científicos de Microsoft explican que el mundo actual dista mucho de estar en una situación donde, de manera realista, sea posible desarrollar programas grandes y complejos, como por ejemplo sistemas operativos, cuya infalibilidad pueda ser garantizada.

Según Microsoft Research, aunque el desarrollo de código infalible será costoso, de todas formas se trata de un proyecto viable para sistemas donde las garantías de funcionamiento son fundamentales, como por ejemplo, el citado sistema bancario.

Parni escribió:Al comienzo nos concentraremos en porciones pequeñas, aunque de rango crítico, de software, donde la seguridad y la confiabilidad sean imprescindibles

Por su parte, su colega Jay Lorch agrega que el grupo de investigadores trabaja únicamente con sistemas que interactúan con otros. La razón de esto sería lo imprevisibles que son los seres humanos.

Lorch escribió:Las personas somos muy complejas, razón por la que es aventurado siquiera intentar especificar la forma en que un ser humano interactúa con un programa informático



Velocidad multiplicada



Según otro científico participante en la iniciativa, Chris Hawblitzel, el proyecto ha sido posible mediante la combinación de hardware y software mejorado, como asimismo algoritmos más veloces, desarrollados por Microsoft Research. Hawblitzel agrega que los nuevos sistemas permiten acercarse aún más al momento en que los desarrolladores podrán comenzar a escribir código infalible. “Si tenemos éxito, la gente dentro de 15 años podrá mirar el retrospectiva y decir “es increíble que antes escribían código de esa forma”


El equipo de científicos participantes en el proyecto IronFleet incluyen, (desde arriba, izquierda) a Chris Hawblitzel, Brian Zill, Jon Howell, Michael Lowell Roberts, Bryan Parno, Manos Kapritsos, Jay Lorch y Srinath Setty (Fotografía © Microsoft Research)


Los sistemas distribuidos son conocidos por albergar a errores sutiles. La verificación puede, en principio, eliminar estos errores a priori, pero la verificación ha sido históricamente difícil de aplicar a escala-programa completo, y mucho menos escala-sistema distribuido.

IronFleet organiza la implementación de un sistema distribuido y lo prueba en capas (Figura) para evitar la mezcla de protocolos distribuidos sutiles con la complejidad de la implementación. En la parte superior (X3.1), escribimos una especificación simple para el comportamiento del sistema. A continuación, escribimos una capa de protocolo distribuido abstracta (X3.2) y el uso de técnicas de estilo TLA para demostrar que refina la capa de especificaciones (X3.3). Entonces escribimos una capa de aplicación imperativa para ejecutarse en cada host (X3.4) y demostrar que, a pesar de las complejidades introducidas al escribir código de sistemas reales, la aplicación refina correctamente la capa de protocolo (x3.5).



Para evitar el razonamiento complejo sobre la ejecución intercalada de operaciones de bajo nivel en varios hosts, utiliza una estrategia de contención de concurrencia: las pruebas anteriores asumen que cada paso de implementación realiza un paso de protocolo atómica. Ya que la ejecución de la aplicación real no es atómica, utilizamos un argumento para demostrar la reducción de una prueba asumiendo que la atomicidad es igualmente válida como prueba para el sistema real. Este argumento requiere una propiedad verificado la mecánica de la aplicación, así como un pequeño papel a prueba de sólo de las implicaciones de la propiedad.

yvory_saavedra

Mensajes : 12
Fecha de inscripción : 02/02/2016

Ver perfil de usuario

Volver arriba Ir abajo

Re: Finalmente: IronFleet

Mensaje por Geovana el Dom Mayo 15, 2016 3:38 pm

Microsoft simplificará el trabajo a los desarrolladores con Xamarin

Para lograrlo sin duda el desplazamiento mas considerable fue la compra de Xamarin, el santo grial de la programación multiplataforma, con el que se podrán adaptar app de alguna plataforma a otra con tan solo pulsar el botón rojo de port-it. Por el momento, su aterrizaje ha sido por filtración, haciéndose hueco poco a poco, pero si esto funciona aspira a convertirse en el Líder.

Quien se está beneficiando es el usuario, que va a poder eligir su terminal con mayor normalidad en cuanto a las aplicaciones a las que va a poder acceder.

Xamarin se ha encargado de desarrollar y perfeccionar una suite de herramientas con las que se puede programar el código una vez, y luego ser exportado a otros sistemas.

Los fundadores de Xamarin, Miguel de Icaza and Nat Friedman, permanecerán en Microsoft y dicen: "Creamos Xamarin porque sabíamos que tenía que haber una mejor manera de construir aplicaciones móviles. Somos desarrolladores, así que sabemos lo que quieren los desarrolladores: un lenguaje moderno de programación, herramientas de gran alcance, un flujo de trabajo eficiente y agradable y el poder de crear las mejores experiencias de usuario. Nuestra misión es que desarrollar grandes aplicaciones móviles sea algo rápido, fácil y divertido."

fuente [http://www.vbote.com/vbote-solutions-academy-blog/295-por-qu%C3%A9-microsoft-ha-comprado-xamarin,-suite-de-desarrollo-de-apps-m%C3%B3viles.html]

Geovana

Mensajes : 6
Fecha de inscripción : 02/02/2016

Ver perfil de usuario

Volver arriba Ir abajo

Re: Finalmente: IronFleet

Mensaje por Henry Quispe Acarapi el Dom Mayo 15, 2016 10:47 pm

SISTEMAS DE VERIFICACION


El reciente aumento en el poder de la verificación del software tiene varios grupos de investigación lo utilizan para probar la corrección de la totalidad de las implementaciones de sistemas. SEL4 es un microkernel escrito en C, con la corrección funcional completa probada usando el demostrador de teoremas Isabelle / HOL. mCertiKOShyp es un pequeño hipervisor verificado, cuya verificación el asistente de demostración interactiva Coq pone un fuerte énfasis en la modularidad y la abstracción. Expressos utiliza Dafny a la cordura a comprobar un gestor de políticas para un microkernel. nuestra Ironclad proyecto muestra cómo verificar por completo la seguridad de los servicios sensibles todo el camino hasta el montaje. Hierro- Fleet difiere mediante la verificación de una implementación distribuida en vez que el código que se ejecuta en una sola máquina, y mediante la verificación liveness, así como la seguridad, propiedades.

La metodología IronFleet divide un sistema en capas específicas para hacer la verificación de las implementaciones prácticas de sistemas distribuidos factible. La especificación de alto nivel da la más simple Descripción del comportamiento del sistema. El protocolo ofertas de capa exclusivamente con el diseño del protocolo distribuido; nos conectamos a la especificación mediante la verificación de estilo TLA. A la capa de aplicación, las razones programador sobre una programa de un solo host sin tener que preocuparse por la concurrencia.
Reducción y refinamiento atan estos de forma individual factible componentes en una metodología que se adapta para implementaciones concretas. Esta metodología admite implementaciones convencionalmente estructurados capaces de procesar hasta 18.200 peticiones / segundo (28.800) y IronRSL peticiones / segundo (IronKV), el rendimiento de la competencia con verificado implementaciones de referencia.

Henry Quispe Acarapi

Mensajes : 10
Fecha de inscripción : 04/02/2016

Ver perfil de usuario

Volver arriba Ir abajo

Re: Finalmente: IronFleet

Mensaje por Contenido patrocinado


Contenido patrocinado


Volver arriba Ir abajo

Ver el tema anterior Ver el tema siguiente Volver arriba


 
Permisos de este foro:
No puedes responder a temas en este foro.