{rfName}
Sy

Indexed in

Citations

9

Altmetrics

Analysis of institutional authors

Marino, JulioAuthorFredlund, Lars-AkeAuthorHerranz, AngelAuthor

Share

June 9, 2019
Publications
>
Article
No

Synthesis of verifiable concurrent Java components from formal models

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

Authors:

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

Affiliations

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

Abstract

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.
[+]

Keywords

ConcurrencyCspJavaJcspJmlKeyMessage passingModel-drivenShared resourcesVerification

Quality index

Bibliometric impact. Analysis of the contribution and dissemination channel

The work has been published in the journal Software and Systems Modeling due to its progression and the good impact it has achieved in recent years, according to the agency WoS (JCR), it has become a reference in its field. In the year of publication of the work, 2019, it was in position 45/108, thus managing to position itself as a Q2 (Segundo Cuartil), in the category Computer Science, Software Engineering. Notably, the journal is positioned 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
[+]

Impact and social visibility

From the perspective of influence or social adoption, and based on metrics associated with mentions and interactions provided by agencies specializing in calculating the so-called "Alternative or Social Metrics," we can highlight as of 2026-04-24:

  • The use, from an academic perspective evidenced by the Altmetric agency indicator referring to aggregations made by the personal bibliographic manager Mendeley, gives us a total of: 10.
  • The use of this contribution in bookmarks, code forks, additions to favorite lists for recurrent reading, as well as general views, indicates that someone is using the publication as a basis for their current work. This may be a notable indicator of future more formal and academic citations. This claim is supported by the result of the "Capture" indicator, which yields a total of: 10 (PlumX).

With a more dissemination-oriented intent and targeting more general audiences, we can observe other more global scores such as:

  • The Total Score from Altmetric: 1.
  • The number of mentions on the social network X (formerly Twitter): 1 (Altmetric).

It is essential to present evidence supporting full alignment with institutional principles and guidelines on Open Science and the Conservation and Dissemination of Intellectual Heritage. A clear example of this is:

  • Assignment of a Handle/URN as an identifier within the deposit in the Institutional Repository: https://oa.upm.es/94514/

As a result of the publication of the work in the institutional repository, statistical usage data has been obtained that reflects its impact. In terms of dissemination, we can state that, as of

  • Views: 16
  • Downloads: 11
[+]

Leadership analysis of institutional authors

There is a significant leadership presence as some of the institution’s authors appear as the first or last signer, detailed as follows: First Author (MARIÑO CARBALLO, JULIO) and Last Author (HERRANZ NIEVA, ANGEL).

[+]

Awards linked to the item

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).
[+]