Sí. Hay toda una rama de la informática, llamada Métodos formales, cuyo objetivo es hacerlo.
La idea básica es bastante simple de explicar.
Tome un sistema, cualquier sistema. Podría ser una planta industrial, un avión o una embarcación de tendido de tuberías submarinas. También podría ser una pieza de software, una CPU o una red de comunicación.
- ¿Qué herramienta puedo usar para encontrar si mi computadora está infectada?
- Cómo evitar que mi laptop HP I3 se ralentice
- ¿Cuál es la mejor computadora portátil para programador en 2016? Por favor responda lo antes posible bajo rs.45000
- Arquitectura de la computadora: ¿Cómo se usan los transistores multimillonarios dentro de una CPU moderna?
- ¿Una almohadilla de enfriamiento de la computadora portátil enfría la computadora portátil al soplar aire en su base o simplemente actúa como un escape, extrayendo el aire de la base a través de ella?
Un modelo del sistema está escrito por humanos en un lenguaje formal, cuya sintaxis es precisa y no ambigua. El modelo describe completamente el sistema con todas sus propiedades.
Usando el mismo lenguaje, es posible escribir propiedades que describan comportamientos “buenos” y “malos” del sistema.
Una vez que todo esto se ha hecho, se ejecuta a través de un tipo especial de software, llamado verificador de modelos . Utilizando algoritmos complejos y propiedades lógicas, el verificador de modelos verifica que todas las condiciones “buenas” se cumplan y que todas las condiciones “malas” nunca sucedan. En todos los casos posibles.
Esto es exactamente “resolver problemas críticos”, excepto que se hace antes de que sucedan. Se realiza incluso antes de que se construya el sistema .
Esto es lo que Intel y otros fabricantes de CPU hacen actualmente. En lugar de construir un nuevo procesador (que requiere la creación de una línea de conexión) y probarlo, primero escriben un modelo y hacen que una de sus grandes supercomputadoras verifique su bondad utilizando técnicas de verificación de modelos.
