P

P是一种基于状态机的编程语言，用于形式化建模和指定复杂的分布式系统。P允许程序员将系统设计建模为一组通信的状态机。P支持多种后端分析引擎（基于模型检测、符号执行等自动化推理技术），以验证用P建模的分布式系统是否满足预期的正确性规范。

P是一种由微软与加州大学伯克利分校共同开发的异步事件驱动编程语言，专为物联网应用设计。

P语言经过精心设计，可检查所设计的系统是否具有响应性，即能够及时处理每个事件。默认情况下，状态机必须在每个状态下处理所有到达的事件。默认的安全性检查器会查找违反此规则的情况。有时，在每个状态下处理所有事件并不实际，语言提供了“延迟事件”的概念，允许程序员显式标注何时推迟处理某个事件。同时，语言还提供默认的活性检查，确保事件不会被无限期地延迟。调用转换（类似于子程序）用于提取公共的事件处理代码，使程序员能够编写复杂的有限状态机。

P曾被用于实现并验证随Microsoft Windows 8发布的USB设备驱动栈的核心部分。该驱动比之前的版本（未使用P）更加可靠且性能更优，由于P提供的语言抽象和验证能力，我们对其实现设计的鲁棒性更有信心。

P：一种用于编写异步事件驱动程序的领域特定语言。这种异步语言倡导一种编程范式，要求显式声明事件延迟，从而促进构建响应式系统。本工作的主要技术贡献是一种异步模型，强制队列中的每个事件在关联的状态机被调度时立即处理，并有机会从队列中取出该事件。系统的验证器会系统性地探索各状态机的状态空间，确保不存在未处理的事件。在某些情况下，例如处理高优先级事件，或在事务期间处理一系列事件交换时，可能需要临时排队其他低优先级事件。P提供了延迟事件等功能，供程序员显式指定此类延迟。