ABSTRACT
This chapter treats distributed systems in a rather formal way. It presents an overview of the models commonly used for specifying properties of a distributed system. The purpose of a model is to precisely define specific properties or characteristics of a system to be built or analyzed and to provide the foundation for verifying these properties. Petri net can be analyzed to determine whether correct termination of a distributed system will always occur or whether the possibility of a deadlock exists. The chapter explores concepts of clock, event, state, and time is introduced in a rather informal way. It considers two applications of formal models: One is the application of a total ordering on a distributed mutual exclusion and the other is the application of logical vector clocks on ordering of messages.
