《ISO-TR-15942-2000.pdf》由会员分享，可在线阅读，更多相关《ISO-TR-15942-2000.pdf（58页珍藏版）》请在三一文库上搜索。
1、Reference number ISO/IEC TR 15942:2000(E) ISO/IEC 2000 TECHNICAL REPORT ISO/IEC TR 15942 First edition 2000-03-01 Information technology Programming languages Guide for the use of the Ada programming language in high integrity systems Technologies de linformation Langages de programmation Guide pour
2、 lemploi du langage de programmation Ada dans les systmes de haute intgrit Copyright International Organization for Standardization Provided by IHS under license with ISO Licensee=NASA Technical Standards 1/9972545001 Not for Resale, 04/06/2007 23:32:09 MDTNo reproduction or networking permitted wit
3、hout license from IHS -,-,- ISO/IEC TR 15942:2000(E) PDF disclaimer This PDF file may contain embedded typefaces. In accordance with Adobes licensing policy, this file may be printed or viewed but shall not be edited unless the typefaces which are embedded are licensed to and installed on the comput
4、er performing the editing. In downloading this file, parties accept therein the responsibility of not infringing Adobes licensing policy. The ISO Central Secretariat accepts no liability in this area. Adobe is a trademark of Adobe Systems Incorporated. Details of the software products used to create
5、 this PDF file can be found in the General Info relative to the file; the PDF-creation parameters were optimized for printing. Every care has been taken to ensure that the file is suitable for use by ISO member bodies. In the unlikely event that a problem relating to it is found, please inform the C
6、entral Secretariat at the address given below. ISO/IEC 2000 All rights reserved. Unless otherwise specified, no part of this publication may be reproduced or utilized in any form or by any means, electronic or mechanical, including photocopying and microfilm, without permission in writing from eithe
7、r ISO at the address below or ISOs member body in the country of the requester. ISO copyright office Case postale 56 ? CH-1211 Geneva 20 Tel. + 41 22 749 01 11 Fax + 41 22 734 10 79 E-mail copyrightiso.ch Web www.iso.ch Printed in Switzerland ii ISO/IEC 2000 All rights reserved Copyright Internation
8、al Organization for Standardization Provided by IHS under license with ISO Licensee=NASA Technical Standards 1/9972545001 Not for Resale, 04/06/2007 23:32:09 MDTNo reproduction or networking permitted without license from IHS -,-,- ISO/IEC TR 15942:2000 (E) ISO/IEC 2000 - All rights reservediii Cont
9、ents 1Scope.1 1.1Within the scope1 1.2Out of scope 2 2Verification Techniques.2 2.1Traceability 2 2.2Reviews3 2.3Analysis3 2.3.1Control Flow analysis.4 2.3.2Data Flow analysis4 2.3.3Information Flow analysis4 2.3.4Symbolic Execution4 2.3.5Formal Code Verification5 2.3.6Range Checking6 2.3.7Stack Usa
10、ge analysis6 2.3.8Timing Analysis.6 2.3.9Other Memory Usage analysis.6 2.3.10 Object Code Analysis .7 2.4Testing7 2.4.1Principles .7 2.4.2Requirements-based Testing.7 2.4.3Structure-based Testing.8 2.5Use of Verification Techniques in this Technical Report8 3General Language Issues9 3.1Writing Verif
11、iable Programs.9 3.1.1Language Rules to Achieve Predictability10 3.1.2Language Rules to Allow Modelling10 3.1.3Language Rules to Facilitate Testing11 3.1.4Pragmatic Considerations12 3.1.5Language Enhancements.12 3.2The Choice of Language.13 4Significance of Language Features for High Integrity14 4.1
12、Criteria for Assessment of Language Features .14 4.2How to use this Technical Report .14 5Assessment of Language Features15 5.1Types with Static Attributes.16 5.1.1Evaluation 17 5.1.2Notes 17 5.1.3Guidance17 5.2Declarations.17 5.2.1Evaluation 18 5.2.2Notes 18 5.2.3Guidance18 5.3Names, including Scop
13、e and Visibility19 5.3.1Evaluation 19 5.3.2Notes 19 5.3.3Guidance20 5.4Expressions.20 5.4.1Evaluation 21 5.4.2Notes 21 5.4.3Guidance22 Copyright International Organization for Standardization Provided by IHS under license with ISO Licensee=NASA Technical Standards 1/9972545001 Not for Resale, 04/06/
14、2007 23:32:09 MDTNo reproduction or networking permitted without license from IHS -,-,- ISO/IEC TR 15942:2000 (E) ISO/IEC 2000 - All rights reservediv 5.5Statements.22 5.5.1Evaluation23 5.5.2Notes 23 5.5.3Guidance23 5.6Subprograms.24 5.6.1Evaluation24 5.6.2Notes 24 5.6.3Guidance25 5.7Packages (child
15、 and library) 25 5.7.1Evaluation26 5.7.2Notes 26 5.7.3Guidance26 5.8Arithmetic Types.27 5.8.1Evaluation27 5.8.2Notes 27 5.8.3Guidance28 5.9Low Level and Interfacing29 5.9.1Evaluation30 5.9.2Notes 30 5.9.3Guidance31 5.10Generics.31 5.10.1 Evaluation32 5.10.2 Notes 32 5.10.3 Guidance33 5.11Access Type
16、s and Types with Dynamic Attributes.34 5.11.1 Evaluation34 5.11.2 Notes 34 5.11.3 Guidance35 5.12Exceptions.35 5.12.1 Evaluation36 5.12.2 Notes 36 5.12.3 Guidance36 5.13Tasking.37 5.13.1 Evaluation39 5.13.2 Notes 39 5.13.3 Guidance39 5.14Distribution40 5.14.1 Evaluation40 5.14.2 Notes 40 5.14.3 Guid
17、ance40 6Compilers and Run-time Systems40 6.1Language issues.41 6.2Compiler Qualification41 6.3Run-Time System42 7References 43 7.1Applicable Documents .43 7.2Referenced Documents44 Copyright International Organization for Standardization Provided by IHS under license with ISO Licensee=NASA Technical
18、 Standards 1/9972545001 Not for Resale, 04/06/2007 23:32:09 MDTNo reproduction or networking permitted without license from IHS -,-,- ISO/IEC TR 15942:2000 (E) Foreword ISO (the International Organization for Standardization) and IEC (the International Electrotechnical Commission) form the specializ
19、ed system for worldwide standardization. National bodies that are members of ISO or IEC participate in the development of International Standards through technical committees established by the respective organization to deal with particular fields of technical activity. ISO and IEC technical commit
20、tees collaborate in fields of mutual interest. Other international organizations, governmental and non-governmental, in liaison with ISO and IEC, also take part in the work. International Standards are drafted in accordance with the rules given in the ISO/IEC Directives, Part 3. In the field of info
21、rmation technology, ISO and IEC have established a joint technical committee, ISO/IEC JTC 1. Draft International Standards adopted by the technical committees are circulated to the member bodies for voting. Publication as an International Standard requires approval by at least 75 % of the member bod
22、ies casting a vote. In exceptional circumstances, when a technical committee has collected data of a different kind from that which is normally published as an International Standard (“state of the art“, for example), it may decide by a simple majority vote of its participating members to publish a
23、Technical Report. A Technical Report is entirely informative in nature and does not have to be reviewed until the data it provides are considered to be no longer valid or useful. Attention is drawn to the possibility that some of the elements of this Technical Report may be the subject of patent rig
24、hts. ISO and IEC shall not be held responsible for identifying any or all such patent rights. ISO/IEC TR 15942 was prepared by Joint Technical Committee ISO/IEC JTC 1, Information technology, Subcommittee SC 22, Programming languages, their environments and system software interfaces. ISO/IEC 2000 -
25、 All rights reservedv Copyright International Organization for Standardization Provided by IHS under license with ISO Licensee=NASA Technical Standards 1/9972545001 Not for Resale, 04/06/2007 23:32:09 MDTNo reproduction or networking permitted without license from IHS -,-,- ISO/IEC TR 15942:2000 (E)
26、 Introduction As a society, we are increasingly reliant upon high integrity systems: for safety systems (such as fly-by-wire aircraft), for security systems (to protect digital information) or for financial systems (e.g., cash dispensers). As the complexity of these systems grows, so do the demands
27、for improved techniques for the production of the software components of the system. These high integrity systems must be shown to be fully predictable in operation and have all the properties required of them. This can only be achieved by analysing the software, in addition to the use of convention
28、al dynamic testing. There is, currently, no mainstream high level language where all programs in that language are guaranteed to be predictable and analysable. Therefore for any choice of implementation language it is essential to control the ways that the language is used by the application. The Ad
29、a language ARM is designed with specific mechanisms for controlling the use of certain aspects of the language. Furthermore, 1. The semantics of Ada programs are well-defined, even in error situations. Specifically, the effect of a program can be predicted from the language definition with few imple
30、mentation dependencies or interactions between language features. 2. The strong typing within the language can be used to reduce the scope (and cost) of analysis to verify key properties. 3. The Ada language has been successfully used on many high integrity applications. This demonstrates that valid
31、ated Ada compilers have the quality required for such applications. 4. Guidance can be provided to facilitate the use of the language and to encourage the development of tools for further verification. Ada is therefore ideally suited for implementing high integrity software and this document provide
32、s guidance in the controls that are required on the use of Ada to ensure that programs are predictable and analysable. All language design balances functionality against integrity. For instance, the ability to control storage allocation directly will impact the need to ensure the integrity of data.
33、An aspect of the integrity of Ada programs is the possibility of avoiding access types (references) completely, whereas in other languages references are linked to array accessing and/or parameter passing, and therefore cannot be excluded. There are a number of different analysis techniques in use f
34、or high integrity software and this document is not prescriptive about which techniques to use. Furthermore, each analysis technique requires different controls on the use of the language. Ada assists analysis: for instance, the modes of Ada parameters, suitably used, provide information for data fl
35、ow analysis which other languages cannot always provide. This Technical Report, therefore, catalogues specific verification techniques (see 2.5), and classifies the impact that language features have on the use of these techniques (in the tables in Section 5). It is the users responsibility to selec
36、t the analysis techniques for a particular application; this document can then be used to define the full set of controls necessary for using that set of techniques. The guidance given here first specifies its scope, by reference to the safety and security standards to which high integrity applicati
37、ons may be written. Section 2 then analyses the verification techniques that are applied in the development of high integrity systems.By this means, the regulatory rules of the standards for safety and security are abstracted to avoid the need to consider each such standard separately. Section 3 add
38、resses general issues concerning how computer languages must be constructed if programs written in that language are to be fully predictable. These issues are relevant to any restricted language defined through the application of this guidance. ISO/IEC 2000 - All rights reservedvi Copyright Internat
39、ional Organization for Standardization Provided by IHS under license with ISO Licensee=NASA Technical Standards 1/9972545001 Not for Resale, 04/06/2007 23:32:09 MDTNo reproduction or networking permitted without license from IHS -,-,- ISO/IEC TR 15942:2000 (E) Section 4 provides identification of a
40、three-way classification system used for Ada language features. This classification is based upon the ease with which verification techniques can be applied to a program containing the feature. This classification is needed since while the majority of the core features in Ada assists verification, t
41、he use of certain features makes the resulting code difficult or impossible to analyse with the currently available program analysis tools and techniques. Section 5 provides the main technical material of this Technical Report by classifying Ada language features. Users of this Technical Report can
42、then determine which features of Ada are appropriate to use from the verification techniques that are to be employed. The assessment has shown that the vast majority of the Ada features lend themselves to effective use in the construction of high integrity systems. The Technical Report concludes, in
43、 Section 6, by providing information to aid the choice of a suitable Ada compiler together with its associated run-time system. References to relevant standards and guides are provided. A detailed analysis of Ada95 for high integrity systems is available in References CAT1, CAT2 and CAT3 . A compreh
44、ensive index is provided to ease the use of the Technical Report. Levels of criticality Many of the Standards to which high integrity software is written use multiple levels to classify the criticality of the software components which make up the system. While the number and nature of the levels var
45、y, the general approach is always the same: the higher the criticality of the system, the more verification techniques need to be used for its assurance. Table 1 relates the various levels of classification used in some well known International Standards. Table 1: Levels of criticality in some Stand
46、ards StandardNumber of levelsLowest LevelHighest Level DO-178B4DA IEC-615084Safety Integrity Level 1Safety Integrity Level 4 ITSEC7E0E6 This Technical Report emphasizes the higher levels of criticality, for which the more demanding verification techniques are employed and for which Ada provides majo
47、r benefits. This Technical Report, however, does not directly use any such levels but focuses on the correlation between the features of the language and the verification techniques to be employed at the higher levels of criticality. The material in ISO/IEC 15026, DS 00-56, ARP 4754 and ARP 4761 may
48、 be useful in determining the criticality of a system if this is not covered by application-specific standards. Readership This Technical Report has been written for: 1. Those responsible for coding standards applicable to high integrity Ada software. 2. Those developing high integrity systems in Ada. 3. Vendors marketing Ada compilers, source code generators, and verification tools for use in the development of high integrity systems. 4. Regulators who need to approve high integrity systems containing software written in Ada. 5. Those concerned with high integrity systems who w