An integrated framework for formal development of open distributed systems

This paper contributes to the discussion on issues related to the formal development of open distributed systems (ODS). The deficiencies of traditional formal notations in this setting are highlighted. We argue that there is no single formalism exhibiting all the features required to capture properties of ODSs. As a solution, we propose an integrated development framework that involves two notations: the Unified Modeling Language (UML) and the Prototype Verification System (PVS). We discuss the motivation for the choice of these notations, provide an overview of a CASE tool we have developed to support the proposed framework, and present a case study to demonstrate our approach.