Módulo Empresarial para la Validación Formal de Ejercicios aplicado a la Programación Concurrente en Java

P. Basanta Val, M. García Valls, I. Estévez Ayres, M.J. Martin Gutiérrez
DOI: https://doi.org/10.1016/j.riai.2012.05.013

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

Texto completo:

PDF

Referencias

Alonso D., Pastor, J.A., Alvarez, B., 2004. Real-Time Teaching with Java: JPR 3. En: OTM Workshops. Larnaca (Chipre)

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, 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, 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 G., et al., 2001. The Real-Time Specification for Java, AdissonWesley.

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, 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, 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, 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, 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, D., Marceau, C., Polak, W., 1990. Formal Verification of Ada Programs. IEEE Transactions on Software Engineering 16(9), 1058-1075

Henzinger, T.A, Sifakis, J. (2007) The Discipline of Embedded Systems Design. IEEE Computer 40(10): 32-40.

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, Enterprise Java Beans Container, disponible en octubre del 2011 desde http http://jcp.org/en/jsr/detail?id=220

JavaEE, Java Enterprise Edittion, disponible en octubre del 2011 desde oracle.com/technetwork/java/javaee/

JPF. Java Path Finder, disponible en octubre del 2011 desde http://javapathfinder.sourceforge.net

JavaServ, Java Servlets, disponible en octubre del 2011 desde http://jcp.org/en/jsr/detail?id=340

JMail, Java Mail, disponible en octubre del 2011 desde http://jcp.org/en/jsr/detail?id=919

JMS, Java Messaging System, disponible en octubre del 2011 desde http://jcp.org/en/jsr/detail?id=914

Kalibera, T. Parizek, P., Malohlava, M., 2010. Exhaustive Testing of Safety Critical Java. En: JTRES’10, 2010 Prague, Czech Republic

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, S.P, Tkuchuk, O., Prasad, M., Ghosh, I., Goel, N., 2009. WEAVE: Web Applications Validation Environment. En: ICSE’09. Vancouver (Canada).

Visser, W., Pireanu, C.S., Khurshid, S., 2004. Test input generation with java PathFinder. SIGSOFT Softw. Eng. Notes 29(4), 97-107.

Visser, W., Havelund, K., Brat, G., Park,S., Lerda,. F. Model Checking Programs. Automated Software Engineering Journal. Volume 10, Number 2, April 2003.

Volanschi, N., 2008.A portable compiler-integrated approach to permanent checking. Journal: Automated Software Engineering 15(1) 21-37

Wellings, A., 2004. Concurrent and Real-Time Programming in Java. Wiley.

Abstract Views

571
Metrics Loading ...

Metrics powered by PLOS ALM


Bookmark and Share

 

Citado por (artículos incluidos en Crossref)

This journal is a Crossref Cited-by Linking member. This list shows the references that citing the article automatically, if there are. For more information about the system please visit Crossref site

1. Herramienta Web Ligera para La Programación en C-Concurrente
Pablo Basanta-Val, Marisol García-Valls, Pablo López-Anastasio
Revista Iberoamericana de Automática e Informática Industrial RIAI  vol: 10  num.: 4  primera página: 465  año: 2013  
doi: 10.1016/j.riai.2013.05.010



Creative Commons License

Esta revista se publica bajo una Licencia Creative Commons Attribution-NonCommercial-CompartirIgual 4.0 International (CC BY-NC-SA 4.0)

Universitat Politècnica de València     https://doi.org/10.4995/riai

e-ISSN: 1697-7920     ISSN: 1697-7912