Open distributed systems : on concepts, methods, and design from a logical point of view
著者
書誌事項
Open distributed systems : on concepts, methods, and design from a logical point of view
(Vieweg advanced studies in computer science)
Vieweg, c1993
大学図書館所蔵 全5件
  青森
  岩手
  宮城
  秋田
  山形
  福島
  茨城
  栃木
  群馬
  埼玉
  千葉
  東京
  神奈川
  新潟
  富山
  石川
  福井
  山梨
  長野
  岐阜
  静岡
  愛知
  三重
  滋賀
  京都
  大阪
  兵庫
  奈良
  和歌山
  鳥取
  島根
  岡山
  広島
  山口
  徳島
  香川
  愛媛
  高知
  福岡
  佐賀
  長崎
  熊本
  大分
  宮崎
  鹿児島
  沖縄
  韓国
  中国
  タイ
  イギリス
  ドイツ
  スイス
  フランス
  ベルギー
  オランダ
  スウェーデン
  ノルウェー
  アメリカ
注記
Includes bibliographical references (p. [201]-208) and index
内容説明・目次
内容説明
This work presents a new, abstract and comprehensive view of open distributed systems. The starting point is a small number of core concepts and basic principles, which are informally introduced and precisely defined using mathematical logic. It is shown how the basic concepts of open systems interconnection (OSI), which are currently the most important standardization activities in the context of open distributed systems, can be obtained by specialization and extension of these basic concepts. Application examples include the formal treatment of the interaction point concept and the hierarchical development of communication systems. This book is a contribution to the field of software engineering in general and to the design of open distributed systems in particular. It is oriented towards the design and implementation of real systems, and brings together both formal logical reasoning and current software engineering practice.
目次
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.
「Nielsen BookData」 より