Automatic Distributed Code Generation from Formal Models of Asynchronous Concurrent Processes

8 years 11 days ago

Download convecs.inria.fr

Abstract—Formal process languages inheriting the concurrency and communication features of process algebras are convenient formalisms to model distributed applications, especially when they are equipped with formal veriﬁcation tools (e.g., modelcheckers) to help hunting for bugs early in the development process. However, even starting from a fully veriﬁed formal model, bugs are likely to be introduced while translating (generally by hand) the concurrent model —which relies on high-level and expressive communication primitives— into the distributed implementation —which often relies on low-level communication primitives. In this paper, we present DLC, a compiler that enables distributed code to be generated from models written in a formal process language called LNT, which is equipped with a rich veriﬁcation toolbox named CADP. The generated code can be either executed in an autonomous way (i.e., without requiring additional code to be deﬁned by the user), or connected t...

Hugues Evrard, Frédéric Lang

Real-time Traffic