ITU-T Z 500 FRENCH-1997 Framework on formal methods in conformance testing《一致性测试的正式方法框架 Z系列 方法 验证和测试的编程语言方法 10号研究组 49pp》.pdf

1、UNION INTERNATIONALE DES TLCOMMUNICATIONSUIT-TZ.500SECTEUR DE LA NORMALISATIONDES TLCOMMUNICATIONSDE LUIT(05/97)SRIE Z: LANGAGES DE PROGRAMMATIONMthodes de validation et dessaiCadre gnral des mthodes formellesappliques aux tests de conformitRecommandation UIT-T Z.500(Antrieurement Recommandation du

2、CCITT)RECOMMANDATIONS UIT-T DE LA SRIE ZLANGAGES DE PROGRAMMATIONPour plus de dtails, voir la Liste des Recommandations de lUIT-T.TECHNIQUES DE DESCRIPTION FORMELLE Z.100Z.199Langage de description et de spcification (SDL) Z.100Z.109Application des techniques de description formelle Z.110Z.119Diagra

3、mmes des squences de messages Z.120Z.129LANGAGES DE PROGRAMMATION Z.200Z.299CHILL: le langage de haut niveau de lUIT-T Z.200Z.209LANGAGE HOMME-MACHINE Z.300Z.499Principes gnraux Z.300Z.309Syntaxe de base et procdures de dialogue Z.310Z.319LHM tendu pour terminaux crans de visualisation Z.320Z.329Spc

4、ification de linterface homme-machine Z.330Z.399QUALIT DES LOGICIELS DE TLCOMMUNICATION Z.400Z.499MTHODES DE VALIDATION ET DESSAI Z.500Z.599Recommandation Z.500 (05/97) iRECOMMANDATION UIT-T Z.500CADRE GNRAL DES MTHODES FORMELLESAPPLIQUES AUX TESTS DE CONFORMITSourceLa Recommandation UIT-T Z.500, la

5、bore par la Commission dtudes 10 (1997-2000) de lUIT-T, a t approuve le6 mai 1997 selon la procdure dfinie dans la Rsolution n 1 de la CMNT.ii Recommandation Z.500 (05/97)AVANT-PROPOSLUIT (Union internationale des tlcommunications) est une institution spcialise des Nations Unies dans le domainedes t

6、lcommunications. LUIT-T (Secteur de la normalisation des tlcommunications) est un organe permanent delUIT. Il est charg de ltude des questions techniques, dexploitation et de tarification, et met ce sujet desRecommandations en vue de la normalisation des tlcommunications lchelle mondiale.La Confrenc

7、e mondiale de normalisation des tlcommunications (CMNT), qui se runit tous les quatre ans, dtermineles thmes dtudes traiter par les Commissions dtudes de lUIT-T lesquelles laborent en retour desRecommandations sur ces thmes.Lapprobation des Recommandations par les Membres de lUIT-T seffectue selon l

8、a procdure dfinie dans laRsolution n 1 de la CMNT.Dans certains secteurs de la technologie de linformation qui correspondent la sphre de comptence de lUIT-T, lesnormes ncessaires se prparent en collaboration avec lISO et la CEI.NOTEDans la prsente Recommandation, lexpression “Administration“ est uti

9、lise pour dsigner de faon abrge aussi bienune administration de tlcommunications quune exploitation reconnue.DROITS DE PROPRIT INTELLECTUELLELUIT attire lattention sur la possibilit que lapplication ou la mise en uvre de la prsente Recommandation puissedonner lieu lutilisation dun droit de proprit i

10、ntellectuelle. LUIT ne prend pas position en ce qui concerne lexistence,la validit ou lapplicabilit des droits de proprit intellectuelle, quils soient revendiqus par un Membre de lUIT ou parune tierce partie trangre la procdure dlaboration des Recommandations.A la date dapprobation de la prsente Rec

