CAN CSA-Z243 101-1989 Information Processing Systems-Open Systems Interconnection-LOTOS-A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour (Fi.pdf

1、CAN/CSA-Z243.101-89A National Standard of Canada(reaffirmed 2013)Information Processing Systems-Open Systems Interconnection-LOTOS- A Formal Description Technique Based on the Temporal Ordering of Observational BehaviourLegal Notice for StandardsCanadian Standards Association (operating as “CSA Grou

2、p”) develops standards through a consensus standards development process approved by the Standards Council of Canada. This process brings together volunteers representing varied viewpoints and interests to achieve consensus and develop a standard. Although CSA Group administers the process and estab

3、lishes rules to promote fairness in achieving consensus, it does not independently test, evaluate, or verify the content of standards.Disclaimer and exclusion of liabilityThis document is provided without any representations, warranties, or conditions of any kind, express or implied, including, with

4、out limitation, implied warranties or conditions concerning this documents fitness for a particular purpose or use, its merchantability, or its non-infringement of any third partys intellectual property rights. CSA Group does not warrant the accuracy, completeness, or currency of any of the informat

5、ion published in this document. CSA Group makes no representations or warranties regarding this documents compliance with any applicable statute, rule, or regulation. IN NO EVENT SHALL CSA GROUP, ITS VOLUNTEERS, MEMBERS, SUBSIDIARIES, OR AFFILIATED COMPANIES, OR THEIR EMPLOYEES, DIRECTORS, OR OFFICE

6、RS, BE LIABLE FOR ANY DIRECT, INDIRECT, OR INCIDENTAL DAMAGES, INJURY, LOSS, COSTS, OR EXPENSES, HOWSOEVER CAUSED, INCLUDING BUT NOT LIMITED TO SPECIAL OR CONSEQUENTIAL DAMAGES, LOST REVENUE, BUSINESS INTERRUPTION, LOST OR DAMAGED DATA, OR ANY OTHER COMMERCIAL OR ECONOMIC LOSS, WHETHER BASED IN CONT

7、RACT, TORT (INCLUDING NEGLIGENCE), OR ANY OTHER THEORY OF LIABILITY, ARISING OUT OF OR RESULTING FROM ACCESS TO OR POSSESSION OR USE OF THIS DOCUMENT, EVEN IF CSA GROUP HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGES, INJURY, LOSS, COSTS, OR EXPENSES.In publishing and making this document availa

8、ble, CSA Group is not undertaking to render professional or other services for or on behalf of any person or entity or to perform any duty owed by any person or entity to another person or entity. The information in this document is directed to those who have the appropriate degree of experience to

9、use and apply its contents, and CSA Group accepts no responsibility whatsoever arising in any way from any and all use of or reliance on the information contained in this document. CSA Group is a private not-for-profit company that publishes voluntary standards and related documents. CSA Group has n

10、o power, nor does it undertake, to enforce compliance with the contents of the standards or other documents it publishes. Intellectual property rights and ownershipAs between CSA Group and the users of this document (whether it be in printed or electronic form), CSA Group is the owner, or the author

11、ized licensee, of all works contained herein that are protected by copyright, all trade-marks (except as otherwise noted to the contrary), and all inventions and trade secrets that may be contained in this document, whether or not such inventions and trade secrets are protected by patents and applic

12、ations for patents. Without limitation, the unauthorized use, modification, copying, or disclosure of this document may violate laws that protect CSA Groups and/or others intellectual property and may give rise to a right in CSA Group and/or others to seek legal redress for such use, modification, c

13、opying, or disclosure. To the extent permitted by licence or by law, CSA Group reserves all intellectual property rights in this document.Patent rightsAttention is drawn to the possibility that some of the elements of this standard may be the subject of patent rights. CSA Group shall not be held res

14、ponsible for identifying any or all such patent rights. Users of this standard are expressly advised that determination of the validity of any such patent rights is entirely their own responsibility.Authorized use of this documentThis document is being provided by CSA Group for informational and non

15、-commercial use only. The user of this document is authorized to do only the following:If this document is in electronic form:sLOADTHISDOCUMENTONTOACOMPUTERFORTHESOLEPURPOSEOFREVIEWINGITsSEARCHANDBROWSETHISDOCUMENTANDsPRINTTHISDOCUMENTIFITISIN0$ this remains the continuing responsibility of the SDO.

16、 An NSC reflects a consensus of a number of capable individuals whose collective interests provide, to the greatest practicable extent, a balance of representation of general interests, producers, regulators, users (including consumers), and others with relevant interests, as may be appropriate to t

17、he subject in hand. It normally is a standard which is capable of making a significant and timely contribution to the national interest.Those who have a need to apply standards areencouraged to use NSCs. These standards are subjectto periodic review. Users of NSCs are cautionedto obtain the latest e

18、dition from the SDO which publishes the standard.The responsibility for approving standards as National Standards of Canada rests with theStandards Council of Canada270 Albert Street, Suite 200Ottawa, Ontario, K1P 6N7CanadaCette Norme nationale du Canada est offerte en anglais et en franais.Although

19、 the intended primary application of this Standard is stated in its Scope, it is importantto note that it remains the responsibility of the users to judge its suitability for their particular purpose.TMA trade-mark of the Canadian Standards Association, operating as “CSA Group”National Standard of C

20、anada CAN/CSA-Z24 3.101-8 9 ( IS0 8807:1989) Information Processing Systems-Open Systems Interconnection-LOTOS-A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour Prepared by Canadian Standards Association Approved by Standards Council of Canada Q ISSN 031 7-5669

21、 Published in August 1989 by Canadian Standards Association, 178 Rexdale Boulevard, Rexdale (Toronto), Ontario, Canada M9W 1R3. Technical Editor: Paul V. Bates Managing Editor: Bernard Kelly Canadian Standards Association-1989 All rights reserved. No part of this publication may be reproduced in any

22、 form, in an electronic retrieval system or otherwise, without the prior permission of the publisher. Contents Contents Technical Committee on Open Systems v Preface vii 0. Introduction 7 0.1 General 7 0.2 FDTs 7 0.3 The Requirement for Standard FDTs 7 0.4 The Objectives To Be Satisfied by an FDT 7

23、0.5 The Origin of LOTOS 2 0.6 The Structure of this International Standard 2 1. 2. 3. 4. 4.1 4.2 4.3 4.4 4.5 4.6 4.7 4.8 5. 5.1 5.2 5.3 5.4 6. 6.1 Scope and Field of Application 3 References 3 Conformance 3 Basic Mathematical Concepts and Notation 5 General 5 Sets 5 Lists 6 Strings 6 Relations and F

24、unctions 6 Backus-Naur Form 7 Syntax-Directed Definitions 8 Derivation Systems 70 Introduction 73 Many-Sorted Algebras 73 Labelled Transition Systems 73 Structured Labelled Transition Systems 74 Model 73 Formal Syntax 75 Lexical Tokens 75 6.1.1 General 75 6.1.2 Basic Characters 75 6.1.3 Reserved Sym

25、bols 75 6.1.4 Identifiers 77 6.1.5 Requirement 78 6.1.6 Comments 78 6.1.7 Token Separators 78 6.1.8 Requirement 78 6.2 Specification Text 78 6.2.1 Specification 78 6.2.2 Definition-Block 78 6.2.3 Data-Type-Definitions 79 6.2.4 P-Expressions 79 6.2.5 Sorts, Operations and Equations 79 6.2.6 Process-D

26、efinitions 20 6.2.7 Behaviour-Expressions 20 6.2.8 Value-Expressions 23 6.2.9 Declarations 23 6.2.10 Special-Identifiers 23 7. Semantics 25 7.1 Introduction 25 7.1.1 Structure of the Static Semantics Definition 25 7.1.2 Structure of the Dynamic Semantics Definition 25 7.1.3 Structure of Clause 7 26

27、7.2 General Structures and Definitions 26 7.2.1 Names and Related Functions 26 7.2.2 Algebraic Specifications, Terms, and Equations 27 7.2.3 Canonical Specifications 28 7.3 Static Semantics 29 7.3.1 Introduction 29 7.3.2 General Structures and Definitions 30 7.3.3 Reconstruction of Terms 35 7.3.4 Fl

28、attening of a LOTOS Specification 39 7.3.5 Functional Structure of the Flattening Function 56 7.4 Semantics of Data-Presentations 60 7.4.1 General 60 7.4.2 The Derivation System of a Data-Presentation 60 7.4.3 Congruence Relation Induced by a Data-Presentation 67 7.4.4 Quotient Term Algebra 67 7.5 S

29、emantics of a Canonical LOTOS Specification 67 7.5.1 General 67 7.5.2 Auxiliary Definitions 67 7.5.3 Transition Derivation System 63 7.5.4 Structured Labelled Transition System of a Behaviour-Expression 69 7.5.5 Formal Interpretation of a Canonical LOTOS Specification 70 Information Processing Syste

30、ms-Open Systems Interconnection-LOTOS- A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour August 1989 iii Contents Annexes A-Standard Library of Data Types 77 B-Equivalence Relations 87 C-A Tutorial on LOTOS 95 D-Syntax Diagrams 727 E-Informal Basis for Abstract

31、 Data Types 735 CAN/CSA-Z243.101-89 August 1989 Technical Committee Technical Committee On Open Systems D.A. Sheppard C. Ashford J. Berube A. Bickle A. Bignell G.V. Bochmann D. Bonyun P. Bowie B.L. Catley B.S. Colwell J. Costa R.J. Craven G.P. Dallaire R. Dexter D.B. Forsyth G. Gori M.D. Harrop M. I

32、slam Protocols, Standards and Communications Inc., Ottawa, Ontario Chairman Bell-Northern Research, Ottawa, Ontario Atkinson, Tremblay (b) provide an explanation of circumstances surrounding the actual field condition; and (c) be phrased where possible to permit a specific yes or “no“ answer. sample

33、 copy, write to CSA Marketing or telephone (416) 747-4019. This CSA Standard is adopted from the IS0 International Standard 8807. As a member This Standard was reviewed and adopted by the CSA Technical Committee on Open Requests for interpretation should Interpretations are published in CSA Informat

34、ion Update. For subscription details and a free Information Processing Systems-Open Systems Interconnection-LOTOS- A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour August 1989 vii INERNATIONAL STANDARD IS0 8807 : 1989 (El Information processing systems - Open

35、Systems Interconnection - LOTOS - A formal description technique based on the temporal ordering of o bservatio na I be havio u r 0 Introduction 0.1 General Formal description techniques (FDTs) are methods of defining the behaviour of an (information processing) system in a language with a formal syn

36、tax and semantics, instead of a natural language such as English. In the following sub-clauses of this introduction, the importance of FDTs and their standardization is discussed. The objectives that an FDT must satisfy are considered. The origin of LOTOS is discussed. Finally the structure of this

37、document is explained. 0.2 FDTs Formal description techniques are important tools for the design, analysis and specification of information processing systems. It is by means of formal techniques that system descriptions can be produced that are complete, consistent, concise, unambiguous and precise

38、. This is only possible if an FDT is self-contained, so that the descriptions given in an FDT need not refer to any informal knowledge of the system that is described. An important aspect of a formal system is that it allows analysis by mathematical methods. An FDT that has such a formal, mathematic

39、al basis can be used to prove the correctness of specifications. 0.3 The requirement for standard FDTs If an FDT is defined in an International Standard, the description is available to all who require it. The Directives for the production of such a standard require a high degree of international ac

40、ceptance and technical stability. Any amendment also requires international agreement. Hence a standard FDT offers the most useful form of presentation to those who wish to apply it. 0.4 The objectives to be satisfied by an FDT Although this document describes an FDT that is generally applicable to

41、distributed, concurrent information processing systems, it has been developed particularly for OSI. The main objectives to be satisfied by such an FDT are that it should be 1 IS0 8807 : 1989 (El a) expressive: an FDT should be able to define both the protocol specifications and the service definitio

42、ns of the seven layers of OSI described in IS0 7498. b) well-defined: an FDT should have a formal mathematical model that is suitable for the analysis of these specifications and definitions. The same model should support the checking of conformance of implementations that are permitted by the OSI I

43、nternational Standards. This model should also support the testing of an implementation for conformance. well-structured an FDT should offer means for structuring the description of a specification or definition in manner that is meaningful and intuitively pleasing. A good structure increases the re

44、adability, understandability, flexibility, and maintainability of system descriptions, and offers a better framework for their analysis. d) abstract there are two aspects of abstraction that an FDT should offer: c) 1) an FDT should be completely independent of methods of implementation, so that the

