CAN CSA-ISO IEC TR 15942-2004 Information technology - Programming languages - Guide for the use of the Ada programming language in high integrity systems.pdf

1、National Standard of CanadaCAN/CSA-ISO/IEC TR 15942:04(ISO/IEC TR 15942:2000)Technical Report ISO/IEC TR 15942:2000 (first edition, 2000-03-01) has been adopted withoutmodification (IDT) as CSA Standard CAN/CSA-ISO/IEC TR 15942:04, which has been approved as a NationalStandard of Canada by the Stand

2、ards Council of Canada.ISBN 1-55397-738-6 December 2004Reference numberISO/IEC TR 15942:2000(E)ISO/IEC2000Information technology Programminglanguages Guide for the use of the Adaprogramming language in high integritysystemsTechnologies de linformation Langages de programmation Guidepour lemploi du l

3、angage de programmation Ada dans les systmes dehaute intgritThe Canadian Standards Association (CSA), under whose auspices this National Standard has been produced, was chartered in 1919 and accredited by the Standards Council of Canada to the National Standards system in 1973. It is a not-for-profi

4、t, nonstatutory, voluntary membership association engaged in standards development and certification activities. CSA standards reflect a national consensus of producers and users including manufacturers, consumers, retailers, unions and professional organizations, and governmental agencies. The stan

5、dards are used widely by industry and commerce and often adopted by municipal, provincial, and federal governments in their regulations, particularly in the fields of health, safety, building and construction, and the environment. Individuals, companies, and associations across Canada indicate their

6、 support for CSAs standards development by volunteering their time and skills to CSA Committee work and supporting the Associations objectives through sustaining memberships. The more than 7000 committee volunteers and the 2000 sustaining memberships together form CSAs total membership from which it

7、s Directors are chosen. Sustaining memberships represent a major source of income for CSAs standards development activities. The Association offers certification and testing services in support of and as an extension to its standards development activities. To ensure the integrity of its certificati

8、on process, the Association regularly and continually audits and inspects products that bear the CSA Mark. In addition to its head office and laboratory complex in Toronto, CSA has regional branch offices in major centres across Canada and inspection and testing agencies in eight countries. Since 19

9、19, the Association has developed the necessary expertise to meet its corporate mission: CSA is an independent service organization whose mission is to provide an open and effective forum for activities facilitating the exchange of goods and services through the use of standards, certification and r

10、elated services to meet national and international needs.For further information on CSA services, write toCanadian Standards Association5060 Spectrum Way, Suite 100Mississauga, Ontario, L4W 5N6CanadaThe Standards Council of Canada is the coordinating body of the National Standards system, a federati

11、on of independent, autonomous organizations working towards the further development and improvement of voluntary standardization in the national interest. The principal objects of the Council are to foster and promote voluntary standardization as a means of advancing the national economy, benefiting

12、 the health, safety, and welfare of the public, assisting and protecting the consumer, facilitating domestic and international trade, and furthering international cooperation in the field of standards. A National Standard of Canada is a standard which has been approved by the Standards Council of Ca

13、nada and one which reflects a reasonable agreement among the views of a number of capable individuals whose collective interests provide to the greatest practicable extent a balance of representation of producers, users, consumers, and others with relevant interests, as may be appropriate to the sub

14、ject in hand. It normally is a standard which is capable of making a significant and timely contribution to the national interest. Approval of a standard as a National Standard of Canada indicates that a standard conforms to the criteria and procedures established by the Standards Council of Canada.

15、 Approval does not refer to the technical content of the standard; this remains the continuing responsibility of the accredited standards development organization. Those who have a need to apply standards are encouraged to use National Standards of Canada whenever practicable. These standards are su

16、bject to periodic review; therefore, users are cautioned to obtain the latest edition from the organization preparing the standard.The responsibility for approving National Standards of Canada rests with theStandards Council of Canada270 Albert Street, Suite 200Ottawa, Ontario, K1P 6N7CanadaAlthough

17、 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.Registered trade-mark of Canadian Standards AssociationCAN/CSA-ISO/IEC TR 15942:04Information techno

18、logy Programming languages Guide for theuse of the Ada programming language in high integrity systemsDecember 2004 Canadian Standards Association CSA/1CAN/CSA-ISO/IEC TR 15942:04Information technology Programming languages Guide for the use of the Ada programming language in high integrity systemsCS

