El plan de UCLM-EIIA no tiene optatividad. ESC es una asignatura finalista (no se usa como base para ninguna otra). Por tanto el único emplazamiento posible es 4º. Las prácticas se orientan a desarrollo de software por un motivo práctico, pero la metodología es aplicable a sistemas puramente hardware (mecánicos o electrónicos).
Porque el campo de la Ingeniería Aeronáutica lo necesita. Lee los periódicos.
Porque no existe ninguna implementación de Python de tiempo real estricto. Y porque C es el más simple de los lenguajes de programación utilizables para tiempo real. Otras opciones populares podrían ser Ada y C++ pero su complejidad es mucho mayor. Plantearemos estas opciones en el postgrado.
Porque es el método de modelado de sistemas reactivos más sencillo e intuitivo que existe. Otra opción es usar Redes de Petri, pero pensamos que es una mejor opción para un postgrado.
Porque es un sistema operativo de tiempo real relativamente sencillo certificado
IEC 61508,
EN 50128,
FDA 510(k),
IEC 62304,
IEC 61513,
IEC 62061,
ISO 26262,
DO 178C.
Eso implica que puede usarse para aplicaciones médicas, industriales, de automoción y aeroespaciales.
Porque es el lenguaje de especificación formal más sencillo que hemos encontrado.
Para una utilidad razonable deberíamos incluir LTL y CTL como mínimo. Nos limitamos a LTL exclusivamente para reducir la carga del estudiante. Mejor LTL que CTL porque casi todas las herramientas de model checking soportan LTL o una variante.
La inmensa mayoría de los fabricantes de sistemas de tiempo real utiliza RTA. Timed transition systems es una adición relativamente reciente a nuXmv, que no es soportada por nuSMV.
El siguiente texto introduce muy bien las razones para la inclusión de métodos formales en el Grado en Ingeniería Aeroespacial.
Los siguientes cursos de grado forman parte de programas en Ingeniería Aeroespacial o Ingeniería Aeronáutica. En modo alguno se trata de una lista exhaustiva. Se extenderá esta tabla más adelante. Nótese que Berkeley no tenía un Major en Aerospace Engineering hasta ahora y no se dispondrá de información hasta después del verano.
| Código | Nombre | Universidad |
|---|---|---|
| AERE 407 | Applied Formal Methods | Iowa State University |
| 16.332 | Formal Methods for Safe Autonomous Systems | Massachusetts Institute of Technology |
| AAE 66800 | Hybrid Systems: Theory And Analysis | Purdue University |
En otras ingenierías relacionadas también se incluyen asignaturas sobre métodos formales.
| Código | Nombre | Universidad | Grado |
|---|---|---|---|
| 15-424/624/824 | Logical Foundations of Cyber-Physical Systems | Carnegie Mellon University | Computer Science |
| 6B162002L | Advanced Software Engineering | Nanjing University of Aeronautics and Astronautics | Electrical and Computer Engineering |
| 18-341 | Logic Design and Verification | Carnegie Mellon University | Electrical and Computer Engineering |
| 19CSE441 | INTRODUCTION TO CYBER-PHYSICAL SYSTEMS | Amrita Vishwa Vidyapeetham | Computer Science and Engineering |
| ECE 659 | Digital Systems Verification | University of Tennessee, Knoxville | Electrical and Computer Engineering |
Todas las grandes compañías han investigado de una manera u otra la introducción de métodos formales, aunque aún está en un estado incipiente, más por la falta de formación de su personal que por la necesidad.
Boeing es conocida por haber utilizado métodos formales en numerosas ocasiones (el Max es otra historia). Incluso tiene colaboraciones con los creadores de nuXmv.
Airbus ha publicado un gran número de artículos en revistas especializadas sobre la aplicación de métodos formales en el desarrollo de software para aviónica. Merece la pena explorar sus propias conclusiones o la experiencia en el programa del A380. Incluso hay un video sobre la apliación de abstract interpretation y theorem proving en Airbus.
NASA integra la verificación formal como uno de los procesos de desarrollo de su Systems Engineering Handbook. Es conocido que utilizó theorem proving en el desarrollo del software del transbordador espacial.