Entorno de soporte para el autoaprendizaje en el diseño de
Contents
1. pages 241 268 Springer Berlin Heidelberg 2002 L Prechelt G Malpohl and M Philippsen Find ing plagiarisms among a set of programs with jplag Journal of Universal Computer Science 8 11 1016 1038 2002 F Prados I Boada J Soler and J Poch A web based tool for entity relationship modeling In ICC SA 1 pages 364 372 2006 A Abell M E Rodr guez T Urp X Burgu s M J Casany C Mart and C Quer LEARN SQL Automatic assessment of SQL based on IMS QTI specification IEEE Int Conf Advanced Learning Technologies 0 592 593 2008 M Clavel M Egea and V T da Silva Mova A tool for modeling measuring and validating uml class di agrams Technical report Universidad Complutense de Madrid 20072. los resultados que presentamos no son muy signi ficativos pero dan unas primeras impresiones del potencial de la herramienta En el Cuadro 1 podemos ver una comparaci n de las notas de pr cticas de los estudiantes que han utilizado la plataforma con respecto al total de estudiantes de la asig natura Aunque el n mero de alumnos que la han utilizado es reducido 50 de los que han presentado la pr ctica podemos ver que el porcentaje de estudiantes con notas de Excelente y Notable supera significativamente el global de la asignatura La iteraci n en la resoluci n de los ejerci cios a partir del feedback del entorno ayuda a obtener la soluci n correcta y obtener la m xima puntuaci n en los ejercicios donde pod a usarse el verificador Analizando las estad sticas de uso del entorno hemos observado que los alumnos han utilizado un promedio de entre 3 a 6 inten tos seg n el ejercicio hasta obtener la soluci n correcta Este dato nos confirma que el feedback proporcionado en la mayor a de los casos es positivo y ayuda a resolver al XVII Jornadas de Ense anza Universitaria de la Inform tica M trica Aula Todas las VERIL Aulas Presentados Total 49 47 Aprobados Presentados 93 11 Nota Media Presentados 6 97 6 56 Cuadro 2 Resultados finales asignatura g n caso particular que los estudiantes no hab an tenido en cuenta en su dise o original Con pocas iteraciones con el verificador los
3. posibles circuitos que se pueden verificar En la tabla superior del interfaz aparecen los ejer cicios que se pueden verificar mediante la herramienta La tabla resume el n mero de intentos totales intentos falli dos y correctos realizados para cada ejercicio La parte in ferior se divide en dos pesta as en la primera aparece una descripci n textual del ejercicio mientras que en la segun da aparece el resultado de la verificaci n Al seleccionar el circuito EjemploAND 2 en la pesta a Descripci n se muestra el enunciado del problema A partir de este enunciado se dise a una posible solu ci n que se puede observar en la Figura 5 b En este caso se ha implementado el circuito err neamente a prop sito usando una puerta OR Una vez terminado el dise o se puede verificar mediante el bot n Verificar Es importante que el dise o tenga el mismo n mero de entradas y sali das y con las mismas etiquetas definidas en el enunciado Antes de verificar el comportamiento del circuito el veri ficador comprueba si las entradas y salidas se han definido acorde con el enunciado En caso contrario notifica este error al estudiante inmediatamente Una vez comprobado que se han usado las mismas etiquetas definidas en el enun ciado el resultado de la verificaci n se devuelve en la pes ta a Verificaci n En la Figura 5 c se puede observar el resultado en caso de error El verificador devuelve un con junto de valores para las entrad
4. pr ctica 0 0 0 Ejercicio 2a de la pr ctica 0 o 0 Ejercicio 2d de la pr ctica 0 0 0 Ejercicio 3a de la pr ctica 0 0 0 Ejemplo ANDZ 0 0 o Descripci n verificaci n Implementar un circuito que genere la AND l gica de dos se ales Las entradas del circuito son in1 y in2 y la salida es output lt gt vetas a ANALIZAR FEEDBACK men Y o o Descripci n Verificaci n Tiempo de creaci n del Test 0 016 seg Tiempo de ejeouci n del verificador 1 141 seg lt gt d DISE AR j Logisim main of CircuitoAND2 QU File Edt Project Simulate Window Help r AlB o gt DD CircuitoAND2 int pns output HO Base HO Gates in2 O Plexers D O Arithmetic E Memory Input Output leas y o o Descripci n Verificaci n Tiempo de creaci n del Test 0 031 seg INCORRECTO El comportamiento de los circuitos no es el mismo Para el siguiente vector de bits de entrada el comportamiento difiere ini 1 in2 0 Tiempo de ejecuci n del verificador 2 562 seg lt gt c Figura 5 Ejemplo de verificaci n a Interfaz VERIL de verificaci n b Dise o err neo de un producto l gico de dos entradas c Resultado de la herramienta del dise o proporcionado d Resultado de la herramienta al dise ar el circuito correcto con una puerta l gica AND de 2 entradas de Logisim a Verilog en la Figura 2 se define c
5. Entorno de soporte para el autoaprendizaje en el dise o de circuitos digitales 11 de febrero de 2011 Resumen El dise o de circuitos digitales forma parte de las competencias b sicas en titulaciones tecnol gicas como los nuevos Grados en Ingenier a Inform tica e Ingenier a de Telecomunicaciones Un obst culo importante para el aprendizaje de dichas competencias es que las herramien tas existentes para el dise o de circuitos no permiten al estudiante validar si sus dise os se ajustan a las especifi caciones de partida En este art culo se describe un en torno de autoaprendizaje para que los estudiantes puedan realizar ejercicios de dise o de circuitos y recibir un feed back continuado durante el proceso de aprendizaje de estas competencias 1 Motivaci n En los nuevos grados del espacio europeo de Inge nier a Inform tica y Ingenier a de Telecomunicaciones los alumnos desarrollan las competencias relacionadas con los principios b sicos del funcionamiento del mundo digital En particular unas de las competencias que se deben de sarrollar son las t cnicas de an lisis y s ntesis de circuitos digitales Es esencial que los alumnos sean capaces de dis e ar circuitos digitales antes de ampliar sus conocimientos en las posteriores asignaturas de los respectivos grados El profesorado de esta rea tiene muchas dificultades para dise ar el modelo de aprendizaje de las t cnicas de dise o de circuitos Esta compete
6. Para realizar la pr ctica el estudiante recibe el enuncia do el programa Logisim modificado y un manual de insta Area tem tica no escribir nada aqu Calificaci n de estudiantes VERIL Global Excelente 58 18 Notable 21 9 Aprobado 1 9 Suspenso 1 6 Muy Deficiente 0 5 No Presentado 1 53 Cuadro 1 Calificaciones en la pr ctica laci n y uso de Logisim y VERIL Mediante la plataforma VERIL los estudiantes tienen la posibilidad de verificar 4 ejercicios de la pr ctica con un peso del 65 el 35 restante est asignado a ejercicios no relacionados con dis e o de circuitos La utilizaci n del entorno en esta prueba piloto no ha sido obligatoria pero se ha indicado clara mente al alumnado que su utilizaci n ayuda significativa mente a la superaci n de la pr ctica 4 2 Evaluaci n de la prueba Despu s de realizar la prueba hemos analizado el rendimiento de los estudiantes en la pr ctica N tese que finalmente s lo un n mero reducido de estudiantes han uti lizado la plataforma 1 el total de alumnos que ha presen tado la pr ctica han sido 31 ya que el resto no hab an super ado la evaluaci n continua en esta asignatura hay un gran ndice de abandono de estudiantes cuando no superan la evaluaci n continua 2 El total que alumnos que han uti lizado la herramienta han sido 14 Consideramos que una de las razones ha sido la no obligatoriedad de su uso Por lo tanto
7. alumnos han llegado a la soluci n correcta Finalmente tambi n hemos analizado el resultado de superaci n de la asignatura para ver si existe impacto con la utilizaci n del entorno v ase Cuadro 2 Teniendo en cuenta que el uso de la plataforma no era obligatorio se ha realizado la comparaci n del global de la asignatura con respecto del aula donde se ha hecho la prueba piloto Pode mos observar que el porcentaje de aprobados sobre pre sentados se ve incrementado significativamente Tambi n existe un descenso en el porcentaje de abandono de la asig natura Si calculamos la nota media podemos observar un ligero incremento en el aula de la prueba piloto Si calcu lamos la nota media nicamente de los alumnos que ha uti lizado la plataforma podemos ver que la nota media es de 8 27 Este resultado final nos confirma que la utilizaci n de este entorno puede ayudar a adquirir las competencias de esta asignatura y as incrementar el rendimiento de la misma 4 3 Valoraci n de los estudiantes Hemos realizado una encuesta a los estudiantes para recoger su opini n sobre la prueba piloto Todos concluyen que les ha ayudado en la realizaci n de la pr ctica pero han tenido diferentes dificultades en su utilizaci n e Dificultades en la instalaci n El programa Logisim est implementado en JAVA por lo tanto es mul tiplataforma El inconveniente que conlleva la uti lizaci n del entorno es que se debe instalar un pro grama
8. aparece en la mayor a de herramientas autom ticas El uso de las TIC en la ense anza simplifica los m todos de copia de ejerci cios En este caso un simple fichero permite compar tir la soluci n dise ada por un alumno e Mal uso del verificador Ciertos estudiantes pueden hacer un mal uso del verificador us ndolo como un mecanismo de prueba y error sin analizar real mente el feedback devuelto De esta forma el en torno se convierte en un simple depurador de cir cuitos Para resolver estos problemas potenciales proponemos algunas soluciones En el primer caso se tiene que analizar posteriormente a la entrega el ndice de similitud entre los dise os enviados por los estudiantes Existen herramien tas como JPlag 11 para realizar esta comprobaci n Para controlar el mal uso proponemos limitar el n mero de ver ificaciones en un cierto periodo de tiempo Esta opci n permitir a bloquear temporalmente el acceso al servicio a estudiantes que utilizaran este m todo de prueba y error para obtener la soluci n correcta 5 Conclusiones y trabajo futuro En este art culo hemos presentado un entorno para la verificaci n autom tica de circuitos l gicos Hemos pre sentado resultados preliminares de su utilizaci n con resul tados prometedores tanto en su utilizaci n como en mejo ras de los rendimientos en la asignatura relacionada Este trabajo est relacionada con trabajos previos sobre el uso de herramientas de co
9. as que producen un valor err neo en las salidas Con este feedback el usuario puede simular con Logisim qu salida produce su dise o para es os valores de entrada En este caso el error es evidente Si se modifica el dise o cambiando la puerta OR por una AND y se verifica de nuevo el resultado correcto se puede observar en la Figura 5 d 4 Resultados 4 1 Prueba piloto Para evaluar el impacto de la plataforma en el apren dizaje se ha realizado una prueba piloto en una aula de la asignatura de Fundamentos de Computadores de nuestra universidad El n mero de estudiantes totales de la asig natura consta de 245 alumnos los cuales se encuentran di vididos en 4 aulas El aula escogida para realizar la prueba piloto consta de 61 estudiantes La evaluaci n de esta asignatura est compuesta de una evaluaci n continua con 3 pruebas una pr ctica y un ex amen final La nota final se calcula de la siguiente forma 20 EC 40 P 40 EX donde EC P y EX son las notas de la evaluaci n continua la pr ctica y el examen respectivamente La pr ctica con una duraci n aproxima da de un mes se realiza al final del semestre y permite relacionar todos los conceptos aprendidos en la asignatu ra Concretamente en ella se ejercitan los sistemas de nu meraci n circuitos combinacionales y secuenciales Co mo parte de esta pr ctica el estudiante debe dise ar un conjunto de circuitos que al final se combinan en un sis tema complejo
10. caci n tanto en circuito combinacionales como secuenciales La t cnica de Model Checking consiste en comprobar si un modelo cumple una condici n dada En nuestro caso v ase Figura 3 se traduce en construir a partir de los dos circuitos que se quiere comparar un nuevo circuito con las mismas entradas y con una nica salida tal que su funci n es la siguiente n out A outl Hout2 i 1 donde out 1 y out2 son las salidas i del circuito 1 y circuito 2 respectivamente n el n mero de salidas del circuito y la operaci n XNOR Este circuito deber cumplir que la salida out siempre obtenga el valor 1 Model Checking comprobar de forma eficiente si esta condici n se cumple para todos los posibles valores de entrada y en el caso de circuitos secuenciales para todos los posibles estados El proceso de verificaci n se puede observar en el dia grama de flujo de la Figura 4 Inicialmente la soluci n pro porcionada por el equipo docente est en formato Verilog Actualmente Logisim guarda los circuitos en un formato propio no compatible con ning n lenguaje de descripci n de Hardware formato CIRC Con el prop sito de desar rollar un verificador lo m s independiente posible existe el parser CIRCtoVER que traduce el formato de descripci n XVII Jornadas de Ense anza Universitaria de la Inform tica Veril Wo Curso Fundamentos de Computadores m Ejercicio Intentos Incorrectos Correctos Ejercicio 1c de la
11. complementario para la verificaci n el model checker NuSMV 10 El manual proporcionado a los estudiantes describe paso a paso la instalaci n pero los estudiantes se han encontrado con algunos problemas inesperados durante la instalaci n que de penden sobretodo del sistema operativo utilizado Dificultades en la interpretaci n del feedback En al gunos casos los estudiantes no han sabido entender el error de su dise o a partir del feedback Este prob lema a n es m s evidente en el caso de los circuitos secuenciales en los cuales se devuelve el conjunto de estados correctos hasta encontrar el err neo e Dificultades en la utilizaci n de Logisim El progra ma es muy intuitivo de utilizar pero hay algunos componentes que no est n bien explicados en los manuales por lo que los alumnos tienen dudas sobre su uso Para resolver estos problemas conjuntamente pro ponemos ampliar el manual de instalaci n y de uso de en torno Otra posibilidad es crear un Wiki para almacenar toda esta informaci n electr nicamente junto con alg n tu torial y con por ejemplo una nueva secci n de Preguntas m s frecuentes con los problemas que com nmente se en cuentran los estudiantes 4 4 Valoraci n del equipo docente Aunque despu s del an lisis de los resultados acad mi cos parece que la utilizaci n del entorno es realmente positiva el equipo docente ha detectado algunos inconve nientes e Casos de plagio Este temor
12. dicaci n del estudiante al aprendizaje de las competencias del m bito de tecnolog as de computadores La disponibilidad de herramientas que aporten usabilidad e interacci n hacia los alumnos ayudan a la participaci n de estos en el desarrollo de su aprendizaje en asignaturas complejas Para potenciar y motivar a n m s la introducci n de esta plataforma en el aula se propone asignar un peso en la evaluaci n de la asignatura a actividades pr cticas ligadas a la utilizaci n de la plataforma En concreto se pretende que el feedback continuo pro porcionado por este entorno facilite a los estudiantes el aprendizaje de la asignatura y que esto se vea reflejado en los resultados de la evaluaci n En particular se ha con siderado tres m tricas a evaluar la tasa de abandono de la asignatura la tasa de aprobados y la nota media 3 Descripci n de la plataforma En esta secci n se describe el entorno de soporte al au toaprendizaje que se ha desarrollado Primero se presenta XVII Jornadas de Ense anza Universitaria de la Inform tica Gestor de Base de Datos Servidor Web Interfaz de Navegador Web Profesor Administrador Verificaci n Alumno Figura 2 Arquitectura del entorno de verificaci n la arquitectura de la plataforma En segundo lugar se ex plicita c mo se realiza el proceso de verificaci n 3 1 Arquitectura La plataforma utiliza un modelo cliente servidor tal co mo se muestra en la F
13. e ni sea almacenada en su ordenador Para el proceso de verificaci n se estudiaron dos posi bles implementaciones alternativas La primera era uti lizar t cnicas de simulaci n y la segunda utilizar t cnicas basadas en Model Checking En la primera opci n se de ber a utilizar alg n int rprete de lenguaje de descripci n de Hardware para simular la ejecuci n de los circuitos En este caso se construye un test que simula para los dos circuitos todos los posibles valores en las entradas Para cada valor se comprueba si el valor de cada una de las sal idas coincide Este tipo de simulaci n es bastante r pido para circuitos peque os pero aumenta exponencialmente el tiempo y la complejidad para circuitos con muchas en tradas Adem s el problema se agudiza en el momento de verificar circuitos secuenciales ya que se tiene que com probar la coincidencia de los valores de las salidas para 1 n el caso de utilizar como lenguaje de descripci n Verilog se puede utilizar alg n software libre como Icarius 9 Area tem tica no escribir nada aqu Circuito dise ado Soluci n SI Obtener traza error Figura 4 Proceso de verificaci n todas las entradas y para cada uno de los estados posibles del circuito La segunda t cnica que hemos seleccionado para esta plataforma se fundamenta en Model Checking La ventaja respecto la anterior es su eficiencia en tiempo en el proce so de verifi
14. gura 1 Ejemplo de uso de herramientas de verificaci n en un ejercicio de dise o de circuitos los estudiantes de una aula numerosa Como ejemplo consideremos un ejercicio de dise o de circuitos como el que se muestra en la Figura 1 El enunci ado pide el dise o de una puerta AND En la parte superior de la Figura se muestra la soluci n correcta al ejercicio e imaginemos que un estudiante propone la soluci n err nea que se muestra en la parte inferior de la Figura utilizando una puerta OR Proponemos una herramienta que permi ta al estudiante comprobar por si mismo si su soluci n es correcta y que en caso de error le proporcione como re sultado un conjunto de valores para las entradas que ejem plifique el fallo y permita depurar el dise o En este caso la herramienta indicar a el error dando como ejemplo los valores de entrada inl 1 y in2 0 en los que el valor de la salida obtenida 1 difiere de la esperada en el enunciado 0 Este ejemplo es trivial y s lo se utiliza para ilustrar el proceso de resoluci n de un ejercicio mediante una her ramienta de autocorrecci n Los ejercicios reales de dis e o de circuitos tienen enunciados m s complejos que pueden llegar a tener decenas de puertas l gicas y otros el ementos como registros y multiplexores En este escenario hay m ltiples soluciones posibles y no es trivial identificar posibles errores por lo que el feedback obtenido mediante una herramienta de autocor
15. igura 2 En el servidor el sistema est formado por una base de datos y un servidor Web y de aplicaciones Apache con Tomcat que hace de interfaz para comunicarse con los clientes Internamente la base de datos almacena la informaci n sobre los usuarios y las colecciones de ejercicios existentes Adem s el sistema guarda los dise os enviados por los estudiantes como posi ble soluci n para permitir al docente examinar el progreso de los estudiantes Los usuarios pueden acceder al entorno por dos v as diferentes por navegador Web o mediante el programa de dise o gr fico Logisim 2 dependiendo su perfil Se han considerado tres perfiles de usuario diferentes en esta apli caci n e Perfil de alumno El alumno puede acceder a la plataforma mediante el programa de dise o de cir cuitos l gicos Logisim Mediante este programa el alumno puede ver los ejercicios disponibles y su evoluci n en la resoluci n de los mismos Perfil de profesor El profesor accede a la platafor ma mediante un interfaz Web Mediante este interfaz se pueden a adir modificar ejercicios consultar los ejercicios resueltos por los estudiantes y ver estad s ticas en general de la evoluci n de una aula o de un alumno en concreto Perfil de administrador El administrador tambi n ac cede a la plataforma mediante el interfaz Web y tiene permisos tanto para modificar los usuarios del sis tema como para modificar las aulas disponibles Centr nd
16. je de descripci n de hardware Verilog 7 para posteriormente com parar ambos circuitos mediante Model Checking Despu s de presentar los objetivos docentes Secci n 2 y la arquitectura del entorno Secci n 3 este art culo de scribe la experiencia de su aplicaci n en una asignatura obligatoria Secci n 4 1 los resultados en el aprendiza je Secci n 4 2 y las valoraciones de estudiantes Sec ci n 4 3 y del equipo docente Secci n 4 4 2 Objetivos docentes El principal objetivo es proporcionar un entorno virtu al para la autocorrecci n de ejercicios de dise o de cir cuitos con disponibilidad 24x7 las 24 horas los 7 d as de la semana Mediante este entorno los estudiantes pueden comprobar de forma autom tica si su dise o es cor recto Adem s de facilitar el proceso de autoevaluaci n la plataforma permite tambi n tener un control sobre la evoluci n de los alumnos en todo momento registrando su utilizaci n por parte de los estudiantes y los patrones de su uso Es importante de destacar tambi n la mejora en la Area tem tica no escribir nada aqu asincron a del aprendizaje debido a la relajaci n de las re stricciones de espacio y tiempo de utilizaci n as como la disponibilidad temporal del profesorado En las asignaturas de primer curso donde se aprende la competencia de dise o de circuito digitales en nuestro ca so Fundamentos de Computadores los estudiantes uti lizan una herramien
17. l verificador tambi n es posible su utilizaci n en otras asignaturas m s avanzadas dentro del mismo mbito co mo Electr nica Digital Una ventaja del analizador es que al ser dependiente nicamente de Verilog es posible de uti lizarlo en asignaturas donde se dise en circuitos m s com plejos descritos con lenguajes de descripci n de Hardware como Verilog 7 o bien VHDL 8 Referencias 1 Capilano Computing LogicWorks 5 Interactive Soft ware Prentice Hall 2004 2 C Burch Logisim a graphical tool for designing and simulating logic circuits B 4 5 6 7 8 9 10 11 12 13 14 Area tem tica no escribir nada aqu http ozark hendrix edu burch logisim 2010 CEDAR CEDAR logic simulator http cedarlogic scienceontheweb net 2010 Magma Magma EDA tools http www magma da com 2010 Synopsys Synopsys EDA tools http www synopsys com 2010 L McMillan K Symbolic Model Checking Kluwer 1993 F Vahid Verilog for Digital Design Wiley 2007 V A Pedroni Circuit Design with VHDL The MIT Press 2004 S Williams Icarius a free compiler for Verilog http bleyer org icarus 2010 Cimatti E M Clarke E Giunchiglia F Giunchiglia M Pistore M Roveri R Sebastiani and A Tacchel la NuSMV 2 An opensource tool for symbolic mod el checking In Computer Aided Verification volume 2404 of Lecture Notes in Computer Science
18. ncia normalmente est ligada a asignaturas obligatorias de primer curso como por ejemplo Fundamentos de Computadores con un alto n mero de estudiantes y con hist ricos importantes en la mayor a de universidades sobre el nivel de abandono y de no superaci n de la asignatura Las actividades que se de sarrollan en este mbito docente en formato de ejercicios tipo consisten en dise ar diversos circuitos a partir de una especificaci n de partida basada en un conjunto de en tradas de salidas y el comportamiento final deseado para el circuito en relaci n a estas se ales Al estudiante se le pide que describa los componentes del circuito que implementa este comportamiento Las actividades relacionadas con el dise o de circuitos no son un proceso mec nico sino m s bien creativo y se puede obtener m s de una soluci n v li da Por eso es vital que los alumnos puedan desarrollar el m ximo n mero de actividades pr cticas en este mbito recibiendo un feedback constante que les permita evaluar su progreso Para el profesorado habitualmente es dif cil dar un feedback inmediato constante e individual a todos Enunciado Dise a un circuito con dos entradas in1 in2 cuya salida output tenga valor 1 si y s lo si ambas entradas tienen valor 1 Soluci n correcta ino in2 output Dise o estudiante int in2 0 O output Feedback INCORRECTO para la traza de entrada inl 0 in2 1 Fi
19. omo tra ductor En el momento en que los dos circuitos a verificar ya est n en formato Verilog se puede iniciar el m dulo de verificaci n DiCiCheck Digital Circuit Checking que en la Figura 2 se define como Llamada Model Checker Ini cialmente este m dulo construye el modelo explicado an teriormente utilizando el m dulo VERtoSMV Un model checker verificar si la condici n propuesta se cumple so bre el modelo Posteriormente el sistema analiza la salida del model checker que en caso de no ser funcionalmente equivalentes ya devuelve una traza indicando para que val ores de las entradas se ha detectado el error Esta traza se indica al estudiante en la pesta a de Verificaci n en el in terfaz VERIL N tese que en caso de ser un circuito se cuencial devuelve el conjunto de estados que ha verificado correctamente hasta encontrar el error Mediante esta in 2Nuestro verificador utiliza el model checker NuSMV 10 formaci n el alumno recibe el feedback y puede compro bar manualmente en Logisim los valores de la traza prob lem tica y corregir su dise o para evitarlo 3 3 Ejemplo de verificaci n En la Figura 5 se presenta a modo de ejemplo la verifi caci n del circuito mostrado en la Secci n de Motivaci n El objetivo es dise ar un circuito que produzca el producto l gico de dos entradas Las entradas se identifican por inl y in2 y la salida por out put En la Figura 5 a podemos ver el interfaz VERIL con los
20. onos en los estudiantes ya hemos mencionado que el acceso a la plataforma se realiza mediante una ver Circuito Estudiante Entradas oute Soluci n Propuesta Figura 3 Modelo de verificaci n utilizando Model Check ing si n del programa Logisim modificada El programa que utilizan los alumnos ha sido adaptado con la introducci n de un nuevo m dulo VERIL que se puede ver en la Figu ra 5 a Este nuevo interfaz permite visualizar los ejerci cios disponibles y permite verificar el circuito dise ado en ese momento mediante Logisim El proceso de verifi caci n conjuntamente con un ejemplo de verificaci n se explicar n de forma detallada en las siguientes secciones 3 2 Proceso de verificaci n Como se puede observar en la Figura 2 el proceso de verificaci n se produce en el ordenador del estudiante Es ta decisi n se justifica para garantizar la escalabilidad de la plataforma el proceso de verificaci n de un circuito re quiere un c lculo intensivo por lo que realizar este proceso en el servidor podr a dificultar el acceso de los estudiantes al entorno durante los picos de utilizaci n como las fechas de entrega de las pr cticas Realizando la verificaci n en el cliente se evitan posibles sobrecargas del servidor y se garantiza la prestaci n de servicio N tese que se han im plementado medidas especiales de seguridad para qu la soluci n propuesta por el equipo docente no sea visible para el estudiant
21. recci n puede ser muy valioso Actualmente existen varias herramientas inform ticas mediante las cuales los alumnos pueden dise ar gr fica mente circuitos l gicos 1 2 3 Estas herramientas son muy intuitivas de utilizar pero tienen un inconveniente los alumnos no pueden determinar si su dise o es v li do a partir de la especificaci n dada Precisamente para aportar soluci n a esta problem tica se propone un entorno virtual de autoaprendizaje que per mita a los estudiantes una mejora constante y autoevaluada de sus habilidades de dise o de circuitos El entorno tiene las siguientes caracter sticas e El sistema de verificaci n es similar al utilizado en la industria de fabricaci n de microchips para la ver ificaci n de sus dise os 4 5 aunque a menor es cala Se ha desarrollado desde cero una herramienta acad mica de verificaci n basada en analizar los cir cuitos mediante t cnicas de Model Checking 6 e La herramienta verifica si dos circuitos son fun cionalmente iguales es decir no realiza la compara ci n de si los dos circuitos tienen el mismo n mero exacto de componentes internos sino que se com prueba si tienen el mismo comportamiento propor cionando un contraejemplo en caso contrario El alumno utiliza un software de dise o y simulaci n de circuitos 2 que permite dibujar el circuito Inter namente el proceso de verificaci n traduce este dis e o y la soluci n oficial a un lengua
22. rrecci n aut matica aplicada a diferentes mbitos de la inform tica programaci n bases de datos 12 13 ingenier a del software 14 etc Con sideramos que hay dos aspectos destacables de esta aprox imaci n El primero es la integraci n de la plataforma con la herramienta de dise o de circuitos usada en la asignatu ra de forma que el estudiante puede aprovechar la autocor recci n sin tener que salir de la herramienta y interfaz gr fica que le es familiar El segundo aspecto es la utilizaci n de Model Checking para la verificaci n de los circuitos Esta t cnica proporciona feedback al estudiante y a difer encia de otros entornos para la correcci n autom tica no requiere hacer el esfuerzo de definir juegos de prueba ni se basa en la comparaci n directa de un circuito con otro con lo que se permiten circuitos diferentes pero con el mismo comportamiento Este entorno a n tiene algunos inconvenientes en su uti lizaci n detectados y recogidos en la prueba piloto Los cuales seran revisados en futuras versiones a se intentar mejorar la usabilidad del entorno b Limitado uso ya que solo se utiliza como herramienta de soporte en las pr cti cas Proponemos que en un futuro haya un repositorio de ejercicios de autoevaluaci n adicionales que ayuden a los alumnos a reforzar los conocimientos adquiridos Aunque nuestro primer objetivo ha sido utilizar el en torno en la asignatura de Fundamentos de Computadores e
23. ta de dise o gr fico de circuitos 2 Esta herramienta les permite dise ar gr ficamente los cir cuitos sin necesidad de tener conocimientos de lenguajes de descripci n de hardware 8 7 Adem s les permite simular de forma manual su dise o para valores concretos en las entradas En este proceso de aprendizaje creemos que es fundamental que los estudiantes puedan recibir un feedback inmediato en el momento de resolver un ejerci cio de dise o El dise o de circuitos no es una actividad repetitiva sino que requiere un alto grado de creatividad que debe adquirirse con la pr ctica El feedback permite identificar los errores y corregirlos para evitarlos en el fu turo Este entorno permite el autoaprendizaje y autoevalu aci n de los estudiantes de una forma planificada Tam bi n se puede controlar en todo momento los ejercicios disponibles De esta forma se puede planificar el conjunto de ejercicios que los alumnos tienen disponibles depen diendo del material docente planificado en cada semana Mediante este control de la informaci n disponible con juntamente con los datos estad sticos se puede conocer en todo momento la evoluci n individual de los alumnos y de la evoluci n colectiva de las aulas Esta informaci n per mite al profesorado detectar las principales carencias de los estudiantes en los aspectos de dise o para poder incidir en los puntos d biles que se observen Creemos que este entorno puede potenciar la de
Download Pdf Manuals
Related Search