Stepwise refinement of control software — A case study using RAISE

We develop a control program for a realistic automation problem by stepwise refinement. We focus on exemplifying appropriate levels of abstraction for the refinement steps. By using phases as a means for abstraction, safety requirements are specified on a high level of abstraction and can be verified using process algebra. The case study is carried out using the RAISE specification language, and we report on some experiences using the RAISE tool set.