Entorno de soporte para el autoaprendizaje en el diseño de
Contents
1. a Model Checker gt Do 3 Navegador Verificaci n a Web Traductor NuSMY Clientes Herramienta de Dise o Gr fico Profesor Administrador i Alumno Figura 2 Arquitectura del entorno de verificaci n entorno permite incidir en el autoaprendizaje de los alumnos en competencias complejas En las asignaturas de primer curso donde se desa rrolla la competencia de dise o de circuito digitales en nuestro caso Fundamentos de Computadores los estudiantes utilizan una herramienta de dise o gr fico de circuitos 2 Esta herramienta les permi te dise ar gr ficamente los circuitos sin necesidad de tener conocimientos de lenguajes de descripci n de hardware 9 15 Adem s les permite simular de forma manual su dise o para valores concretos en las entradas En este proceso de aprendizaje cree mos fundamental que los estudiantes puedan recibir un feedback inmediato en el momento de resolver un ejercicio 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 para co rregirlos Este entorno permite el autoaprendizaje y auto evaluaci n de los estudiantes de una forma planifi cada Tambi 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 dependiendo d2. Oberta de Catalunya Referencias 1 A Abell M E Rodr guez T Urp X Bur gu s M J Casany C Mart and C Quer LEARN SQL Automatic assessment of SQL 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 P steres y recursos docentes based on IMS QTI specification ICALT pages 592 593 2008 C Burch Logisim a graphical tool for desig ning and simulating logic circuits http ozark hendrix edu burch logisim 2010 CEDAR CEDAR logic simulator http cedarlogic scienceontheweb net 2010 Cimatti E M Clarke E Giunchiglia F Giun chiglia M Pistore M Roveri R Sebastiani and A Tacchella NuSMV 2 An opensource tool for symbolic model checking In Com puter Aided Verification volume 2404 pages 241 268 Springer Berlin 2002 Capilano Computing LogicWorks 5 Interacti ve Software Prentice Hall 2004 J Garc a J Sanz and B Sotomayor A new approach to educational software for logic analysis and design In International Confe rence on Education IADAT e2004 2004 M J Castel De Haro F Gallego C Poma res P Suau C J Villagr and S Cort s e VALUACI N en tiempo real In JENUT 2009 K L McMillan Symbolic Model Checking Kluwer 1993 V A Pedroni Circuit Design with VHDL The MIT Press 2004 J Petit and S Roura Programaci n 1 Una asignatura orientada a la resoluci n de proble mas In JENUI 2009 20
3. autocorrecci n puede ser muy valioso Actualmente existen varias herramientas acad micas mediante las cuales los alumnos pueden di se ar gr ficamente circuitos l gicos Estas herramientas son muy intuitivas de utilizar pero tie nen un inconveniente no se puede determinar si un dise o es v lido a partir de una especificaci n dada P steres y recursos docentes Para realizar esta verificaci n existen herramientas industriales de dise o y verificaci n 14 No obstan te su utilizaci n presenta varios inconvenientes su uso en asignaturas introductorias no es adecuado de bido a su complejidad y alto coste econ mico Tam bi n existe otro tipo de herramientas que muestran de forma autom tica el dise o de circuitos a partir de un mapa de Karnaugh o grafo de estados 6 pero no permiten verificar si el dise o proporcionado por un alumno es correcto a partir de la especificaci n Precisamente para aportar soluci n a esta proble m tica se propone un entorno virtual de autoapren dizaje que permita a los estudiantes una autoevalua ci n constante de sus dise os 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 14 aunque a menor escala Se ha desarrollado una herramienta acad mica de verificaci n basada en analizar los circuitos mediante t cnicas de Model Checking 8 e La herramienta v
4. de 61 estudiantes La evaluaci n de esta asignatura se realiza me 476 Li VerilUOC tJ Curso Fundamentos de Computadores x Ejercicio Intentos Incorrectos Correctos Ejercido 1c de la pr ctica o Ejercicio 2a de la pr ctica o Ejercicio 2d de la pr ctica Ejercicio 3a de la pr ctica Ejemplo AND2 Descripci n verificaci n Soo lalolo o o alojo o o Implementar un circuito que genere la AND l gica de dos se ales Las entradas del circuito sonin1 y in2 y la salida es output P steres y recursos docentes 2 Logisim main of CircuitoANDZ QuE File Edt Project Simulate Window Help 5 ale e gt DD t CIrCuROAND2 im A main a n D Ooutput 7 Jul mot O Plexers Arithmetic E Memory H O Input Output 100 DISE AR a ANALIZAR FEEDBACK la u o o Tiempo de creaci n del Test 0 016 seg Descripci n Verificaci n Tiempo de ejecuci n del verificador 1 141 seg El m d diante una evaluaci n continua con 3 pruebas una pr ctica y un examen final La nota final se calcula de la siguiente forma 20 WEC 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 aproximada de un mes se realiza al final del semestre y permite rela cionar todos los conceptos aprendidos en la asigna tura Concretamente en ella se ejercitan los siste
5. entradas se ha de tectado el error Esta traza se indica al estudiante en la pesta a de Verificaci n en el interfaz VERILUOC N tese que en caso de ser un circuito secuencial de vuelve el conjunto de estados que ha verificado co rrectamente hasta encontrar el error Mediante esta informaci n el alumno recibe el feedback y puede comprobar manualmente en Logisim los valores de la traza problem tica y corregir su dise o 3 3 Ejemplo de verificaci n En la Figura 5 se presenta a modo de ejemplo la verificaci 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 en tradas se identifican por inl y in2 y la salida por output En la Figura 5 a podemos ver el interfaz VERILUOC con los posibles circuitos que se pue den verificar en la tabla superior La tabla resume el n mero de intentos totales fallidos y correctos reali zados para cada ejercicio La parte inferior se divide en dos pesta as en la primera aparece una descrip ci n textual del ejercicio mientras que en la segunda 2Nuestro verificador utiliza el model checker NuSMV 4 Soluci n propuesta Circuito dise ado J CIRCtoVER Ejecutar NuSMV Obtener traza error Ccorrecto C Err neo gt Figura 4 Proceso de verificaci n aparece el resultado de la verificaci n Al seleccio nar el circu
6. ha sido adaptado con la introduc ci n de un nuevo m dulo VERILUOC que se pue de ver en la Figura 5 a Este nuevo interfaz permite visualizar los ejercicios disponibles y permite veri ficar el circuito dise ado en ese momento mediante Logisim En las siguientes secciones describiremos el proceso de verificaci n junto con un ejemplo 3 2 Proceso de verificaci n Como se puede observar en la Figura 2 el pro ceso de verificaci n se produce en el ordenador del estudiante Esta decisi n se justifica para garantizar la escalabilidad de la plataforma el proceso de veri ficaci n de un circuito requiere un c lculo intensivo por lo que realizar este proceso en el servidor podr a P steres y recursos docentes dificultar el acceso de los estudiantes al entorno du rante los picos de utilizaci n como las fechas de en trega 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 Es necesario observar que se han implementado medidas especia les de seguridad para que la soluci n propuesta por el equipo docente no sea visible para el estudiante ni sea almacenada en su ordenador Para el proceso de verificaci n se estudiaron dos posibles implementaciones alternativas La primera era utilizar t cnicas de simulaci n y la segunda uti lizar t cnicas basadas en Model Checking En la pri mera opci n se deber a utilizar alg n int rpre
7. s lo un n mero reducido de estudiantes han utilizado la plataforma 1 El total de alumnos que ha presentado la pr ctica han sido 31 ya que el resto no hab an superado la evaluaci n continua en esta asignatura hay un gran ndice de abandono de estudiantes cuando no superan la eva luaci n continua 2 El total que alumnos que han utilizado la herramienta han sido 14 Consideramos que una de las razones ha sido la no obligatoriedad de su uso Por lo tanto los resultados que presenta mos no son muy significativos pero muestran unos primeros indicios 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 uti lizado la plataforma con respecto al total de estu diantes de la asignatura Aunque el n mero de alum nos que la han utilizado es reducido 50 de los que han presentado la pr ctica podemos ver que el por centaje de estudiantes con notas de Excelente y No table supera significativamente el global de la asig natura La iteraci n en la resoluci n de los ejercicios a partir del feedback del entorno ayuda a obtener la XVII Jornadas de Ense anza Universitaria de la Inform tica 477 Calificaci n de estudiantes VERILUOC Global Excelente 58 18 Notable 21 9 Aprobado 1 9 Suspenso 1 6 Muy Deficiente 0 5 No Presentado 7 53 Cuadro 1 Calificaciones en la pr ctica soluci n correcta y obtener la m xima p
8. 09 F Prados I Boada J Soler and J Poch Au tomatic generation and correction of technical exercises In ICECE 053 2005 L Prechelt G Malpohl and M Philippsen Finding plagiarisms among a set of programs with JPlag Journal of Universal Computer Science 8 11 1016 1038 2002 M Serra E Santamaria M A Rius M A Huertas and M E Rodr guez Nuevos para digmas de la educaci n roles de acci n docen te en el entorno virtual de la UOC In CEDI 05 2005 Synopsys Synopsys EDA tools http www synopsys com 2010 F Vahid Verilog for Digital Design Wiley 2007 S Williams Icarius a free compiler for Veri log http bleyer org icarus 2010
9. Checking 1 Motivaci n En los nuevos grados del espacio europeo de In genier a Inform tica e Ingenier a de Telecomunica ciones los alumnos desarrollan las competencias re lacionadas con los principios b sicos del funciona miento del mundo digital Una competencia b sica a adquirir es saber aplicar t cnicas de an lisis y s n tesis de circuitos digitales sencillos Es esencial que los alumnos sean capaces de dise ar circuitos digi tales antes de ampliar sus conocimientos en las pos teriores asignaturas de los respectivos grados El profesorado de esta rea tiene muchas dificul tades para dise ar el modelo de aprendizaje de las 471 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 in 0 E O output in2 0 Dise o estudiante int O o O output in2 0 Feedback INCORRECTO para la traza de entrada in1 0 in2 1 Figura 1 Ejemplo de uso de herramientas de verificaci n en un ejercicio de dise o de circuitos t cnicas de dise o de circuitos Normalmente esta competencia est ligada a asignaturas obligatorias de primer curso como por ejemplo Fundamentos de Computadores con un alto n mero de estudian tes e hist ricos importantes sobre el nivel de aban dono y de no superaci n de la asignatura Un ejer cicio tipo en este mbito docente consiste en di se ar diversos circuitos
10. Entorno de soporte para el autoaprendizaje en el dise o de circuitos digitales D Ba eres I Bermejo R Claris J Jorba M Serra F Santanach A Rodr guez Universitat Oberta de Catalunya Rambla del Poblenou 156 08018 Barcelona ldbaneres rclariso jjorba mserravi fsantanach jrodriguezgarrjQ0uoc edu ivan200gmail com Resumen El dise o de circuitos digitales forma parte de las competencias b sicas de los nuevos Grados en In genier a Inform tica e Ingenier a de Telecomunica ciones Un obst culo importante para el aprendiza je de dichas competencias es que las herramientas acad micas existentes para el dise o de circuitos no permiten validar si un dise o se ajusta a la especi ficaci n de partida En este art culo se describe un entorno de autoaprendizaje para que los estudiantes puedan realizar ejercicios de dise o de circuitos y recibir un feedback continuo Summary The design of digital circuits is a basic compe tence of the new Degrees in Computer Science and Engineering of Telecommunications An important hindrance in the learning process of these skills is that the existing academic tools for the design of cir cuits do not allow the student to validate if his design satisfies the specification In this article we describe an online environment where the students can verify their designs with an automatic feedback Palabras clave Circuitos verificaci n autoevaluaci n educaci n a distancia Model
11. a partir de una especifica ci n de partida sta se basa en un conjunto de en tradas de salidas y el comportamiento final deseado para el circuito en relaci n a estas se ales Al estu diante 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 creati vo y se puede obtener m s de una soluci n v lida Por eso es vital que los alumnos puedan desarro llar estas pr cticas recibiendo un feedback constante que les permita evaluar el progreso de su aprendiza je Habitualmente para el profesorado es dif cil dar un feedback inmediato constante e individual a to dos los estudiantes de una aula numerosa Adem s 472 el problema es significativamente mayor cuando el sistema de aprendizaje es a distancia Esta inquietud surge tambi n en la docencia de otros mbitos tem ticos dentro de la Inform tica El trabajo en este campo ha dado lugar al desarrollo de diferentes herramientas para la autoevaluaci n de ejercicios como por ejemplo LEARN SQL 1 ba ses de datos ACME 11 matem ticas estad stica bases de datos y otros Jutge org programaci n 10 o Pl Man l gica 7 entre otros La mayor a de es tas herramientas se basan en la comprovaci n del re sultado de juegos de prueba Sin embargo estas he rramientas no resultan apropiadas para la autoeva luaci n de circuitos l gicos
12. aci n de la pr ctica pero han tenido diferentes dificultades en su utilizaci n e Dificultades en la instalaci n El programa Lo gisim est implementado en JAVA por lo tanto es multiplataforma El inconveniente que con lleva la utilizaci n del entorno es que se debe instalar un programa complementario para la verificaci n el model checker NuSMV 4 El manual proporcionado a los estudiantes descri M trica Aula Todas las VERILUOC Aulas Present Total 49 47 Aprobados Present 93 11 Nota Media Present 6 97 6 56 Cuadro 2 Resultados finales asignatura be paso a paso la instalaci n pero los estudian tes se han encontrado con algunos problemas inesperados durante la instalaci n que depen den sobretodo del sistema operativo utilizado e Dificultades en la interpretaci n del feedback En algunos casos los estudiantes no han sabido entender el error de su dise o a partir del feed back Este problema a n es m s evidente en el caso de los circuitos secuenciales en los cua les se devuelve el conjunto de estados correctos hasta encontrar el err neo Dificultades en la utilizaci n de Logisim El programa es muy intuitivo de utilizar pero hay algunos componentes que no est n bien expli cados en los manuales por lo que los alumnos tienen dudas sobre su uso Para resolver estos problemas de forma global proponemos mejorar el manual de instalaci n y de uso de entorno Otra posibilida
13. d es crear un Wiki pa ra almacenar toda esta informaci n electr nicamen te junto con una nueva secci n de Preguntas m s frecuentes con los problemas m s comunes 4 4 Valoraci n del equipo docente El equipo docente ha detectado algunos inconve nientes en la utilizaci n del entorno e Casos de plagio Este temor aparece en la ma yor a de herramientas autom ticas El uso de las TIC en la ense anza simplifica los m todos de copia de ejercicios e Mal uso del verificador Ciertos estudiantes pueden hacer un mal uso del verificador us n dolo como un mecanismo de prueba y error sin analizar realmente el feedback devuelto Para resolver estos problemas potenciales propo nemos algunas soluciones En el primer caso se de ber a analizar posteriormente a la entrega el ndice de similitud entre los dise os enviados por los es tudiantes Existen herramientas como JPlag 12 pa ra realizar esta comprobaci n Para controlar el mal 478 uso proponemos limitar el n mero de verificaciones en un cierto periodo de tiempo 5 Conclusiones y trabajo futuro En este art culo hemos presentado un entorno para la verificaci n autom tica de circuitos l gicos y re sultados preliminares con mejoras de los rendimien tos en la asignatura relacionada Consideramos que hay dos aspectos destacables de esta aproximaci n El primero es la integraci n de la plataforma con la herramienta de dise o de cir cuitos usada
14. el material docen te asignado para cada una de las semanas Median te este control de la informaci n disponible y junto 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 informa ci n permite 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 dicaci n del estudiante al aprendizaje de las com petencias del mbito de tecnolog as de computado res 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 esta plataforma En concreto se pretende que este entorno facili te a los estudiantes el aprendizaje de la asignatura y que esto se vea reflejado en los resultados de la eva luaci n En particular se ha considerado tres m tri cas 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 autoaprendizaje desarrollado En primer lugar se presenta la arquitectura de la plataforma En segun do lugar se explicita c mo se realiza el proceso de verificaci n 474 3 1 Arquitectura La plataforma utiliza un modelo cliente
15. el n mero de entradas posibles es muy elevado y no resulta factible definir el resultado esperado para cada una de ellas Tam poco es posible identificar un subconjunto de casos representativos Como ejemplo consideremos un ejercicio de di se o de circuitos como el que se muestra en la Figu ra 1 El enunciado pide el dise o de una puerta AND En la parte superior de la figura se muestra la solu ci n correcta al ejercicio Imaginemos que un estu diante propone la soluci n err nea que se muestra en la parte inferior de la figura utilizando una puer ta OR Proponemos una herramienta que permita al estudiante comprobar por s mismo si su soluci n es correcta y que en caso de error le proporcione como resultado un conjunto de valores para las en tradas que ejemplifique 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 Es te ejemplo es trivial y s lo se utiliza para ilustrar el proceso de resoluci n Los ejercicios reales de di se o de circuitos tienen enunciados m s complejos que pueden llegar a tener decenas de puertas l gicas y otros elementos 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
16. en la asignatura de forma que el estu diante puede aprovechar la autocorrecci n sin tener que salir de la herramienta 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 diferencia de otros entornos para la correcci n autom tica no requiere hacer el esfuerzo de definir juegos de prueba ni se basa en la com paraci 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 utilizaci n los cuales han sido detectados y reco gidos en la prueba piloto Adem s ser n revisados en futuras versiones 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 entorno en la asignatura de Fundamentos de Compu tadores el verificador tambi n es posible su utiliza ci n en otras asignaturas m s avanzadas dentro del mismo mbito como Electr nica Digital Una ven taja del analizador es que al ser dependiente nica mente de Verilog es posible utilizarlo en asignaturas donde se dise en circuitos m s complejos descritos con lenguajes de descripci n de Hardware como Ve rilog 15 o bien VHDL 9 Agradecimientos Este trabajo ha sido financiado con la ayuda APLICA 2010 de la Univ
17. erifica si dos circuitos son fun cionalmente iguales es decir se comprueba si tienen el mismo comportamiento proporcio nando un contraejemplo en caso contrario e El alumno utiliza un software de dise o y si mulaci n de circuitos 2 que permite dibujar el circuito Internamente el proceso de verifica ci n compara este dise o con la soluci n oficial mediante Model Checking Despu s de presentar los objetivos docentes Sec ci n 2 y la arquitectura del entorno Secci n 3 este art culo describe la experiencia de su aplicaci n en una asignatura obligatoria con el respectivo an lisis de los resultados Secci n 4 2 Objetivos docentes El principal objetivo es proporcionar un entorno virtual para la autocorrecci n de ejercicios de dise o de circuitos 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 correcto Adem s de facilitar el pro ceso de autoevaluaci n la plataforma permite tener un control sobre la evoluci n de los alumnos en todo momento registrando su utilizaci n y los patrones de uso En universidades virtuales como es el caso de la Universitat Oberta de Catalunya UOC 13 este XVII Jornadas de Ense anza Universitaria de la Inform tica 473 Servidor Gestor de Base de Datos I Servidor Web Llamada Y i t y
18. ito E jemploAND2 en la pesta a Des cripci n se muestra el enunciado del problema A partir de este enunciado se dise a una posible soluci n V ase 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 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 En la Figura 5 c se puede observar el resultado en ca so de error que aparece en la pesta a Verificaci n El verificador devuelve un conjunto de valores pa ra las entradas que producen un valor err neo en las salidas Con este feedback el usuario puede simu lar con Logisim qu salida produce su dise o para esos valores de entrada En este caso el error es evi dente 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 aprendizaje se ha realizado una prueba piloto en una aula de la asignatura de Fundamentos de Compu tadores del Grado en Ingenier a Inform tica de la UOC 13 La asignatura consta de 245 alumnos los cuales se encuentran divididos en 4 aulas El aula escogida para realizar la prueba piloto consta
19. mas de numeraci n circuitos combinacionales y secuen ciales Como parte de esta pr ctica el estudiante de be dise ar un conjunto de circuitos que al final se combinan en un sistema complejo Para realizar la pr ctica el estudiante recibe el enunciado el programa Logisim modificado y un manual de instalaci n y uso de Logisim y VERI LUOC Mediante la plataforma VERILUOC los es tudiantes tienen la posibilidad de verificar 4 ejerci cios de la pr ctica con un peso del 65 el 35 restante est asignado a ejercicios no relacionados con dise o de circuitos El uso del entorno en es ta prueba piloto no ha sido obligatoria pero se ha explicado al alumnado que su utilizaci n ayuda sig nificativamente a la superaci n de la pr ctica b VERIFICAR y A 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 difere c Figura 5 Ejemplo de verificaci n a Interfaz VERILUOC 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 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
20. servidor tal como se muestra en la Figura 2 En el servidor el sistema est formado por una base de datos y un servidor Web y de aplicaciones Apache con Tom cat 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 posible soluci n para permitir al docente examinar el pro greso 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 dependien do de su perfil Se han considerado dos perfiles de usuario diferentes en esta aplicaci n e Perfil de alumno El alumno puede acceder a la plataforma mediante el programa de dise o de circuitos l gicos Logisim El alumno puede ver en todo momento los ejercicios disponibles y su evoluci n en la resoluci n de los mismos e Perfil de profesor administrador El profesor accede a la plataforma mediante un interfaz Web Mediante este interfaz se pueden a a dir modificar ejercicios consultar los ejercicios resueltos por los estudiantes y ver estad sticas sobre la evoluci n de una aula o de un alumno en concreto Tambi n se tienen permisos tan to para modificar los usuarios del sistema como para modificar las aulas disponibles Centr ndonos en los estudiantes el programa Lo gisim que utilizan
21. te de lenguaje de descripci n de Hardware para simular la ejecuci n de los circuitos En este caso se cons truye 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 salidas coincide Este tipo de simulaci n es bastante r pido para circuitos peque os pero aumenta exponencial mente el tiempo y la complejidad para circuitos con muchas entradas Adem s el problema se agudiza en el momento de verificar circuitos secuenciales La segunda t cnica que hemos seleccionado para esta plataforma se fundamenta en Model Checking La ventaja respecto a la anterior es su eficiencia en tiempo en el proceso de verificaci n tanto en circui tos combinacionales como secuenciales La t cnica de Model Checking consiste en comprobar si un mo delo 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 sa lida con la funci n out Aj_ outl Sout2 donde outl y out2 son las salidas i del circuito 1 y circui to 2 respectivamente n el n mero de salidas del cir cuito 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 sec
22. uen ciales para todos los posibles estados El proceso de verificaci n se puede observar en el diagrama de flujo de la Figura 4 Inicialmente la so luci n proporcionada por el equipo docente est en formato Verilog Actualmente Logisim guarda los lEn el caso de utilizar como lenguaje de descripci n Verilog se puede utilizar alg n software libre como Icarius 16 XVII Jornadas de Ense anza Universitaria de la Inform tica 475 Circuito E j Estudiante Entradas Propuesta Figura 3 Modelo de verificaci n con Model Checking circuitos en un formato propio no compatible con ning n lenguaje de descripci n de Hardware forma to CIRC Con el prop sito de desarrollar un verifi cador lo m s independiente posible existe el parser CIRCtoVER que traduce el formato de descripci n de Logisim a Verilog en la Figura 2 se define como traductor En el momento en que los dos circuitos a verificar ya est n en formato Verilog se puede ini ciar el m dulo de verificaci n DiCiCheck Digital Circuit Checking que en la Figura 2 se define co mo Llamada Model Checker Inicialmente este m dulo construye el modelo explicado anteriormente utilizando el m dulo VERtoSMV Un model chec ker verificar si la condici n propuesta se cumple sobre 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 valores de las
23. untuaci n en los ejercicios donde pod a usarse el verificador Ana lizando las estad sticas de uso del entorno hemos observado que los alumnos han utilizado un prome dio de entre 3 a 6 intentos seg n el ejercicio hasta obtener la soluci n correcta Este dato nos confirma que el feedback en la mayor a de los casos es posi tivo y ayuda a resolver alg n caso particular que los estudiantes no hab an tenido en cuenta Finalmente tambi n hemos analizado el resulta do de superaci n de la asignatura 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 Podemos observar que el porcentaje de aprobados sobre presentados se ve incrementado significativamente Tambi n existe un descenso en el porcentaje de abandono de la asigna tura Si calculamos la nota media podemos observar un ligero incremento en el aula de la prueba piloto Si calculamos la nota media nicamente de los alum nos que ha utilizado 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 asigna tura 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 Todos concluyen que les ha ayudado en la realiz
Download Pdf Manuals
Related Search