BS ISO 9074:1989

0 Introduction
0.1 General
0.2 Formal Description Techniques
0.3 Requirement for standard FDTs
0.4 Objectives to be satisfied by an FDT
1 Scope and field of application
2 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 nondeterminism
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 heater
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 statements
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
Indices

Defines the semantics and syntax of the formal description technique Estelle.