In this paper we present a process algebra approach for the
integrated verification of correctness and performance in concurrent
systems.
The verification procedure is entirely performed within the Circal
process algebra, without any recourse to other formalisms.
Performance is characterised in terms of logical properties,
which do not incorporate explicit time.
Such properties are then interpreted in terms of degree of concurrency
and allow the quantitative evaluation of the throughput of the system.
The approach has been applied to two four-phase handshaking protocols,
which are motivated by the implementation of the AMULET2 asynchronous
RISC processor.
Both correctness and performance properties are captured in the
same verification framework and automatically proved using the
Circal System.
