[Artifact] Deductive Verification of Cooperative RTOS Applications

This is the artifact accompanying the paper "Deductive Verification of Cooperative RTOS Applications". It contains case studies, tools and replication instructions used in the experiments for the paper. The artifact comes packaged in a virtual machine image (in artifact-VM.zip) with an appropriate version of the VerCors verifier installed. For convenience, the artifact data are also included separately from the VM (in artifact-contents.zip) for easier inspection. For more detail on contents and usage of the artifact, refer to the included README.<br>The VM has been tested with VirtualBox 7.1.6. Both username and password to the VM are "artifact" (no quotes).

本材料为论文《合作式实时操作系统应用的演绎验证》（Deductive Verification of Cooperative RTOS Applications）的配套实验附件，内含该论文实验环节所使用的案例研究、工具集及实验复现操作指南。
该附件以虚拟机镜像格式打包（打包文件为artifact-VM.zip），其中已预装适配版本的VerCors验证器（VerCors verifier）。为方便用户检视，附件相关数据还脱离虚拟机镜像单独提供（打包文件为artifact-contents.zip）。
如需了解本附件的具体内容与使用细则，请参阅附带的README文件。
本虚拟机镜像已在VirtualBox 7.1.6版本中完成兼容性测试。该虚拟机的用户名与密码均为"artifact"（无需引号）。