Vérification formelle des aspects de cohérence d’un Workflow net

02/08/2016
Publication e-STA e-STA 2010-1
OAI : oai:www.see.asso.fr:545:2010-1:17200
DOI :

Résumé

Vérification formelle des aspects de cohérence d’un Workflow net

Métriques

26
4
214.7 Ko
 application/pdf
bitcache://03a15828ffd673d2353eb5496cf6b6fc7f9073d2

Licence

Creative Commons Aucune (Tous droits réservés)
<resource  xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
                xmlns="http://datacite.org/schema/kernel-4"
                xsi:schemaLocation="http://datacite.org/schema/kernel-4 http://schema.datacite.org/meta/kernel-4/metadata.xsd">
        <identifier identifierType="DOI">10.23723/545:2010-1/17200</identifier><creators><creator><creatorName>Abdallah Missaoui</creatorName></creator><creator><creatorName>Zohra Sbaï</creatorName></creator><creator><creatorName>Kamel Barkaoui</creatorName></creator></creators><titles>
            <title>Vérification formelle des aspects de cohérence d’un Workflow net</title></titles>
        <publisher>SEE</publisher>
        <publicationYear>2016</publicationYear>
        <resourceType resourceTypeGeneral="Text">Text</resourceType><dates>
	    <date dateType="Created">Tue 2 Aug 2016</date>
	    <date dateType="Updated">Tue 2 Aug 2016</date>
            <date dateType="Submitted">Fri 20 Jul 2018</date>
	</dates>
        <alternateIdentifiers>
	    <alternateIdentifier alternateIdentifierType="bitstream">03a15828ffd673d2353eb5496cf6b6fc7f9073d2</alternateIdentifier>
	</alternateIdentifiers>
        <formats>
	    <format>application/pdf</format>
	</formats>
	<version>28942</version>
        <descriptions>
            <description descriptionType="Abstract"></description>
        </descriptions>
    </resource>
.

