DLC: Compiling a Concurrent System Formal Specification to a Distributed Implementation

International audienceFormal methods can verify the correctness of a concurrentsystem by analyzing its model. However, if the actual implementation iswritten by hand, subtle and hard to detect bugs may be unintentionallyintroduced, thus ruining the verification effort. In this paper, we presentDLC (Distributed LNT Compiler), a tool that automatically generatesdistributed implementation of concurrent systems modeled in the LNTlanguage, which can be formally verified using the CADP toolbox