Formal specification of concurrent systems

This paper presents a formal methodology for developing concurrent systems. We extend the Larch family of specification languages and tools with the C CS process algebra to support the specification and verification of concurr ent systems. We present and follow a refinement strategy that relates an im plementation ina programming language to a formal specification of such a s ystem. We illustrate our methodology on an example that uses the preconditi oned conjugate gradient method for solving a linear system of equations. (C ) 1998 Elsevier Science Ltd. All rights reserved.