Observatorio de I+D+i UPM

Memorias de investigación
Capítulo de libro:
A Model-driven Methodology for Generating and Verifying CSP-based Java Code
Año:2018
Áreas de investigación
  • Ciencias de la computación y tecnología informática
Datos
Descripción
Model-driven methodologies can help developers create more reliable soft- ware. In previous work, we have advocated a model-driven approach for the analysis and design of concurrent, safety-critical systems. However, to take full advantage of those techniques, they must be supported by code generation schemes for concrete programming languages. Ideally, this translation should be traceable, automated and should support verification of the generated code. In this paper we consider the prob- lem of generating concurrent Java code from high-level interaction models. Our pro- posal includes an extension of JML that allows to specify shared resources as Java interfaces, and several translation patterns for (partial) generation of CSP-based Java code. The template code thus obtained is JML-annotated Java using the JCSP library, with proof obligations that help with both traceability and verification. Finally, we present an experiment in code verification using the KeY tool.
Internacional
Si
DOI
10.3233/978-1-61499-886-0-8
Edición del Libro
Editorial del Libro
IOS Press
ISBN
978-1-61499-885-3
Serie
Título del Libro
Communicating Process Architectures 2015 & 2016
Desde página
87
Hasta página
110
Esta actividad pertenece a memorias de investigación
Participantes
  • Autor: Julio Mariño Carballo (UPM)
Grupos de investigación, Departamentos, Centros e Institutos de I+D+i relacionados
  • Creador: Grupo de Investigación: BABEL: Desarrollo de Software Fiable y de Alta Calidad a partir de Tecnología Declarativa
  • Departamento: Lenguajes y Sistemas Informáticos e Ingeniería de Software
S2i 2021 Observatorio de investigación @ UPM con la colaboración del Consejo Social UPM
Cofinanciación del MINECO en el marco del Programa INNCIDE 2011 (OTR-2011-0236)
Cofinanciación del MINECO en el marco del Programa INNPACTO (IPT-020000-2010-22)