11、ommandation, lUIT navait pas t avise de lexistence dune propritintellectuelle protge par des brevets acqurir pour mettre en uvre la prsente Recommandation. Toutefois, comme ilne sagit peut-tre pas de renseignements les plus rcents, il est vivement recommand aux responsables de la mise enuvre de cons

12、ulter la base de donnes des brevets du TSB. UIT 1998Droits de reproduction rservs. Aucune partie de cette publication ne peut tre reproduite ni utilise sous quelque formeque ce soit et par aucun procd, lectronique ou mcanique, y compris la photocopie et les microfilms, sans laccordcrit de lUIT.Recom

13、mandation Z.500 (05/97) iiiTABLE DES MATIRESPage1 Domaine dapplication. 12 Rfrences normatives 12.1 Tests de conformit . 12.2 Techniques de description formelle. 23 Dfinitions. 23.1 Termes dautres normes apparentes 23.2 Termes dfinis dans la prsente Recommandation 34 Abrviations 45 Concepts mathmati

14、ques et conventions de notation 55.1 Ensembles 55.2 Logique 55.3 Relations 65.4 Fonctions . 66 La signification de la conformit. 66.1 Introduction . 66.2 Spcifications 66.3 Implmentations 76.4 Conformit dune implmentation une spcification formelle. 87 Concepts de test 107.1 Introduction . 107.2 Arch

15、itecture de test 107.3 Modle formel de larchitecture de test 117.4 Excution des tests. 128 Test de conformit 148.1 Introduction . 148.2 Dfinition des tests de conformit . 148.3 Gnration de tests. 148.4 Rduction de la taille de suite de tests . 158.5 Couverture de dfaut . 168.6 Cot de suite de tests

16、. 169 Conformit 179.1 Introduction . 179.2 Paragraphe 6: la signification de la conformit . 179.3 Paragraphe 7: concepts de test. 189.4 Paragraphe 8: test de conformit . 18Annexe A 18A.1 Spcifications 18A.2 Options dimplmentation et spcifications instancies. 23A.3 Implmentations et modles dimplmenta

17、tions.28A.4 Conformit par relations dimplmentation 30A.5 Conformit par exigences 33A.6 Architecture de test 34A.7 Spcifications des tests 35A.8 Rfrences . 42iv Recommandation Z.500 (05/97)IntroductionDe nombreuses spcifications de protocole et de service sont aujourdhui dcrites en termes de notation

18、s formellesappeles Techniques de Description Formelle (FDT, formal description techniques). Le SDL, LOTOS, Estelle et ASN.1sont des exemples de FDT normalises. Il existe galement une notation formelle pour des spcifications de suites detests: la notation combine arborescente et tabulaire (TTCN, tree

19、 and tabular combined notation). Lutilisation des FDTprsente les avantages suivants: elles dcrivent les formats et comportements de manire univoque, elles fournissent une base de validation rigoureuse incluant les essais de conformit.La conformit une norme de protocole ou de service de communication

20、 est considre comme une exigence pralablede linteroprabilit correcte des systmes ouverts. Le test de conformit, cest-dire lvaluation au moyen dessais de laconformit dun produit sa spcification, est un aspect important du dveloppement du produit car il augmente laconfiance en une interoprabilit corre

21、cte.La prsente Recommandation “Cadre gnral des mthodes formelles des tests de conformit“ (FMCT, framework onformal methods in conformance testing), dfinit la signification de la conformit lorsque des mthodes formelles sontutilises pour la spcification dun protocole ou dun service de communication. E

22、lle est galement destine servir deguide pour la gnration de tests informatiss.La prsente Recommandation dfinit un cadre pour lutilisation des mthodes formelles dans les essais de conformit.Elle est destine aux personnes charges des implmentations, des tests et des spcifications, impliques dans des t

23、ests deconformit afin de les aider dfinir la conformit ainsi que les procdures dessai dune implmentation donne, eugard une spcification fournie comme description formelle.Recommandation Z.500 (05/97) 1Recommandation Z.500Recommandation Z.500 (05/97)CADRE GNRAL DES MTHODES FORMELLESAPPLIQUES AUX TEST