Vérification Formelle des Aspects de Cohérence d’un Workflow net Abdallah Missaoui Ecole Nationale d’Ingénieurs de Tunis BP. 37 Le Belvédère, 1002 Tunis, Tunisia abdallah.missaoui@enit.rnu.tn Zohra Sbaï Ecole Nationale d’Ingénieurs de Tunis BP. 37 Le Belvédère, 1002 Tunis, Tunisia zohra.sbai@enit.rnu.tn Kamel Barkaoui Conservatoire National des Arts et Métiers Rue Saint Martin, 75141 Paris, France barkaoui@cnam.fr Résumé—Un processus workflow est un ensemble d’activités de forte granularité dont chacune réalise une tâche bien précise en consommant et/ou produisant des données. La vérification du bon fonctionnement de ces processus devient une question capitale vus leur complexité et le coût notable des pannes. Dans ce papier, nous exploitons des résultats récents de la théorie des processus workflow et les technologies de vérification basée sur le model checking. Nous proposons un outil de validation et de vérification de workflow net en utilisant SPIN model checker. Notre méthode repose sur l’analyse des spécifications Promela des processus workflow. Les propriétés de processus sont exprimées en langage temporelle linéaire (LTL) puis analysées par SPIN. Les résultats obtenus permettent l’identification et la vérification efficaces de plusieurs aspects de cohérence des processus workflow. Mots cl´es—Vérification, Processus Workflow, Cohérence, Mo- del checking, SPIN. I. INTRODUCTION La gestion des processus métier permet à une entreprise de rationnaliser les tâches successives et de diminuer le temps d’exécution des tâches pour chaque collaborateur. Un processus de workflow définit un ensemble d’activités et l’ordre qu’elles doivent suivre à l’exécution pour réaliser un but spécifique [9]. Au cours de l’exécution d’un processus de workflow, une activité peut être exécutée une, plusieurs fois ou jamais. Des décisions sur le choix de chemins (choix entre activités alternatives) doivent être prises. L’analyse des flux de travail permet ainsi d’identifier les processus dont le but est de renforcer leur traçabilité et d’informatiser l’élaboration des tâches. Une difficulté résiduelle porte surtout sur le paramétrage et la vérification des modèles représentant les processus ou les procédures modélisées. L’objectif de ce travail est de vérifier si un processus workflow satisfait une spécification représentant son comportement en utilisant la vérification de modèle. Nous présentons l’approche de notre outil qui permet en premier temps de traduire un processus workflow en modèle Promela, et par la suite, de lancer la vérification en utilisant l’outil SPIN. Cette vérification de comportement du processus se fait par rapport à une spéci- fication abstraite. Nous traitons le problème de la vérification des propriétés d’un processus workflow et nous analysons divers aspects de la cohérence d’un processus. Ce papier est organisé comme suit. Nous commençons dans la section 2 par présenter le modèle de workflow adopté. Les technologies du model checking ainsi que l’architecture de notre outil sont présentées dans la section 3. La section 4 décrit la traduction en Promela d’un workflow net. La méthode de vérification des propriétés et de la cohérence est détaillée dans les sections 5 et 6. II. MODELE DE WORKFLOW Les réseaux de Petri constituent un formalisme puissant pour l’expression du contrôle de flux dans un processus. Ils ont une sémantique formelle et fournissent un formalisme graphique. En outre, plusieurs techniques d’analyse pour les réseaux de Petri sont disponibles. La modélisation en réseau de Petri met en évidence le flux de contrôle intrinsèque à un processus et permet de définir les états des activités et des tâches, leurs conditions d’exécution et le flot d’événement les caractérisant. Un réseau de Petri (RdP) est un triplet N = (P, T, F) où : - P = {p1, p2, ..., pm} est un ensemble fini de places, - T = {t1, t2, ..., tn} est un ensemble fini de transitions, - F ⊆ (P × T) ∪ (T × P) est l’ensemble des arcs reliant les places aux transitions et vice versa. En utilisant le concept de conditions et d’événements, les places représentent les conditions et les transitions représentent les événements. Les liens entre les deux entités décrivent les relations de précédence, de parallélisme, de choix, etc. Chaque place contient un nombre entier positif ou nul de marques ou jetons. Le marquage M est une fonction M : P → N qui définit l’état du système décrit par le réseau à un instant donné. Un marquage initial M0 donné est noté par (N, M0). Le marquage M du WF-net est représenté par des jetons noirs répartis sur les places. Par exemple, M = (p1, 2p3) représente le marquage avec un jeton dans p1, deux jetons dans p3 et les autres places sont vides. Une transition possède un certain nombre de places d’entrée et de places de sortie représentant respectivement les post- conditions et les pré-conditions. Nous définissons le pré-ensemble et post-ensemble d’une place p et d’une transition t comme suit : • p = {t ∈ T | (t, p) ∈ F} p• = {t ∈ T | (p, t) ∈ F} • t = {p ∈ P | (p, t) ∈ F} t• = {p ∈ P | (t, p) ∈ F} Une transition t est dite franchissable si chaque place d’en- trée de t est marquée par au moins un jeton. Une transition franchissable peut comme elle ne peut pas être franchie. Le franchissement d’une transition t enlève un jeton de chacune des places d’entrées de t et ajoute un jeton à chaque place de sortie de t. Le franchissement est noté par M[t M . L’ensemble des marquages accessibles de M est noté par [M . e-STA copyright 2010 by see Volume 7, N°1, pp 37-41 Dans ce papier, Nous nous concentrons sur l’usage des réseaux de Petri comme un outil pour la représentation, la validation et la vérification des processus workflow. Un WF-net est un RdP particulier, introduit dans [2], possédant deux places spéciales : i et f. Ces places sont employées pour marquer le début et la fin d’un processus. Les tâches sont représentées par des transitions et l’ordre de ces tâches est représenté par des places reliant des transitions. Le traitement d’un cas commence le moment où un jeton est mis dans la place i et se termine le moment où un jeton apparaît dans la place f. un RdP N = (P, T, F) est un WF-net si et seulement si : i. N possède 2 places spéciales i et f. La place i est une place source (• i = ∅). La place f est une place puit (f• = ∅). ii. Si on ajoute une transition t∗ à N qui connecte f avec i, c’est à dire • t∗ = {f} et t∗• = {i} alors le RdP résultant est fortement connecté. Le modèle que nous adoptons est celui des réseaux de workflow (WF-net). Il nous permet de donner une description complète des différentes dimensions d’un processus métier tout en offrant des mécanismes de vérification des propriétés de ce processus. III. MODEL CHECKING Le model-checking est un ensemble de techniques de vérifi- cation automatique de propriétés temporelles sur des systèmes réactifs. Il permet de vérifier de manière très efficace que des systèmes de grande taille possèdent certaines propriétés. En premier temps, l’algorithme de model checking prend en entrée deux données : une abstraction du comportement du système réactif et un ensemble de propositions logiques atomiques temporelles. La logique temporelle est une forme de logique spécialisée dans les énoncés et raisonnements faisant intervenir la notion d’ordonnancement dans le temps [9]. Elle permet d’exprimer l’évolution de l’état d’un système. Ces propriétés peuvent être vues comme des comportements dynamiques. Le model Checking consiste, en deuxième temps, à exprimer la négation de la formule de logique temporelle que nous souhaitons tester. Il est capable, par la suite, de reconnaître exactement l’ensemble des exécutions satisfaisant la négation de la formule donnée. Plusieurs outils de model checking ont vu le jour tels que NuSMV, BLAST et SPIN. Dans ce papier nous adoptons SPIN model checker. SPIN est un outil de model checking, qui accepte le langage de spécification Promela (PROcess MEta LAnguage). Il permet de vérifier des propriétés exhaustivement. Dans ce travail, nous présentons une méthode, basée sur le model checking, pour la vérification des propriétés de cohérence d’un workflow net. La première étape consiste à traduire le WF-net en langage Promela. Par la suite, les propriétés sont exprimées comme des formules LTL (Logique Temporelle Linéaire). Relativement à cette spécification formelle du comportement du modèle, SPIN model checker vérifie si ces propriétés sont satisfaites. En effet, le mode de vérification de SPIN détermine si le modèle proposé en Promela satisfait ou non une propriété LTL. Spin transforme la negation de la propriété en automate de Büchi [10] et calcule par la suite suite le produit synchronisé de cet automate avec celui du système. Le résultat est encore un automate de Büchi dont il vérifie si le langage est vide ou non. S’il est vide, alors il n’existe aucune exécution violant la formule de départ. Si non, l’automate de Büchi accepte un mot. Donc, Il existe un cycle, atteignable depuis l’état iniatial, qui comporte un état accepté. Pour démontrer que toutes les exécutions du système sont valides vis-à-vis de la propriété à vérifier, il suffit de prouver qu’il n’existe pas de cycle accepté atteignable depuis l’état initial. FIGURE 1. Vue d’ensemble. La stratégie de vérification de SPIN se résume comme suit : il détermine l’espace des états correspondant. Par la suite, et afin de trouver un contre exemple, il applique l’algorithme de recherche en profondeur imbriquée sur l’espace des états. Le but est de trouver un cycle acceptable et donc un état atteignable à partir de l’état initial. Si la recherche aboutit à un résultat, la propriété en question n’est pas valide [5]. L’architecture globale de notre outil est donnée par la figure1. Les variables d’entrée de notre système sont : le workflow net donné sous forme d’un fichier PNML ainsi que les propriétés, que nous souhaitons vérifier, exprimées en langage LTL. IV. DESCRIPTION PROMELA D’UN WORKFLOW NET Une méthode de modélisation de réseau de Petri avec le langage Promela a été introduite par Holzmann dans [5], [6]. Dans cette méthode, un système de réseau de Petri est représenté comme un seul processus. Ce dernier décrit le franchissement de chacune des transitions de réseau de Petri en question. Les canaux de langage Promela ne sont pas utilisés. Cette spécification, d’un réseau de Petri en langage Promela, donnée dans [5], ne décrit que le marquage des places et ne prend pas en compte le nombre de franchissement des transitions. Toutefois, il est nécessaire d’enregistrer le nombre de fois une transition a été franchie lors de l’exécution du processus. Ces informations seront utilisées lors de l’analyse et la vérification des propriétés de cohérence d’un WF-net. D’autres travaux ont utilisé SPIN model checker pour la vérification des propriétés des réseaux de Petri. Les solutions proposées se limitent sur l’étude de la vivacité et la finitude [4] et la cohérence [8]. Cette section expose la définition en langage Promela d’un WF- net. Cette spécification décrit le comportement d’un Workflow net et ainsi le franchissement des transitions et les changements d’états à effectuer suite à ce franchissement. De plus, la spécifica- tion adoptée détermine le nombre de franchissements de chaque transition lors de l’exécution d’un processus. En résumé, notre spécification se focalise sur les règles suivantes : – Les transitions sont modélisées par un tableau TR d’entiers (initialisés à zéro) avec une longueur égale au nombre de transitions ; e-STA copyright 2010 by see Volume 7, N°1, pp 37-41 FIGURE 2. Exemple d’un workflow net. – Les places sont représentées par un tableau d’entiers PL avec une longueur égale au nombre de places. Les éléments de ce tableau sont tous initialisés à 0. Le déroulement d’un processus peut être décrit en termes d’états du système et les modifications apportées aux transitions. Un réseau workflow (WF-net) est formulé avec respect à un marquage initial consistant en un seul jeton dans la place initiale (M0 = i). Une transition t ∈ T est franchissable dans un marquage M si toutes ces places d’entrées sont marquées (∀p ∈ • t, M(p) > 0). Le franchissement de t conduit à un marquage M dans lequel le nombre de jetons dans toutes les places de sorties de t a été décrémenté de 1. Ces concepts sont traduits dans la spécification Promela d’un WF-net comme suit : Le franchissement d’une transition t consiste à décrémenter de 1 les éléments du tableau PL qui correspondent aux places d’entrées de t, et à incrémenter de 1 les éléments du même tableau correspondant aux places de sortie de t. De même, la case du tableau TR qui correspond à la transition franchie t, est incrémentée de 1. Ces traitements sont effectués grâce aux macros suivant OUT1, OUT2, ., OUTr et INP1, INP2, , INPs où s (respec- tivement r) correspond au nombre maximal de places d’entrée (respectivement de sortie) à une transition t du WF-net en question. La figure 3 présente la spécification en langage Promela du workflow net donné dans la figure 2. V. VERIFICATION A. Terminaison La terminaison est une propriété importante pour un Work- flow net. Cette propriété donne une garantie que le processus commence et termine l’exécution jusqu’à la fin. La place finale f modélise cette terminaison. Formellement : M ∈ [Mi La terminaison pourra être vérifiée en utilisant des algorithmes standards basés sur la génération des graphes de marquage. Cependant, les techniques de model checking exigent une déclaration précise et non ambiguë des propriétés décrites dans la formule. La propriété de terminaison est traduite en logique temporelle linéaire comme suit : ♦ (PL[indice de f] ≥ 1) B. Terminaison propre La terminaison propre d’un modèle de Workflow suggère que la procédure puisse terminer pour tout cas et qu’au moment où le processus se termine, il y a un seul jeton à la place f et toutes les autres places sont vides. Formellement : ∀M ∈ [Mi : M(f) ≥ 1 ⇒ M = Mf ; FIGURE 3. Spécification d’un WF-net en langage Promela. Nous pouvons vérifier la propriété de terminaison propre en évaluant la formule LTL suivante : (PL[indice de f] ≥ 1 ⇒ PL = [f]) C. Vivacité Il est important de vérifier que le processus ne contient pas des propriétés indésirables. A partir de l’état initial caractérisé par un jeton à la place i, il devrait être possible d’exécuter une tâche aléatoire en suivant la voie adéquate à travers le WF-net et qu’il n’y aura pas de transitions mortes. Formellement : ∀t ∈ T, ∃M ∈ [Mi / M[t . La vivacité implique donc qu’il n’y a aucune transition morte dans le WF-net. Cette propriété se traduit en langage LTL par : ¬( (∃t ∈ T, TR[indice de t] = 0)) Pour vérifier qu’une transition donnée t0 n’est pas vivante, la formule LTL suivante pourrait être utilisée : (TR[t0] = 0) Cette formule est vraie si t0 n’a jamais été franchie (TR[t0] est toujours égale à 0). VI. VERIFICATION DE LA COHERENCE Un processus définit les activités ainsi que leur exécution. Il pourrait être représenté en remplaçant son unique entrée c’est- à-dire son nœud initial par une place ne possédant aucun arc d’entrée, et son unique nœud de sortie par une place ne possédant aucun arc de sortie. Les conditions seront représentées par les places et les tâches par les transitions. Cette modélisation, sous forme d’un workflow net, a été introduite par Van der aalst [1]. La terminaison propre d’un modèle de workflow suggère que la procédure termine pour tout cas, et la quasi-vivacité affirme l’absence de tâches mortes. Ces deux propriétés définissent la cohérence qui est un critère très important qu’un WF-net devrait satisfaire. Plusieurs définitions du concept de la cohérence ont été proposées. Ces définitions plus adaptées à la vérification des processus de workflow, ont été introduites dans [3], [7], dont chacun e-STA copyright 2010 by see Volume 7, N°1, pp 37-41 FIGURE 4. Exemple d’un réseau de Petri. prend en considération certains aspects spécifiques du processus de workflow exécuté. Dans cette section, nous présentons les différents types de cohérence et nous décrivons notre méthode de vérification des propriétés de chacune d’entre elles. A. Structure d’un WF-net Dans cette section, nous proposons de vérifier que la spécifica- tion Promela à analyser avec SPIN est sémantiquement correcte. C’est-à-dire qu’elle représente bien un WF-net. Comme exemple de violation de cette propriété nous citons l’existence de transitions sans sorties ou places sans entrées. Definition 1: Un RdP N = (P, T, F) est structurellement correct si et seulement si : i. N possède une seule place sans entrée nommée i (• i = ∅) et une seule place sans sortie notée f(f• = ∅). ii. pour chaque x de P ∪ T, il y a un chemin de i à x et un chemin de x à f. Ce type d’erreur peut être vérifié directement en analysant le code Promela associé au modèle en question. Pour chacune des transitions du WF-net, une ligne de code Promela est ajoutée pour décrire le franchissement de la transition. De même, les macros OUTx permettent de supprimer un jeton d’une place. Il est donc possible de détecter les erreurs structurelles à travers l’analyse du code Promela. La figure 4 représente un exemple d’un réseau de Petri qui n’est pas structurellement correct. Toutefois, dans la pratique, ce type de vérification est nécessaire pour s’assurer que la structure du modèle de processus en question est bien conforme à celle d’un WF-net. Dans la suite de ce papier, nous supposons que les modèles à analyser sont tous des WF-nets. B. La cohérence faible Le concept de la cohérence faible a été introduit par Martens [7] dans le contexte de processus métier. Cette propriété exige qu’une instance commencée se termine mais autorise le processus en question à ne pas exécuter toutes les tâches. La propriété de faible cohérence (en anglais : weak soundness property) veut dire pour n’importe quel cas, le processus se terminera, et au moment où il se termine il y a un jeton dans la place f et toutes les autres places sont vides. Un processus workflow modélisé par un WF-net N = (P, T, F) est dit faible-cohérent si et seulement si : i. Pour chaque marquage M accessible à partir du marquage initial i, il existe une séquence active conduisant de M au marquage final f. Formellement : M ∈ [Mi ii. L’état Mf est le seul état accessible à partir de l’état Mi. Formellement :∀M ∈ [Mi : M(f) ≥ 1 ⇒ M = f. En se basant sur les définitions présentées dans la section 4, la notion de faible-cohérence pourra être réécrite en LTL comme suit : Definition 2: Un workflow net N = (P, T, F) est dit faible- cohérent si et seulement si : i. ♦ (PL[indice de f] ≥ 1) ii. (PL[indice de f] ≥ 1 ⇒ PL = [f]) C. La cohérence La terminaison propre d’un modèle de workflow suggère que la procédure puisse terminer pour tout cas, et la quasi-vivacité affirme l’absence de tâches mortes. Ensemble, ces deux propriétés définissent la cohérence. Un processus modélisé par un WF-net N = (P, T, F) est dit cohérent si et seulement si : i. Pour chaque marquage M accessible à partir d’un mar- quage initial Mi, il existe une séquence active conduisant de M au marquage final Mf . Formellement : M ∈ [Mi ii. L’état Mf est le seul état accessible à partir de l’état Mi. Formellement : ∀M ∈ [Mi : M(f) ≥ 1 ⇒ M = f; iii. Il n’y a aucune transition morte dans (N, i). Formelle- ment : ∀t ∈ T, ∃M ∈ [Mi : M[t . La définition de cohérence peut être réécrite, en se basant sur les formules LTL, comme suit : Definition 3: Un workflow net N = (P, T, F) est dit cohérent si et seulement si : i. ♦ (PL[indice de f] ≥ 1) ii. (PL[indice de f] ≥ 1 ⇒ PL = [f]) iii. ¬( (∃t ∈ T, TR[indice de t] = 0)) D. La K-cohérence La k-cohérence est une des extensions de la propriété de la cohérence [3]. Un WF-net est dit k-cohérent si et seulement si : i. Pour chaque marquage M accessible à partir d’un mar- quage initial k.i, il existe une séquence active conduisant de M au marquage final (terminaison des k instances). Formellement : ∀M ∈ [k.i , k.f ∈ [M ii. Un état f est le seul état accessible à partir d’un état i avec au moins k jetons à la place f. Formellement : ∀M ∈ [k.i : M(f) ≥ k ⇒ M = k.f iii. Il n’y a aucune transition morte dans (N, i). (N, k.i) quasi- vivant. Formellement : ∀t ∈ T, ∃M ∈ [Mk.i : M[t . Afin de vérifier la k-cohérence, nous devons modifier notre spécification en langage Promela. En effet, le premier élément du tableau PL doit être initialisé à k (k est une constante). Ceci nous permet de modéliser le cas de k jetons à la place i à l’état initial. La définition de la k-cohérence est traduite, en se basant sur les formules LTL, comme suit Definition 4: Un Workflow net N = (P, T, F) est dit k-cohérent si et seulement si : i. ♦ (PL[indice de f] ≥ k) ii. (PL[indice de f] ≥ 1 ⇒ PL = [k.f]) iii. ¬( (∃t ∈ T, TR[indice de t] = 0)) VII. CONCLUSION Dans ce papier, nous avons proposé une méthode basée sur le model checking de vérification des propriétés d’un workflow. Cette vérification a porté sur plusieurs aspects de cohérence. Nous avons proposé d’abord une traduction de workflow net en langage Promela. Ensuite, nous avons décrit les conditions des différents aspects de cohérence en logique temporelle linéaire. Les résultats de de travail sont appliquables uniquement aux WF-nets sans cycles. En effet, il n’est pas possible de prévoir la progression des états de système dans le cas où le modèle e-STA copyright 2010 by see Volume 7, N°1, pp 37-41 présente des boucles. Les perspectives de ce travail porteront sur une analyse plus approfondie des propriétés d’un WF-net à contraintes tempo- relles et une étude de la composition des processus workflow. RÉFÉRENCES [1] W.M.P. Van der Aalst, "The Application of Petri Nets to Workflow Management", The Journal of Circuits, Systems and Computers, vol. 8, pp. 21-66, 1998. [2] W.M.P. Van der Aalst, "Verification of Workflow nets". ICATPN 97, LNCS, vol. 1248, 1997. [3] K. Barkaoui, R. Ben Ayed, Z. Sbaï, "Workflow Soundness Veri- fication based on Structure Theory of Petri Nets", International Journal of Computing and Information Sciences (IJCIS), Vol. 5(1), pp. 51-61, 2007. [4] G. C. Gannod, S. Gupta, "An automated tool for analysing Petri nets using SPIN", In Proceeding of International Conference on Automated Software Engineering, 2001. [5] G. J. Holzmann,"The SPIN Model Checker", Primer and Reference Manual, Addison-Wesley, 2003. [6] G. J. Holzmann, "The Model Checker SPIN", IEEE Transactions on software engineering, vol.23, no.5, 1997. [7] A. Martens, "Analyzing web service based business processes", In the Proceedings of International Conference on Fundamental Approaches to Software Engineering, Part of the European Joint Conferences on Theory and Practice of Software, Lecture Notes in Computer Science vol. 3442, Springer-Verlag, 2005. Tech. Rep., Workflow Management Coalition, Brussals, (1999). [8] S. Yamaguchi, M. Yamaguchi, M. Tanaka, "A soundness verification tool based on the SPIN model checker for acyclic workflow nets", In the proceeding of ITC-CSCC, 2008. [9] WFMC. : Workflow management coalition terminology and glossary (WFMC-TC-1011). Tech. Rep., Workflow Management Coalition, Brussals, 1999. [10] M.Y. Vardi, P. Wolper, "An automata-theoretic approach to auto- matic program verification", Proc. First IEEE Symp. on Logic in Computer Science, pp. 322-331, 1986. e-STA copyright 2010 by see Volume 7, N°1, pp 37-41