会话类型监视器 围绕库构建的Scala中通信协议的混合验证方法。 (如本文。) 在给定会话类型S的情况下,该工具可以综合类型检查监视器的Scala代码,该监视器在运行时验证交互是否遵守S以及可用于实现根据S进行交互的过程的签名。 生成的监视器嵌入有会话类型中指定的运行时数据检查。 可以在找到概述我们的方法的演示文稿。 这些指令用于重新创建和执行本文中的示例(即登录示例)。 我们假设使用Java 8作为默认JRE / JDK的类Unix操作系统,可以从下载。 编译源代码 该项目使用sbt构建工具,可从下载(sbt v。0.13.x)。 安装完成后,在stmonitor/ *中打开一个终端,然后执行命令sbt compile 。 *此后的所有命令都必须在此位置执行。 登录示例 1.综合监视器和CPSP类。 考虑登录示例,其中服务器必须遵循auth.st找到的类型: S_auth=re