Automating SCCS

Abstract

The process of manually checking SCCS formula is time-consuming, repetitive and error prone; one slip at the beginning and the whole thing is wrong. What we need is an automated tool to take out both tedium and errors, and the sort of automated tool we would wish for would be interactive, and intuitive; would help novices to learn about SCCS; would help designers explore the behaviour of SCCS agents; would check the emergent behaviours of combinations of agents; would help us compare both-real time and observational behaviours of agents; and ultimately would check if designs meet their specifications. A tool which goes a long way to meet these objectives is the Concurrency Work Bench (CWB) produced by those nice people at the Laboratory for the Foundation of Computer Science (LFCS), at the University of Edinburgh, and most of this chapter is devoted to its use.