24、S DE CONFORMIT(Genve, 1997)1 Domaine dapplicationLa prsente Recommandation sapplique lorsquil existe une spcification formelle de protocole ou de service decommunication partir de laquelle une suite de tests de conformit doit tre dveloppe. Elle peut servir de guide laprocdure manuelle ainsi quau dve

25、loppement doutils pour la gnration de tests lmentaires assiste par ordinateur.La prsente Recommandation dfinit un cadre gnral et ne prescrit aucune mthode particulire de gnration de testslmentaires ni ne prescrit de relation de conformit spcifique entre une spcification formelle et une implmentation

26、donne. Elle complte la norme mixte UIT-T/ISO “Cadre gnral et mthodologie des tests de conformit“(CTMF) ISO/CEI 9646, qui sapplique une large gamme de produits et de spcifications, y compris des spcificationscrites en langage naturel. Le cadre FMCT interprte les concepts de test de conformit dans un

27、contexte formel.2 Rfrences normativesLa prsente Recommandation se rfre certaines dispositions des Recommandations UIT-T et textes suivants qui de cefait en sont partie intgrante. Les versions indiques taient en vigueur au moment de la publication de la prsenteRecommandation. Toute Recommandation ou

28、tout texte tant sujet rvision, les utilisateurs de la prsenteRecommandation sont invits se reporter, si possible, aux versions les plus rcentes des rfrences normativessuivantes. La liste des Recommandations de lUIT-T en vigueur est rgulirement publie.2.1 Tests de conformitNOTE Dans le texte de la pr

29、sente Recommandation, il sera fait rfrence lensemble des normes ci-dessous par le terme CTMF. Recommandation UIT-T X.290 (1995) (quivalant lISO/CEI 9646-1:1994), Cadre gnral et mthodologiedes tests de conformit OSI pour les Recommandations sur les protocoles pour les applications de lUIT-T Spcificat

30、ions des suites de tests abstraites. Recommandation UIT-T X.291 (1995) (quivalant lISO/CEI 9646-2:1994), Cadre gnral et mthodologiedes tests de conformit dinterconnexion des systmes ouverts pour les Recommandations sur les protocolespour les applications de lUIT-T Spcification de suite de tests abst

31、raite. Recommandation X.292 du CCITT (1992) (quivalant lISO/CEI 9646-3:1992), Cadre gnral etmthodologie des tests de conformit OSI pour les Recommandations sur les protocoles pour les applicationsdu CCITT Notation combine arborescente et tabulaire. Recommandation UIT-T X.293 (1995) (quivalant lISO/C

32、EI 9646-4:1994), Cadre gnral et mthodologiedes tests de conformit dinterconnexion des systmes ouverts pour les Recommandations sur les protocolespour les applications de lUIT-T Ralisation des Tests. Recommandation UIT-T X.294 (1995) (quivalant lISO/CEI 9646-5:1994), Cadre gnral et mthodologiedes tes

33、ts de conformit OSI pour les Recommandations sur les protocoles pour les applications de lUIT-T Prescriptions des laboratoires de test et des clients en matire de processus dvaluation de conformit . Recommandation UIT-T X.295 (1995) (quivalant lISO/CEI 9646-6:1994), Cadre gnral et mthodologiedes tes

34、ts de conformit dinterconnexion des systmes ouverts pour les Recommandations sur les protocolespour les applications de lUIT-T Spcification des tests de profil de protocole. Recommandation UIT-T X.296 (1995) (quivalant lISO/CEI 9646-7:1995), Cadre gnral et mthodologiedes tests de conformit OSI pour

35、les Recommandations sur les protocoles pour les applications de lUIT-T Dclarations de conformit dinstance.2 Recommandation Z.500 (05/97)2.2 Techniques de description formelle Recommandation Z.100 du CCITT (1993), Langage de description et de spcification du CCITT. Recommandation UIT-T Z.120 (1996),

