O mecanismo dos semáforos é um pouco complexo de ser implementado como mostraram os exemplos. Por outro lado, a aplicação deste mecanismo é fundamental em situações onde o acesso a recursos compartilhados deve ser feito de maneira exclusiva entre processo. Neste caso, deve ser possível demonstrar que este acesso exclusivo aos recursos é garantido, que não existe inter-bloqueio entre processos concorrendo pelos recursos e que esta concorrência é justa (ou seja, deve ser garantido que todos os processos têm a mesma chance de adquirir o recurso compratilhado). Se esta análise parece complicada usando os semáforos de Dijkstra, ele será muito mais delicada em aplicações concorrentes gerais usando todo o espectro primitivas IPC. A utilização de abordagens formais para a concepção e análise deste tipo de aplicação torna-se desta forma, fundamental.