Hispanopedia Wiki
Articulo de referencia

ProCoS

[[Duration Calculus]]"},"location":{"wt":"[[Europe]]"},"country":{"wt":""},"owner":{"wt":""},"founder":{"wt":""},"key_people":{"wt":"[[Tony Hoare]] [[Dines Bjørner]] [[Hans Lang...

Hispanopedia WikiContenido en espanolLectura gratuita

ProCoS (" Sistemas demostrablemente correctos ") fue una iniciativa europea de ESPRIT que consistió en dos proyectos de investigación colaborativa en ciencias de la computación y un Grupo de Trabajo , con financiación adicional asociada para la coordinación internacional, que comenzó en 1989 y finalizó en 1997.

Los proyectos tenían como objetivo conectar sistemas basados ​​en computadoras de manera formal en diferentes niveles de abstracción , incluyendo requisitos , especificaciones , programas , a través de la compilación , al código máquina , e incluso directamente al hardware descrito por netlists , basado en el lenguaje de programación occam y el procesador Transputer . [ 1 ] Un resultado de investigación importante del proyecto fue Duration Calculus por Zhou Chaochen , Tony Hoare y Anders P. Ravn . Un resultado posterior del proyecto fue Unifying Theories of Programming (UTP) por Tony Hoare y He Jifeng .

Proyectos y subvenciones

Se financiaron los siguientes proyectos y colaboraciones asociadas: [ 1 ]

  • Proyecto ESPRIT ProCoS BRA (Acción de Investigación Básica) (n.º 3104, 1989–1992) [ 2 ] [ 3 ]
  • Proyecto ESPRIT ProCoS II (nº 7071, 1992-1995) [ 4 ]
  • Grupo de trabajo ESPRIT ProCoS-WG (n.º 8694, 1994–1997) [ 5 ] [ 6 ]
  • Proyecto de codiseño de hardware y software con corrección demostrable del EPSRC del Reino Unido (1993-1996)
  • ESPRIT/ NSF ProCoS-US (EC-US027, 1993–1997) Beca de viaje europea/ estadounidense sobre compilación de hardware demostrablemente correcta.
  • Beca de viaje ESPRIT KIT (Mantente en contacto) (1993–1996) con Zhou Chaochen , UNU-IIST ( Macao )
  • Beca de viaje ESPRIT PROCORSYS KIT (Keep in Touch) (KIT 142, 1994–1997) con Augusto Sampaio , Departamento de Informática, Universidade Federal de Pernambuco ( Brasil )
  • Beca de investigación visitante del EPSRC del Reino Unido (1996-1997) para estudiar sistemas de tiempo real con corrección demostrable para Michael Schenke, Universidad de Oldenburg ( Alemania ).

Fogonadura

Los principales socios del proyecto, entre otros, fueron: [ 1 ]

En marzo de 2015 se celebró una reunión de dos días en la oficina de BCS en Londres. [ 10 ]

Referencias

  1. 1 2 3 Bowen, Jonathan P. ; Fränzle, Martin; Olderog, Ernst-Rüdiger ; Bjørner, Dines ; Hansen, Michael R.; Langmaack, Hans ; Liu, Zhiming ; Martin, Ursula (2026). "Experiencias de los proyectos europeos ProCoS: sistemas demostrablemente correctos" . Aspectos formales de la computación . 38. doi : 10.1145 /3803555 .
  2. ↑ «PROCOS – Convenio de subvención ID: 3104» . CORDIS . Unión Europea: Comisión Europea . 19 de agosto de 1994 . Consultado el 28 de abril de 2026 .
  3. ↑ Bjørner, D. (2017). "ProCoS: Cómo empezó todo – visto desde Dinamarca". En Hinchey, M .; Bowen, JP ; Olderog, ER. (eds.). Provably Correct Systems . NASA Monographs in Systems and Software Engineering. Cham: Springer . pp. 3–5 . doi : 10.1007/978-3-319-48628-4_1 . 
  4. ↑ «PROCOS II – Convenio de subvención ID: 7071» . CORDIS . Unión Europea: Comisión Europea . 17 de junio de 1994 . Consultado el 28 de abril de 2026 .
  5. ↑ «PROCOS – Convenio de subvención ID: 8694» . CORDIS . Unión Europea: Comisión Europea . 21 de junio de 1994 . Consultado el 28 de abril de 2026 .
  6. 1 2 Bowen, Jonathan ; Hoare, CAR ; Langmaack, Hans ; Olderog, Ernst-Rüdiger ; Ravn, Anders P. (1998). "Informe final del grupo de trabajo ProCoS-WG: Grupo de trabajo ESPRIT 8694" (PDF) . Boletín de la Asociación Europea de Ciencias de la Computación Teórica . 64 : 63–72 . Recuperado el 26 de abril de 2026 .
  7. ↑ Bjørner, Cena . "ProCoS: sistemas demostrablemente correctos" . Órbita . Dinamarca: DTU . Consultado el 26 de abril de 2026 .
  8. ↑ Langmaack, H. (1997). "El enfoque ProCoS para sistemas correctos". Sistemas en tiempo real . 13 : 253–275 . doi : 10.1023/A:1007963427189 .
  9. ↑ Olderog, Ernst-Rüdiger . "ProCoS: Provably Correct Systems" . Alemania: Universidad de Oldenburg . Consultado el 26 de abril de 2026 .
  10. ↑ Hinchey, M.; Bowen , JP ; Olderog, ER. , eds. (2017). Provably Correct Systems . NASA Monographs in Systems and Software Engineering. Cham: Springer . doi : 10.1007/978-3-319-48628-4 . ISBN 978-3-319-48627-7.
Lecturas relacionadas
6 articulos
Ciencias de la ComputaciónCiencias de la ComputaciónÁreas fundamentales de la informática La informática es el estudio de la computación , la información y la automatización . [1] [2] [3] La informát...Grupo de trabajoGrupo de trabajoGrupo de trabajo de la Cámara de Representantes de Estados Unidos sobre adicciones ( 2019 ) Un grupo de trabajo es un grupo de expertos que trabaja...[icono]Métodos formalesEn informática , los métodos formales son técnicas matemáticamente rigurosas para la especificación , desarrollo, análisis y verificación de sistem...Abstracción (informática)Abstracción (informática)En ingeniería de software y ciencias de la computación , la abstracción es el proceso de generalizar detalles concretos , [1] como atributos , alej...Ingeniería de requisitosEn el modelo de cascada , [ 1 ] la ingeniería de requisitos se presenta como la primera fase del proceso de desarrollo de software. Los métodos de ...Especificación formalEn informática , las especificaciones formales son técnicas basadas en matemáticas cuyo propósito es ayudar con la implementación de sistemas y sof...