Code Generation From Hierarchical Concurrency Specifications
Résumé
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.
Domaines
Autre [cs.OH]
Loading...