Buscar en
Revista Iberoamericana de Automática e Informática Industrial RIAI
Toda la web
Inicio Revista Iberoamericana de Automática e Informática Industrial RIAI Módulo Empresarial para la Validación Formal de Ejercicios aplicado a la Progr...
Información de la revista
Vol. 9. Núm. 3.
Páginas 290-299 (Julio - Septiembre 2012)
Compartir
Compartir
Descargar PDF
Más opciones de artículo
Visitas
4281
Vol. 9. Núm. 3.
Páginas 290-299 (Julio - Septiembre 2012)
Open Access
Módulo Empresarial para la Validación Formal de Ejercicios aplicado a la Programación Concurrente en Java
Enterprise Module for Exercise Formal Validation applied on Java Concurrent Programming
Visitas
4281
P. Basanta-Val
,1
, M. García-Valls, I. Estévez-Ayres, M.J. Martin-Gutiérrez
Departamento de Ingeniería Telemática, Universidad Carlos III de Madrid, Avda. de la Universidad no 30, 28911, (Leganés) Madrid, España
Este artículo ha recibido

Under a Creative Commons license
Información del artículo
Resumen
Texto completo
Bibliografía
Descargar PDF
Estadísticas
Resumen

La utilización de herramientas que permitan detectar problemas de programación es de utilidad tanto para el docente, el cual puede probar de una forma más exhaustiva las prácticas entregadas, como para el discente, el cual puede utilizar dichas herramientas. En muchos casos, existen herramientas previas utilizadas en el desarrollo software, que pueden ser adaptadas para ser utilizadas en un entorno formativo. Este trabajo aporta la integración de una herramienta de validación formal de sistemas concurrentes Java, la cual garantiza la no existencia de defectos como son el abrazo mortal y las condiciones de carrera, en un entorno Web abierto. Más concretamente, la herramienta que se ha escogido es denominada JPF (Java Path Finder) y se la ha dotado de interfaces dentro de un servidor Java EE (Enterprise Edition), lo que facilita la utilización de servicios propios de la plataforma Java EE y la interoperabilidad entre estos con el módulo diseñado. El artículo trata aspectos tecnológicos derivados de dicha integración como son el diseño de una arquitectura que da soporte a la validación vía web. También detalla una serie de experimentos relativos al rendimiento de la plataforma realizados sobre un curso real, lo que permite medir costes computacionales y su utilidad en la evaluación

Palabras clave:
Herramientas
Informática Industrial
Validación Formal
Sistemas Concurrentes
Educación
Java
Abstract

Tools that allow detecting programming faults are useful for both docents, who may test submitted exercises, and students, who may use these tools in advance. In this article the authors develop one tool for detecting failures in applications. In many cases there are previous tools that may be readapted to be used in an educational scope. This article integrates of one of these tools, which avoids code with dead-locks and race-conditions, into the Internet. The tool integrated is JPF (Java Path Finder) and it is accessed from a Java EE web frontend which carries out the exercise assessment. The article deals with the definition of the module and its evaluation on a realistic scenario. The results show that many assignments may benefit from the output of the tool.

Keywords:
Tools
Industrial Informatics
Formal Validation
Concurrent Systems
Education
Java
Referencias
[Alonso et al., 2004]
Alonso D., Pastor, J.A., Alvarez, B., 2004. Real-Time Teaching with Java: JPR 3. En: OTM Workshops. Larnaca (Chipre).
[Basanta-Val et al., 2010]
Basanta-Val, P., Garcia-Valls, M. y Estevez-Ayres, I., 2010. No-Heap remote objects for distributed real-time Java. ACM Trans.Embed.Comput.Syst. 10 (1): 1-25.
[Basanta-Val et al., 2005]
Basanta-Val, P., Garcia-Valls, M. y Estevez-Ayres, I., 2005. Towards the Integration of Scoped Memory in Distributed Real-Time Java. ISORC 2005. Seatle(US).
[Basanta-Val et al., 2004]
Basanta-Val, P., Garcia-Valls, M. y Estevez-Ayres, I., 2004. No Heap remote objects: Leaving the garbage collector at the server-side. En: OTM Workshops. Larnaca (Chipre).
[Bollella et al., 2001]
Bollella G. et al., 2001. The Real-Time Specification for Java, Adisson- Wesley.
[Caspi et al., 2005]
Caspi P., Sangiovanni-Vincentelli, A.L, Almeida, L., Benveniste, A., Bouyssounouse, B., Buttazzo, G.C., Crnkovic, I., Damm, W., Engblom, J., Fohler, G., García-Valls, M., Kopetz, H., Lakhnech, Y., Laroussinie, F., Lavagno, L., Lipari, G., Maraninchi, F., Peti, P., de la Puente, J.A, Scaife, N., Sifakis, J., de Simone, R., Törngren, M., Veríssimo, P., Wellings, A.J., Wilhelm, R., Willemse, Wang Yi, T.A.C., 2005. Guidelines for a graduate curriculum on embedded software and systems. ACM Trans. Embedded Comput. Syst. 4 (3) 587-611

