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
- Model-Driven Verifying Compilation of Synchronous Distributed Applications, Sagar Chaki, James Edmondson, Proceedings of the ACM/IEEE 17th International Conference on Model Driven Engineering Languages and Systems (MODELS), Sep 28-Oct 3, 2014, Valencia, Spain.
- Toward Parameterized Verification of Synchronous Distributed Applications, Sagar Chaki, James Edmondson, Proceedings of the 21st International SPIN Symposium on Model Checking of Software (SPIN), July 21-23, 2014, San Jose, CA, USA.
Getting Involved
Contact James Edmondson or Sagar Chaki.