P is a language for asynchronous event-driven programming. P allows the programmer to specify the system as a collection of interacting state machines, which communicate with each other using events. P unifies modeling and programming into one activity for the programmer. Not only can a P program be compiled into executable code, but it can also be validated using systematic testing. P has been used to implement and validate the USB device driver stack that ships with Microsoft Windows 8 and Windows Phone. P is also suitable for the design and implementation of networked, embedded, and distributed systems.
Check the P manual.
Information for building P framework is available here.
See fun demo video using P to control a quadrocopter and make sense of the MavLink stream, all visualized in a live DGML diagram.
P: Safe asynchronous event-driven programming. Ankush Desai, Vivek Gupta, Ethan Jackson, Shaz Qadeer, Sriram Rajamani, and Damien Zufferey. In Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2013.
Systematic testing of asynchronous reactive systems. Ankush Desai, Shaz Qadeer, and Sanjit A. Seshia. In Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering (ESEC/FSE 2015).
Building Reliable Distributed Systems With P. Ankush Desai, Ethan Jackson, Amar Phanishayee, Shaz Qadeer and Sanjit A. Seshia. University of California, Berkeley.Technical Report No. UCB/EECS-2015-198.