Code Generation From Hierarchical Concurrency SpecificationsReportar como inadecuado

Code Generation From Hierarchical Concurrency Specifications - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

1 MODEL - MODEL Méthodes formelles et applications LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications

Abstract : This paper explains how executable Java code is generated from hierarchical specifications in the Concurrency Factory specification and verification environment. Besides the ability to generate executable code from verified, abstract concurrency specifications, the paper-s main contributions include: 1 new solutions to the well-known input-output guard-scheduling problem in the context of hierarchically configured concurrent systems; 2 code-generation algorithms that produce both thread-based Java code and distributed ADA code; 3 the use of the Concurrency Factory itself to verify an abstraction of each generated code module; in this sense, the Factory is self-verifying; and, finally, 4 a report on our experience in executing the generated code for simulation and debugging purposes in the case of the Rether real-time ethernet protocol.

keyword : proofs code generation spécification preuves génération de code

Autor: Denis Roegel - Scott Smolka



Documentos relacionados