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

P. Basanta Val

Spain

Universidad Carlos III de Madrid

Departamento de Ingeniería Telemática

M. García Valls

Spain

Universidad Carlos III de Madrid

Departamento de Ingeniería Telemática

I. Estévez Ayres

Spain

Universidad Carlos III de Madrid

Departamento de Ingeniería Telemática

M.J. Martin Gutiérrez

Spain

Universidad Carlos III de Madrid

Departamento de Ingeniería Telemática

Enviado: 09-02-2018

|

Aceptado: 09-02-2018

|
DOI: https://doi.org/10.1016/j.riai.2012.05.013
Datos de financiación

Descargas

Palabras clave:

Herramientas, Informática Industrial, Validación Formal, Sistemas Concurrentes, Educación, Java

Agencias de apoyo:

Ministerio de Industria

Comercio y Turismo español. iLAND (ARTEMIS-JU 100026). ARTISTDesign NoE (IST-2007-214373) del 7º programa marco de la Unión Europea. Ministerio de Ciencia e Innovación y por LEARN3(TIN2008-0513) del Ministerio de Ciencia e Innova

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.
Ver más Ver menos

Citas:

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.

Ver más Ver menos