Open Distributed Systems: On Concepts, Methods, and Design from a Logical Point of View (Paperback, 1993)

0 Introduction.- 0.1 Key topics of open distributed systems design.- 0.2 The role of standards.- 0.3 The need for formal descriptions.- 0.4 Distributed systems from the point of view of DAI.- 1 Formal methods in the system design process.- 1.1 A model for the system design process.- 1.2 Requirements for formal description techniques.- 1.2.1 Expressiveness.- 1.2.2 Abstraction.- 1.2.3 Formality.- 1.2.4 Explicitness and implicitness.- 1.2.5 Compositionality.- 1.3 Synthesis and analysis activities.- 2 Requirement specification of open distributed systems.- 2.1 Basic architectural concepts.- 2.2 System architectures.- 2.3 Refinement and abstraction.- 2.4 The Basic Reference Model of Open Systems Interconnection.- 2.5 Basic concepts of formal description techniques.- 2.6 Some remarks.- 3 The design of a temporal logic for open distributed systems.- 3.1 Some requirements on expressiveness.- 3.2 A survey of temporal logics.- 3.2.1 Traditional temporal logic.- 3.2.2 Extensions of traditional temporal logic.- 3.2.3 Past time temporal logic.- 3.2.4 Branching time temporal logic.- 3.2.5 Interval logic.- 3.2.6 Incorporation of events.- 3.2.7 The impact of validity.- 3.3 A modular temporal logic for open distributed systems.- 3.3.1 Semantical models.- 3.3.2 Atomic formulas and non-temporal operators.- 3.3.3 Operators to refer to the future.- 3.3.4 Operators to refer to the past.- 3.3.5 Operators for event occurrence.- 3.3.6 Operators for interval construction.- 3.3.7 Customizing temporal logics.- 3.3.8 Composition of behavioural specifications.- 3.3.9 A notion of conformance.- 4 The interaction point concept.- 4.1 The role of interaction points.- 4.2 A list of possible interaction point properties.- 4.3 Formal specification of interaction point properties.- 4.3.1 Context and limitations.- 4.3.2 Customizing an appropriate temporal logic.- 4.3.3 General properties.- 4.3.4 Mode of interaction.- 4.3.5 Inspection.- 4.3.6 Summary.- 4.4 Formal reasoning about interaction points.- 4.5 Interaction point representations in operational FDTs.- 4.5.1 Interaction points in Estelle.- 4.5.2 Interaction points in LOTOS.- 4.5.3 Interaction points in SDL.- 4.5.4 Summary.- 4.6 Conformance between abstraction levels via the interaction point concept.- 4.6.1 Problems with an environment-independent notion of conformance.- 4.6.2 Compatibility between interaction points.- 4.6.3 Environment-independent conformance based on interaction point compatibility.- 4.6.4 Application to OSI.- 5 Communication services.- 5.1 The service concept.- 5.2 Design methodology.- 5.3 Example “modified InRes service”.- 5.3.1 Informal description.- 5.3.2 Customizing an appropriate temporal logic.- 5.3.3 Specification of the service.- 5.3.4 Specification of the service provider.- 5.3.5 Interaction point semantics.- 5.3.6 Constraints on the service users.- 5.3.7 Verification of the service provider.- 5.4 Conclusion.- 6 An epistemic logic for open distributed systems.- 6.1 The role of knowledge.- 6.2 Notions of knowledge.- 6.2.1 Possible-worlds semantics.- 6.2.2 Situated-Automata Knowledge.- 6.2.3 View-based knowledge interpretation.- 6.2.4 Group knowledge.- 6.2.5 Awareness.- 6.3 A modular epistemic logic for open distributed systems.- 6.3.1 Semantical models.- 6.3.2 Operators for implicit individual knowledge.- 6.3.3 Operators for explicit individual knowledge.- 6.3.4 Operators for individual awareness.- 6.3.5 Operators for implicit group knowledge.- 6.3.6 Operators for group awareness.- 6.3.7 Operators for explicit group knowledge.- 6.3.8 Customizing temporal epistemic logics.- 6.3.9 Some remarks on conformance.- 7 Applying temporal epistemic logics to open distributed systems.- 7.1 Example “mutual exclusion”.- 7.1.1 Implicit knowledge.- 7.1.2 Knowledge-oriented specification.- 7.1.3 Explicit knowledge.- 7.2 Example “drink server”.- 7.2.1 Specification based on propositional logic.- 7.2.2 Refinement.- 7.2.3 Verification of the drink server refinement.- 7.2.4 Specification based on first-order logic.- 7.2.5 Refinement.- 7.2.6 Verification of the drink server refinement.- 7.2.7 Non-local epistemic properties.- 8 Conclusion.- References.- A.1 Theorems and valid formulas.- A.2 Ordering properties for the service provider.- A.3 Abbreviations.- A.4 Notation.