19、A PrefaceStandards development within the Information Technology sector is harmonized with international standards development. Through the CSA Technical Committee on Information Technology (TCIT), Canadians serve as the Canadian Advisory Committee (CAC) on ISO/IEC Joint Technical Committee 1 on Inf

20、ormation Technology (ISO/IEC JTC1) for the Standards Council of Canada (SCC), the ISO member body for Canada and sponsor of the Canadian National Committee of the IEC. Also, as a member of the International Telecommunication Union (ITU), Canada participates in the International Telegraph and Telepho

21、ne Consultative Committee (ITU-T).This Technical Report was reviewed by the CSA TCIT under the jurisdiction of the Strategic Steering Committee on Information Technology and deemed acceptable for use in Canada. (A committee membership list is available on request from the CSA Project Manager.) From

22、time to time, ISO/IEC may publish addenda, corrigenda, etc. The CSA TCIT will review these documents for approval and publication. For a listing, refer to the CSA Information Products catalogue or CSA Info Update or contact a CSA Sales representative. This Standard has been formally approved as a Na

23、tional Standard of Canada by the Standards Council of Canada.December 2004 Canadian Standards Association 2004All rights reserved. No part of this publication may be reproduced in any form whatsoever without the prior permission ofthe publisher. ISO/IEC material is reprinted with permission. Where t

24、he words “this Technical Report” appear in the text, they should be interpreted as “this National Standard of Canada”.Inquiries regarding this National Standard of Canada should be addressed toCanadian Standards Association5060 Spectrum Way, Suite 100, Mississauga, Ontario, Canada L4W 5N61-800-463-6

25、727 416-747-4044www.csa.caReference numberISO/IEC TR 15942:2000(E)ISO/IEC 2000TECHNICALREPORTISO/IECTR15942First edition2000-03-01Information technology Programminglanguages Guide for the use of the Adaprogramming language in high integritysystemsTechnologies de linformation Langages de programmatio

26、n Guidepour lemploi du langage de programmation Ada dans les systmes dehaute intgritISO/IEC TR 15942:2000(E)PDF disclaimerThis PDF file may contain embedded typefaces. In accordance with Adobes licensing policy, this file may be printed or viewed but shall notbe edited unless the typefaces which are

27、 embedded are licensed to and installed on the computer performing the editing. In downloading thisfile, parties accept therein the responsibility of not infringing Adobes licensing policy. The ISO Central Secretariat accepts no liability in thisarea.Adobe is a trademark of Adobe Systems Incorporate

28、d.Details of the software products used to create this PDF file can be found in the General Info relative to the file; the PDF-creation parameterswere optimized for printing. Every care has been taken to ensure that the file is suitable for use by ISO member bodies. In the unlikely eventthat a probl

29、em relating to it is found, please inform the Central Secretariat at the address given below. ISO/IEC 2000All rights reserved. Unless otherwise specified, no part of this publication may be reproduced or utilized in any form or by any means, electronicor mechanical, including photocopying and microf

30、ilm, without permission in writing from either ISO at the address below or ISOs member bodyin the country of the requester.ISO copyright officeCase postale 56 Gb7 CH-1211 Geneva 20Tel. + 41 22 749 01 11Fax + 41 22 734 10 79E-mail copyrightiso.chWeb www.iso.chii ISO/IEC 2000 All rights reservedISO/IE

31、C TR 15942:2000 (E) ISO/IEC 2000 - All rights reserved iiiContents1 Scope.11.1 Within the scope11.2 Out of scope 22 Verification Techniques.22.1 Traceability 22.2 Reviews32.3 Analysis32.3.1 Control Flow analysis.42.3.2 Data Flow analysis42.3.3 Information Flow analysis42.3.4 Symbolic Execution42.3.5

32、 Formal Code Verification52.3.6 Range Checking62.3.7 Stack Usage analysis62.3.8 Timing Analysis.62.3.9 Other Memory Usage analysis.62.3.10 Object Code Analysis .72.4 Testing72.4.1 Principles.72.4.2 Requirements-based Testing.72.4.3 Structure-based Testing.82.5 Use of Verification Techniques in this

33、Technical Report83 General Language Issues93.1 Writing Verifiable Programs.93.1.1 Language Rules to Achieve Predictability103.1.2 Language Rules to Allow Modelling103.1.3 Language Rules to Facilitate Testing113.1.4 Pragmatic Considerations123.1.5 Language Enhancements.123.2 The Choice of Language.13

