Utilizaremos el entorno Visual Studio Code de Microsoft. Sigue los siguientes pasos.

• Descarga el software desde la página de descargas. Al instalar te recomendamos que selecciones la opción para Abrir con Visual Studio Code tanto para archivos como para carpetas. Si se te olvidó hacerlo puedes activar a mano esa característica como indica esta página.
• Pincha en el icono Figura: ext icon para instalar las siguientes extensiones: Espressif IDF y Wokwi Simulator.
• Pincha en el icono Figura: idf icon para abrir la configuración de la extensión. Selecciona el botón Express.

Figura: Configuración de la extensión Espressif IDF

• Pincha en Select ESP-IDF version y selecciona la última de las versiones liberadas (releases). Pulsa el botón Install.

Figura: Selección de versión de ESP-IDF

• Tras unos minutos tendrás todo el entorno de desarrollo listo para programar la primera práctica. ESP-IDF incluye el sistema operativo de tiempo real FreeRTOS, que es el que utilizaremos en las prácticas.

Utilizaremos Ptolemy II para modelar las máquinas de estado. Ptolemy II es mucho más que una herramienta de modelado de máquinas de estado. Puede utilizarse para modelar con decenas de modelos de computación y se diseñó para experimentar con la interacción entre modelos de computación distintos. Nosotros utilizaremos una mínima parte.

Para instalar Ptolemy necesitas Java
Si no tienes Java instalado no podrás instalar Ptolemy. Basta con un JRE, aunque no sea muy reciente. Si no lo tienes descárgalo del sitio oficial.

• Descarga el software en la página de descargas de Ptolemy II. La versión 11.0.1 es la última estable en el momento de escribir esta página. No es necesario tener la última versión de desarrollo para este curso.

• Descarga el libro de Ptolemy II. En realidad solo vamos a utilizar este capítulo pero es gratis, aprovecha para tenerlo entero.

Ptolemy II se puede usar para simular el comportamiento de las máquinas de estado, lo que puede ayudar a resolver problemas de modelado. Sin embargo en este curso los problemas de modelado son muy básicos, lo utilizaremos más bien como una herramienta de dibujo de dominio específico.

En este curso exploraremos una única técnica de verificación formal, denominada model checking. El verificador a utilizar es nuXmv de Fondazione Bruno Kessler, basado en SMV, un verificador de Carnegie Mellon University. Sigue los siguientes pasos:

• Descarga la versión para tu equipo desde esta página. Se trata de un simple archivo comprimido que contiene el ejecutable y la documentación. Descomprímelo en alguna carpeta que no tenga espacios en ningún punto de la ruta. Casi cualquier compresor soporta el formato utilizado (tar-gzip o tgz). Por ejemplo, descomprime en C:\sw (creala si no existe, sin miedo). Al descomprimirlo se creará una subcarpeta nuXmv-2.0.0-win64 y dentro de esta hay dos interesantes. La subcarpeta bin es donde se encuentra el ejecutable. La subcarpeta user-man es donde se encuentra el manual de usuario.
• Añade nuXmv a la ruta de programas del sistema operativo. Para ello pulsa la tecla Windows y escribe "Variables". Pincha Variables de entorno. En la sección Variables del sistema selecciona PATH y pincha en Editar. Añade la ruta C:\sw\nuXmv-2.0.0-win64\bin al final.

Con esto podrás ejecutar nuXmv en cualquier ventana de órdenes, lo que resultará muy útil para las prácticas.