MCDA

Model Checking Distributed Applications

View project on GitHub

In the Model Checking for Distributed Applications (MCDA) project, we are developing tools and demonstrations for producing verifiably correct distributed applications (i.e., software implementing distributed algorithms) with safety-critical requirements. Our current focus is on applications where nodes are mobile and communicate wirelessly. A canonical example is a team of robots sharing a physical area that must achieve a goal without collisions. Here are some videos (quadcopter, ant) of verified distributed collision avoidance protocols developed using our approach.


Approach

We have developed a domain specific language -- called DASL -- for writing distributed applications and their safety properties assuming synchronous network communication. We have also developed a verifying compiler for DASL programs -- called daslc -- that first verifies a DASL program against its safety property using Software Model Checking (we are currently using CBMC). If the verification succeeds, daslc generates C++ code for the program against the MADARA middleware. MADARA ensures the synchronous network abstraction assumed by the application even if the underlying network is asynchronous with unbounded latency. daslc can also generate code that can be simulated with the V-REP simulator. See our tutorial for details.


Using

Download and compile the source code, follow the installation instructions, and then follow the tutorial. Also, check out the LICENSE.


Papers


Getting Involved

Contact James Edmondson or Sagar Chaki.