论文部分内容阅读
生产者与消费者系统（PCS）是一个经典的进程同步问题，Hocine等学者运用抽象状态机（ASMs）对该问题进行了时序规约。文中主要使用TLA语言对PCS给出了一个时序规约模型，并且利用模型检测工具TLC对PCS进行检测。同时对系统的活性和互斥性也进行了检测，检测结果都满足系统规约。ASMs主要采用转移规则来规约PCS模型，中间的转移过程是无法知道的，TLA能同时规约出PCS的执行过程和系统属性。