DOI:
Abstract:
Our goal is to demonstrate that the NUPRLPE is capable of supporting the formal design and implementation of large-scale, high-performance network systems. We have already used the NUPRLPE in the verification of protocols for the ENSEMBLE group communication toolkit (Kreitz, Hayden, and Hickey 1998; Hickey, Lynch, and van Renesse 1999), in verifiably correct optimizations of ENSEMBLE protocol stacks (Kreitz 1999; Liu et al. 1999), and in the formed design and implementation of new adaptive network protocols (Liu et al. 2001; Bickford et al. 2001a; 2001b). Currently we are working on providing formal support for the development of large distributed embedded systoms.