摘要
利用通信系统演算CCS(Calculus of Communicating Systems),对用来解决进程间通信问题的信号量给出了形式化建模和验证的方法,并利用该方法对以信号量机制解决生产者—消费者问题和哲学家进餐问题进行建模、逻辑说明和验证。该方法具有一定通用性,并可将其推广到其他通过信号量机制解决进程通信的问题当中。
The method of formal modeling and validating the semaphore has been given by utilizing CCS（calculus of communicating systems）.The semaphore is used to resolve communication issue between the processes.This method is also applied to the issues of resolving producer-consumer problem and dining problem of the philosophers with semaphore mechanism in modeling,logically illustration and validation.The method has certain universality and can be extended to other issues which also use semaphore mechanism to resolve the process communications.
出处
《计算机应用与软件》
CSCD
2011年第8期230-233,共4页
Computer Applications and Software
关键词
信号量
CCS(通信系统演算)
同步树
形式化建模
进程代数
Semaphore CCS（calculus of communicating systems） Synchronization tree Formal model Process algebra
