FORMAL METHODS AND DESIGN EXTRACTION - A PILOT-STUDY

In this paper we show, using a small example, how a formal description can be generated from existing informal documents. The aim is to illu strate the possibilities and limitations of using CCS and the concurre ncy workbench within the context of teaching software maintenance. We consider the conversion of systems described using programs and inform al specifications into CCS processes. The testing of the CCS specifica tions using modal-mu logic formulae is described; and the process of t esting can be simplified by providing the tester with suitable macros. The advantage of using CCS and the concurrency workbench is that one can automate the entire testing process; the disadvantage is that one can consider only small restricted sub-systems.