45、technique itself does not provide any undue constraints on implementors 2) an FDT should offer the means of abstraction from irrelevant details with respect to the context at any point in a description. Abstraction can reduce the local complexity of system descriptions considerably. In the presence

46、of a good structure, abstraction can help even further to reduce the complexity of descriptions. 0.5 The origin of LOTOS LOTOS (Language of Temporal Ordering Specification) was developed by FDT experts from ISO/TC97 during the years 1981-1988. The basic idea that LOTOS developed from was that system

47、s can be described by defining the temporal relation between events in the externally observable behaviour of a system. LOTOS has two components. The first component deals with the description of process behaviours and interactions, and is based on a modification of the Calculus of Communicating Sys

48、tems (CCS), which was developed at the University of Edinburgh. The modification includes elements that were introduced in other calculi, which are related to CCS, viz. CSP and CIRCAL. Among the other theories that are related to CCS, and thus to LOTOS, are SCCS, tvlElJE and ACP. CCS, and the relate

49、d formal systems, provide a powerful analytical theory for concurrent processes. The second component deals with the description of data structures and value expressions and is based on the abstract data type language ACT ONE. ACT ONE was developed at the Technical University of Berlin. The part of LOTOS dealing with the description of processes, i.e. dynamic behaviours, is not dependent upon ACT ONE. Many