Observatorio de I+D+i UPM

Memorias de investigación
Ponencias en congresos:
A Model-driven Methodology for Generating and Verifying CSP-based Java Code
Año:2015
Á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 software. 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 \emph{traceable}, \emph{automated} and should support \emph{verification} of the generated code. In this paper we consider the problem of generating concurrent Java code from high-level interaction models. Our proposal 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. %An essential feature is that the 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
Nombre congreso
Communicating Process Architectures, CPA 2015
Tipo de participación
960
Lugar del congreso
Canterbury, UK
Revisores
Si
ISBN o ISSN
978-0-9565409-9-7
DOI
Fecha inicio congreso
23/08/2015
Fecha fin congreso
26/08/2015
Desde la página
85
Hasta la página
108
Título de las actas
Communicating Process Architectures, CPA 2015
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)