{rfName}
Sy

Indexado en

Citaciones

9

Altmetrics

Investigadores/as Institucionales

Marino, JulioAutor o CoautorFredlund, Lars-AkeAutor o CoautorHerranz, AngelAutor o Coautor

Compartir

9 de junio de 2019
Publicaciones
>
Artículo
No

Synthesis of verifiable concurrent Java components from formal models

Publicado en: Software and Systems Modeling. 18 (1): 71-105 - 2019-02-08 18(1), DOI: 10.1007/s10270-017-0581-1

Autores:

Mariño, J; Alborodo, RNN; Fredlund, LÅ; Herranz, A
[+]

Afiliaciones

IMDEA Software Inst, Madrid 28223, Spain - Autor o Coautor
Univ Politecn Madrid, Sch Comp Sci & Engn, E-28660 Madrid, Spain - Autor o Coautor

Resumen

Concurrent systems are hard to program, and ensuring quality by means of traditional testing techniques is often very hard as errors may not show up easily and reproducing them is hard. In previous work, we have advocated a model-driven approach to the analysis and design of concurrent, safety-critical systems. However, to take full advantage of these techniques, they must be supported by code generation schemes for concrete programming languages. Ideally, this translation should be traceable, automated and should support the verification of the generated code. In our work, we consider the problem of generating a concurrent Java component from a high-level model of inter-process interaction (i.e., communication + synchronization). We call our formalism shared resources. From the model, which can be represented in mathematical notation or written as a Java interface annotated using an extension of JML, a Java component can be obtained by a semiautomatic translation. We describe how to obtain shared memory (using a priority monitors library) and message passing (using the JCSP library) implementations. Focusing on inter-process interaction for formal development is justified by several reasons, e.g., mathematical models are language-independent and allow to analyze certain concurrency issues, such as deadlocks or liveness properties prior to code generation. Also, the Java components produced from the shared resource model will contain all the concurrency-related language constructs, which are often responsible for many of the errors in concurrent software. We follow a realistic approach where the translation is semiautomatic (schemata for code generation) and the programmer still retains the power of coding or modifying parts of the code for the resource. The code thus obtained is JML-annotated Java with proof obligations that help with code traceability and verification of safety and liveness properties. As the code thus obtained is not automatically correct, there is still the need to verify its conformance to the original specs. We illustrate the methodology by developing a concurrent control system and verifying the code obtained using the KeY program verification tool. We also show how KeY can be used to find errors resulting from a wrong use of the templates.
[+]

Palabras clave

ConcurrencyCspJavaJcspJmlKeyMessage passingModel-drivenShared resourcesVerification

Indicios de calidad

Impacto bibliométrico. Análisis de la aportación y canal de difusión

El trabajo ha sido publicado en la revista Software and Systems Modeling debido a la progresión y el buen impacto que ha alcanzado en los últimos años, según la agencia WoS (JCR), se ha convertido en una referencia en su campo. En el año de publicación del trabajo, 2019, se encontraba en la posición 45/108, consiguiendo con ello situarse como revista Q2 (Segundo Cuartil), en la categoría Computer Science, Software Engineering. Destacable, igualmente, el hecho de que la Revista está posicionada en el Cuartil Q2 para la agencia Scopus (SJR) en la categoría Software.

Independientemente del impacto esperado determinado por el canal de difusión, es importante destacar el impacto real observado de la propia aportación.

Según las diferentes agencias de indexación, el número de citas acumuladas por esta publicación hasta la fecha 2026-04-24:

  • Google Scholar: 5
  • WoS: 2
  • Scopus: 2
[+]

Impacto y visibilidad social

Desde la dimensión de Influencia o adopción social, y tomando como base las métricas asociadas a las menciones e interacciones proporcionadas por agencias especializadas en el cálculo de las denominadas “Métricas Alternativas o Sociales”, podemos destacar a fecha 2026-04-24:

  • El uso, desde el ámbito académico evidenciado por el indicador de la agencia Altmetric referido como agregaciones realizadas por el gestor bibliográfico personal Mendeley, nos da un total de: 10.
  • La utilización de esta aportación en marcadores, bifurcaciones de código, añadidos a listas de favoritos para una lectura recurrente, así como visualizaciones generales, indica que alguien está usando la publicación como base de su trabajo actual. Esto puede ser un indicador destacado de futuras citas más formales y académicas. Tal afirmación es avalada por el resultado del indicador “Capture” que arroja un total de: 10 (PlumX).

Con una intencionalidad más de divulgación y orientada a audiencias más generales podemos observar otras puntuaciones más globales como:

  • El Score total de Altmetric: 1.
  • El número de menciones en la red social X (antes Twitter): 1 (Altmetric).

Es fundamental presentar evidencias que respalden la plena alineación con los principios y directrices institucionales en torno a la Ciencia Abierta y la Conservación y Difusión del Patrimonio Intelectual. Un claro ejemplo de ello es:

  • Asignación de un Handle/URN como identificador dentro del Depósito en el Repositorio Institucional: https://oa.upm.es/94514/

Como resultado de la publicación del trabajo en el repositorio institucional, se han obtenido datos estadísticos de uso que reflejan su impacto. En términos de difusión, podemos afirmar que, hasta la fecha

  • Visualizaciones: 16
  • Descargas: 11
[+]

Análisis de liderazgo de los autores institucionales

Existe un liderazgo significativo ya que algunos de los autores pertenecientes a la institución aparecen como primer o último firmante, se puede apreciar en el detalle: Primer Autor (MARIÑO CARBALLO, JULIO) y Último Autor (HERRANZ NIEVA, ANGEL).

[+]

Reconocimientos ligados al ítem

This research has been partially funded by Comunidad de Madrid grant S2013/ICE-2731 (N-Greens Software) and Spanish MINECO grant TIN2012-39391-C04-03 (StrongSoft).
[+]