P：一种用于异步事件驱动编程和模型检查的语言

P是一种用于异步事件驱动编程的语言。P允许程序员将系统指定为交互状态机的集合，这些状态机使用事件相互通信。P将建模和编程统一到程序员的一项活动中。不仅可以将P程序编译成可执行代码，而且还可以使用模型检查对其进行系统测试。P已用于实现和验证Microsoft Windows 8和Windows Phone附带的USB设备驱动程序堆栈。目前，p在亚马逊(Amazon，AWS)内部被广泛用于复杂分布式系统的模型检查。

“动态分布式系统的组合编程和测试”，Ankush Desai，Amar Phanishayee，Shaz Qadeer，and Sanjit Seshi.面向对象编程，系统，语言，和应用程序国际会议(OOPSLA)，2018。

“Drona：一种安全的分布式移动机器人框架”，Ankush Desai，Indranil Saha，杨建桥，Shaz Qadeer，Sanjit A.Seshi.在第八届ACM/IEEE国际网络物理系统会议(ICCPS)上，2017.。

“异步反应式系统的系统测试”，Ankush Desai，Shaz Qadeer，and Sanjit A.Seshi.在2015年第10届软件工程基础联席会议(ESEC/FSE 2015)论文集上.。

“安全异步事件驱动编程”，Ankush Desai，Vivek Gupta，Ethan Jackson，Shaz Qadeer，Sriram Rajamani，和Damien Zuffere.ACM SIGPLAN Conference on Programming Language Design and Implementation(PLDI)，2013。

观看有趣的演示视频，使用P控制四轴飞行器并理解MavLink流，所有这些都在实时DGML图表中可视化。

我们构建了Drona，一个用于分布式移动机器人系统的软件框架。Drona使用P语言实现和模型检查分布式机器人软件堆栈(Wiki)。从P编译器生成的C代码可以很容易地部署在机器人操作系统(ROS)上。有关DRONA框架和模拟视频的更多详细信息，请单击此处：https://drona-org.github.io/Drona/