|
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 |