BS ISO/IEC 9074:1997

1 Scope
2 Normative references
3 Definitions
4 Conformance
5 The model
    5.1 Module instance
    5.2 Nesting of modules and parallelism
          5.2.1 Nesting of modules
          5.2.2 Parallelism and nondetermination
    5.3 Specification behavior
          5.3.1 Local situations
          5.3.2 Global instantaneous description of a
                  module instance
          5.3.3 Transitions selected for execution
          5.3.4 Global behavior
          5.3.5 Concept of time in the model
6 Definitional conventions
    6.1 Syntax definitions
    6.2 Semantic notations
7 Language elements
    7.1 Introduction
          7.1.1 Character set
          7.1.2 Estelle scope rules
    7.2 Structure of a specification
          7.2.1 Syntax
          7.2.2 Constraints
          7.2.3 Interpretation rules
          7.2.4 Informal semantics
    7.3 Declaration part
          7.3.1 Syntax
          7.3.2 Constraints
          7.3.3 Informal semantics
          7.3.4 Channel definition
          7.3.5 Interaction points
          7.3.6 Module header
          7.3.7 Module body definition
          7.3.8 Internal interaction points
          7.3.9 Module variable declaration part
          7.3.10 State definition part
          7.3.11 State set definition part
    7.4 References to Estelle objects
          7.4.1 Module variable reference
          7.4.2 Interaction point reference
          7.4.3 Exported variable reference
    7.5 Transition declarations
          7.5.1 General introduction
          7.5.2 Transition
          7.5.3 To clause
          7.5.4 From clause
          7.5.5 Provided clause
          7.5.6 When clause
          7.5.7 Delay clause
          7.5.8 Priority clause
          7.5.9 Any clause
          7.5.10 Initialization part
    7.6 Estelle statement
          7.6.1 Module instance creation
          7.6.2 Release and termination of module instances
          7.6.3 Connect operation
          7.6.4 Attach operation
          7.6.5 Disconnect operation
          7.6.6 Detach operation
          7.6.7 Summary of binding operations
          7.6.8 Output statement
          7.6.9 All statement
          7.6.10 Forone statement
          7.6.11 Exist expression
    7.7 Reserved words
          7.7.1 Syntax
          7.7.2 Constraints
8 Extensions and restrictions to ISO Pascal
    8.1 Simple changes to Pascal syntax
          8.1.1 Syntax
    8.2 Extensions
          8.2.1 Integers and real numbers
          8.2.2 Functions and procedures
          8.2.3 Implementation defined elements
          8.2.4 Directives
          8.2.5 Pure procedures and functions
          8.2.6 Expression
          8.2.7 Assignment operation
    8.3 Restrictions
          8.3.1 Errors
          8.3.2 File manipulation
          8.3.3 Label declarations and goto statements
          8.3.4 Program statement
          8.3.5 Expressions and functions
9 Semantics of Estelle constructs
    9.1 General scheme of definitions
    9.2 Primitives and organization of the clause
    9.3 External context environment and channel definition
          9.3.1 Interactions
          9.3.2 Channel definition interpretation
    9.4 Module instances
          9.4.1 Identifier categories of a module instance
          9.4.2 Internal extensions of context environment
                  and recursive assumptions
          9.4.3 Interaction points of a module instance and
                  related notions
          9.4.4 Locations, variable allocations and variable
                  visibility within a module instance
          9.4.5 States of a module instance
    9.5 Transitions of a module instance
          9.5.1 Transition statement
          9.5.2 Transition interpretation
          9.5.3 Linked interaction points
          9.5.4 Extension of the transition interpretation
                  over gids
    9.6 Interpretation of specific Estelle constructs
          9.6.1 External references
          9.6.2 Semantics of transition clauses
          9.6.3 Enabled transitions and initial states
          9.6.4 Delay values and time interpretation in Estelle
          9.6.5 Fireable transitions and offered transitions
          9.6.6 Semantics of primitive Estelle statements
Annexes
A Collected syntax
    A.1 Collected syntax from clause 7
    A.2 Collected syntax from clause 8
    A.3 Collected syntax from annex C
B User guidelines
    B.1 User data management
          B.1.1 Purpose of user data management
          B.1.2 Principles
          B.1.3 Encode procedure
          B.1.4 Decode procedure
          B.1.5 Guidelines
    B.2 Alternating bit example
C Pascal subset used by Estelle
D Estelle Tutorial
    D.0 Introduction
    D.1 A brief overview of the principal concepts in
          Estelle
          D.1.1 Modules and module instances
          D.1.2 Structuring of modules
          D.1.3 Communication
          D.1.4 Parallelism and Nondeterminism
          D.1.5 Dynamism within a system
          D.1.6 Typing
          D.1.7 Module internal behavior
          D.1.8 Global behavior
    D.2 Syntax and interpretation of Estelle concepts
          D.2.1 Channels, interactions and interaction points
          D.2.2 Modules
          D.2.3 Declaration part
          D.2.4 Initialization part
          D.2.5 Transition part
          D.2.6 Shorthands
    D.3 Estelle statements
          D.3.1 Init statement
          D.3.2 Connect statement
          D.3.3 Disconnect statement
          D.3.4 Connect statement
          D.3.5 Detach statement
          D.3.6 Release and terminate statements
          D.3.7 Output statement
          D.3.8 All and forone statements, exist expression
          D.3.9 Pascal restrictions in Estelle
    D.4 Behavior of Estelle specifications
          D.4.1 Specification module
          D.4.2 Internal behavior of a module
          D.4.3 Global behavior semantics
          D.4.4 Comparison of behaviors using common
                  example
    D.5 References
Indices

Specifies the semantics and syntax of the Formal Description Technique Estelle, mainly used for the formal description of distributed, concurrent information processing systems. Espcially for formal use in describing the service definitions and protocol specifications of the layers of Open Systems Interconnection as in ISO/IEC 7498-1. Does not specify procedures for the verifying of specifications written in Estelle.