.
[de La Puente et al., 1998]
de La Puente, J., Alonso, A., Garcia-Valls, M., Ruiz, J.F., 1998. Teaching real-time systems at DIT/UPM, En: Real-Time Systems, Montreal (Canada).
[de Tomas et al., 1991]
de Tomas, M.A., Gomez, L., Perez A., 1991. Vestal: a tool for teaching concurrency in Ada. En: Proceedings of the conference on TRI-Ada’91: today's accomplishments; tomorrow's expectations. USA.
[Estévez-Ayres et al., 2004]
Estévez-Ayres, I., Basanta-Val, P., García-Valls, M., 2004. Docencia de Programación Concurrente. Experiencias de laboratorio. En: VII Jornadas de Tiempo Real. Málaga, Spain.
[García-Valls et al., 2012]
García-Valls, M., Alonso, A., De La Puente, J.A., 2012. A dual-band priority assignment algorithm for dynamic QoS resource management. Accepted in Future Generation Computer Systems. doi:10.1016/j.future.2011.10.005 Glassfish, Servidor GlassFish, disponible en octubre del 2011 desde http://glassfish.java.net.
[Guaspari et al., 1990]
Guaspari, D., Marceau, C., Polak, W., 1990. Formal Verification of Ada Programs. IEEE Transactions on Software Engineering 16 (9): 1058-1075
[Henzinger et al., 2007]
Henzinger, T.A, Sifakis, J. (2007) The Discipline of Embedded Systems Design. IEEE Computer 40 (10): 32-40.
[Ihantola, 2006]
Ihantola, P., 2006. Test data generation for programming exercises with symbolic execution in Java PathFinder. En: 6° Baltic Sea conference on Computing education research. USA.
[JavaEJB, 2011]
JavaEJB, Enterprise Java Beans Container, disponible en octubre del 2011 desde http http://jcp.org/en/jsr/detail?id=220.
[JavaEE, 2011]
JavaEE, Java Enterprise Edittion, disponible en octubre del 2011 desde oracle.com/technetwork/java/javaee/.
[Java Path Finder, 2011]
JPF. Java Path Finder, disponible en octubre del 2011 desde http://javapathfinder.sourceforge.net.
[JavaServ, 2011]
JavaServ, Java Servlets, disponible en octubre del 2011 desde http://jcp.org/en/jsr/detail?id=340.
[JMail, 2011]
JMail, Java Mail, disponible en octubre del 2011 desde http://jcp.org/en/jsr/detail?id=919.
[JMS, 2011]
JMS, Java Messaging System, disponible en octubre del 2011 desde http://jcp.org/en/jsr/detail?id=914.
[Kalibera et al., 2010]
Kalibera, T., Parizek, P., Malohlava, M., 2010. Exhaustive Testing of Safety.
[Critical et al., 2010]
Critical Java. En: JTRES’10, 2010 Prague,Czech Republic.
[Muñoz-Merino et al., 2009]
Muñoz-Merino, P.J., Delgado-Kloos, C., Fernández-Naranjo, J., 2009. Enabling interoperability for LMS educational services. Computer Standards & Interfaces 31 (2): 484-498
[Rajan et al., 2009]
Rajan, S.P, Tkuchuk, O., Prasad, M., Ghosh, I., Goel, N., 2009. WEAVE: Web Applications Validation Environment. En: ICSE’09. Vancouver (Canada).
[Visser et al., 2004]
Visser, W., Pireanu, C.S., Khurshid, S., 2004. Test input generation with java PathFinder. SIGSOFT Softw. Eng. Notes 29 (4): 97-107
[Visser et al., 2003]
Visser,W., Havelund, K., Brat, G., Park,S., Lerda,. F. Model Checking Programs. Automated Software Engineering Journal. Volume 10, Number 2, April 2003.
[Volanschi, 2008]
Volanschi, N., 2008.A portable compiler-integrated approach to permanent checking. Journal: Automated Software Engineering 15 (1). 21-37.
[Wellings, 2004]
Wellings, A., 2004. Concurrent and Real-Time Programming in Java. Wiley.

www.it.uc3m.es/drequiem.

Copyright © 2011. Elsevier España, S.L.. Todos los derechos reservados
Opciones de artículo
Herramientas