36、Diagramme de squence des messages. ISO/CEI 8807:1989, Systmes de traitement de linformation Interconnexion de systmes ouverts LOTOS Technique de description formelle base sur lorganisation temporelle de comportement observationnel . ISO/CEI 9074:1989, Systmes de traitement de linformation Interconne

37、xion de systmes ouverts Estelle Technique de description formelle base sur un modle de transition dtat tendu .3 Dfinitions3.1 Termes dautres normes apparentesNOTE Bien que les dfinitions suivantes soient donnes dans lUIT-T X.290 et lISO/CEI 9646-1, elles sont reprises ici car leursignification est i

38、mportante pour les interprtations formelles de la prsente Recommandation.3.1.1 mthode de test abstraite: dfinition de la faon dont une instance sous test doit tre teste, formule unniveau dabstraction appropri pour rendre cette description indpendante de toute ralisation particulire dun moyen detest,

39、 mais suffisamment dtaille pour permettre la spcification des tests au moyen de cette mthode.3.1.2 suite de tests de conformit: ensemble complet de tests lmentaires, pouvant tre combins en groupes detests imbriqus, qui est choisi pour lexcution de tests de conformit dynamique dun ou plusieurs protoc

40、oles.3.1.3 test de conformit: test visant dterminer jusqu quel point une instance sous test est conforme.3.1.4 implmentation conforme: instance sous test qui satisfait les conditions de conformit statique et dynamique,en accord avec les capacits dclares dans la ou les dclarations ICS.3.1.5 condition

41、 de conformit dynamique: toutes les conditions (et options) qui dterminent le comportementobservable autoris par la ou les spcifications applicables dans les instances de communication.3.1.6 verdict dchec: verdict de test rendu lorsque les rsultats de test observs attestent la non-conformit aumoins

42、une des conditions de conformit qui faisaient lobjet du test lmentaire, ou contiennent au moins un vnementde test non valide par rapport aux spcifications concernes.3.1.7 dclaration de conformit dune implmentation (ICS, implementation conformance statement):dclaration faite par le fournisseur dune i

43、mplmentation ou dun systme qui dclare se conformer une spcificationdonne, qui prcise les capacits mises en uvre. La dclaration ICS peut prendre diffrentes formes: ICS de protocole,ICS de profil, ICS de protocole spcifique et ICS dobjet informationnel.3.1.8 instance sous test (IUT, implementation und

44、er test): ensemble des procdures dun ou de plusieurs protocolesmises en uvre dans une relation utilisateur/fournisseur adjacente qui constitue la partie du systme ouvert rel qui doittre soumise des tests.3.1.9 informations supplmentaires sur limplmentation concernant le test (IXIT, implementation ex

45、trainformation for testing): dclaration faite par le fournisseur ou le ralisateur dune instance sous test, qui contient toutesles informations (en plus de celles fournies dans la dclaration ICS) concernant linstance sous test et son environnementde test, ou qui y renvoie, et qui doit permettre au la

46、boratoire de test dexcuter une suite de tests approprie sur cetteinstance. Une dclaration IXIT peut prendre diffrentes formes: IXIT de protocole, IXIT de profil, IXIT de profilspcifique et IXIT dobjet informationnel, dclaration dinstance de protocole TMP.3.1.10 moyens de test (MOT, means of testing)

47、: ensemble des quipements et procdures qui peuvent sacquitter dela drivation, de la slection, de la paramtrisation et de lexcution de tests lmentaires, conformment une suite ATSnormalise de rfrence; cet ensemble peut produire un journal de conformit.Recommandation Z.500 (05/97) 33.1.11 suite de tests abstraite paramtre: suite de tests abstraite slectionne dont tous les paramtres pertinents ontt fixs des valeurs conformes aux dclarations ICS et IXIT appropries.3.1.12 succs (verdict de