34、4 Significance of Language Features for High Integrity144.1 Criteria for Assessment of Language Features.144.2 How to use this Technical Report .145 Assessment of Language Features155.1 Types with Static Attributes.165.1.1 Evaluation175.1.2 Notes 175.1.3 Guidance175.2 Declarations.175.2.1 Evaluation

35、185.2.2 Notes 185.2.3 Guidance185.3 Names, including Scope and Visibility195.3.1 Evaluation195.3.2 Notes 195.3.3 Guidance205.4 Expressions.205.4.1 Evaluation215.4.2 Notes 215.4.3 Guidance22ISO/IEC TR 15942:2000 (E) ISO/IEC 2000 - All rights reservediv5.5 Statements.225.5.1 Evaluation235.5.2 Notes 23

36、5.5.3 Guidance235.6 Subprograms.245.6.1 Evaluation245.6.2 Notes 245.6.3 Guidance255.7 Packages (child and library) 255.7.1 Evaluation265.7.2 Notes 265.7.3 Guidance265.8 Arithmetic Types.275.8.1 Evaluation275.8.2 Notes 275.8.3 Guidance285.9 Low Level and Interfacing295.9.1 Evaluation305.9.2 Notes 305

37、.9.3 Guidance315.10 Generics.315.10.1 Evaluation325.10.2 Notes 325.10.3 Guidance335.11 Access Types and Types with Dynamic Attributes.345.11.1 Evaluation345.11.2 Notes 345.11.3 Guidance355.12 Exceptions.355.12.1 Evaluation365.12.2 Notes 365.12.3 Guidance365.13 Tasking.375.13.1 Evaluation395.13.2 Not

38、es 395.13.3 Guidance395.14 Distribution405.14.1 Evaluation405.14.2 Notes 405.14.3 Guidance406 Compilers and Run-time Systems406.1 Language issues.416.2 Compiler Qualification416.3 Run-Time System427 References437.1 Applicable Documents .437.2 Referenced Documents44ISO/IEC TR 15942:2000 (E)ForewordIS

39、O (the International Organization for Standardization) and IEC (the International Electrotechnical Commission) form thespecialized system for worldwide standardization. National bodies that are members of ISO or IEC participate in thedevelopment of International Standards through technical committee

40、s established by the respective organization to deal withparticular fields of technical activity. ISO and IEC technical committees collaborate in fields of mutual interest. Otherinternational organizations, governmental and non-governmental, in liaison with ISO and IEC, also take part in the work.In

41、ternational Standards are drafted in accordance with the rules given in the ISO/IEC Directives, Part 3.In the field of information technology, ISO and IEC have established a joint technical committee, ISO/IEC JTC 1. DraftInternational Standards adopted by the technical committees are circulated to t

42、he member bodies for voting. Publication as anInternational Standard requires approval by at least 75 % of the member bodies casting a vote.In exceptional circumstances, when a technical committee has collected data of a different kind from that which is normallypublished as an International Standar

43、d (“state of the art“, for example), it may decide by a simple majority vote of itsparticipating members to publish a Technical Report. A Technical Report is entirely informative in nature and does not have tobe reviewed until the data it provides are considered to be no longer valid or useful.Atten

44、tion is drawn to the possibility that some of the elements of this Technical Report may be the subject of patent rights. ISOand 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 techno

45、logy, SubcommitteeSC 22, Programming languages, their environments and system software interfaces. ISO/IEC 2000 - All rights reserved v ISO/IEC TR 15942:2000 (E)IntroductionAs a society, we are increasingly reliant upon high integrity systems: for safety systems (such as fly-by-wire aircraft), forse

46、curity systems (to protect digital information) or for financial systems (e.g., cash dispensers). As the complexity of thesesystems grows, so do the demands for improved techniques for the production of the software components of the system.These high integrity systems must be shown to be fully pred

47、ictable 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 conventional dynamic testing.There is, currently, no mainstream high level language where all programs in that language are guaranteed to be predictable an

48、danalysable. Therefore for any choice of implementation language it is essential to control the ways that the language is used bythe application.The Ada language ARM is designed with specific mechanisms for controlling the use of certain aspects of the language.Furthermore,1. The semantics of Ada pr

49、ograms are well-defined, even in error situations. Specifically, the effect of a programcan be predicted from the language definition with few implementation dependencies or interactions betweenlanguage features.2. The strong typing within the language can be used to reduce the scope (and cost) of analysis to verify keyproperties.3. The Ada language has been successfully used on many high integrity applications. This demonstrates thatvalidated Ada compil