, Xfig version 3.2 user manual

T. Aaltonnen, M. Katara, and R. Pitkänen, DisCo Toolset -The New Generation, G. SCHELLHORN et W. REIF, réds., The 4th Workshop on Tools for System Design and Verification, FMTOOLS'2000, pp.11-16

M. Abadi and L. Lamport, Conjoining Specifications. ACM Toplas, vol.17, issue.3, pp.507-534

J. A. , The B Book -Assigning Programs to Meanings

K. Ajami, S. Haddad, and J. M. Ilié, Exploiting Symmetry in Linear Time Temporal Logic Model Checking: One Step Beyond, B. STEFFEN, réd., Tools and Algorithms for Construction and Analysis of Systems, TACAS'98, vol.1384, pp.52-67
URL : https://hal.archives-ouvertes.fr/hal-02547727

M. Allemand, Verification of properties involving logical and physical timing features, Génie Logiciel & Ingénierie de Systèmes & leurs Applications, ICSSEA'2000

M. Allemand, C. Attiogbé, and H. Habrias, International Workshop on Comparing Systems Specification Techniques -What questions are prompted by ones particular method of specification?

L. A. Álvarez, J. M. Murillo, F. Sánchez, and J. Hernández, ActiveJava, un modelo de programación concurrente orientado a objeto, III Jornadas de Ingenería del Software

S. Andova, Process algebra with probabilistic choice, Lecture Notes in Computer Science, vol.1601, pp.111-129

S. Andova, Time and Probability in Process Algebra, T. RUS, réd., International Conference on Algebraic Methodology And Software Technology (AMAST'2000), vol.1816, pp.323-338

P. André, Méthodes formelles et à objets pour le développement du logiciel : Etudes et propositions

P. André, Spécification de l'atelier ASFO

P. André, D. Chiorean, and J. Royer, The formal class model, Joint Modular Languages Conference, pp.59-78

P. André and J. Royer, How To Easily Extract an Abstract Data Type From a Dynamic Description, Research Report, vol.159

P. André and J. Royer, An Algebraic Approach to Heterogeneous Software Systems

P. Argon, Etude sur l'application de méthodes formelles à la compilation et à la validation de programmes Electre

A. Arnold, Systèmes de transitions finis et sémantique des processus communicants. Etudes et recherches en informatique

E. Astesiano and G. Reggio, Formalism and method, M. BIDOIT et M. DAUCHET, réds., TAPSOFT'97, vol.1214, pp.93-114

E. Astesiano-;-l, A. Andrade, A. Moreira, S. Deshpande, and . Kent, UML as heterogeneous multiview notation. strategies for a formal foundation, Proceedings of the OOPSLA'98 Workshop on Formalizing UML. Why? How?, ????

E. Astesiano, M. Broy, and G. Reggio, Algebraic Foundations of System Specification, chapter Algebraic Specification of Concurrent Systems

E. Astesiano, M. Cerioli, and G. Reggio, Pluggin Data Constructs into Paradigm-Specific Languages: Towards an Application to UML, T. RUS, réd., International Conference on Algebraic Methodology And Software Technology (AMAST'2000), vol.1816, pp.273-292

E. Astesiano and G. Reggio, Algebraic Specification of Concurrency, M. BIDOIT et C. CHOPPY, réds., Recent Trends in Data Type Specification, vol.655, pp.1-39

E. Astesiano and G. Reggio, Labelled Transition Logic: An Outline

E. Astesiano, G. Reggio, and F. Morando, The SMoLCS ToolSet. In P. D. MOSSES, M. NIEL-SEN et M. I. SCHWARTZBACH, réds., TAPSOFT'95: Theory and Practice of Software Development, vol.915, pp.801-802

E. Astesiano and E. Zucca, D-oids: a model for dynamic data-types, Mathematical Structures in Computer Science, vol.5, issue.2, pp.257-282

J. C. Attiogbé, Configuration Machines: A Simple Formalism for Specifying Multifaceted Systems

J. C. Attiogbé, Génération de code Promela pour la simulation et la vérification, International Conference on Software and Systems Engineering and their Applications, ICSSEA, ????

J. C. Attiogbé, Système de controle d'accès : une spécification à base des machines à configurations, Approches Formelles dans l'Assistance au Développement de Logiciels, AFADL, ????

J. Aycock, Compiling Little Languages in Python, 7th International Python Conference

B. Barras, S. Boutin, C. Cornes, J. Courant, Y. Coscoy et al., The Coq Proof Assistant Reference Manual: Version 6.2.4. Rapport technique, INRIA, ????
URL : https://hal.archives-ouvertes.fr/inria-00069968

T. Basten and J. Hooman, Process Algebra in PVS, R. CLEAVELAND, réd., Tools and Algorithms for Construction and Analysis of Systems (TACAS), vol.1579, pp.270-284

R. Bastide and P. Palanque, Cooperative Objects : a Concurrent Petri Net Based Object-Oriented Language, IEEE / System Man and Cybernetics 93

R. Bastide, Approaches in unifying Petri nets and the Object-Oriented Approach, 1st Workshop on Object-Oriented Programming and Models of Concurrency

E. Battiston, A. Chizzoni, and F. D. Cindio, Inheritance and Concurrency in CLOWN, 1st Workshop on Object-Oriented Programming and Models of Concurrency

E. Battiston, F. D. Cindio, and G. Mauri, Modular Algebraic Nets to Specify Concurrent Systems, IEEE Transactions on Software Engineering, vol.22, issue.10, pp.689-705

D. M. Beazley, SWIG : An Easy to Use Tool For Integrating Scripting Languages with C and C++, 4th Annual USENIX Tcl/Tk Workshop, pp.287-294

J. A. Bergstra, J. Heering, and P. Klint, Algebraic Specification

J. A. Bergstra and J. W. , of CWI Monograph, chapter Process algebra: Specification and verification in bisimulation semantics, KLOP. Math. & Comp. Sci, vol.II

G. Berry and G. Gonthier, The ESTEREL synchronous programming language : design, semantics, implementation, Inria
URL : https://hal.archives-ouvertes.fr/inria-00075711

O. Biberstein, D. Buchs.-;-g, F. Agha, . De, and R. Cindio, Workshop on Object-Oriented Programming and Models of Concurrency'95, pp.131-145

O. Biberstein, D. Buchs, N. Guelf-;-g, F. Agha, . De et al., Advances in Petri Nets on Object-Orientation, Lecture Notes in Computer Science

O. Biberstein, D. Buchs, and N. Guelfi, CO-OPN/2: A Concurrent Object-Oriented Formalism, Second IFIP Conf. on Formal Methods for Open Object-Based Distributed Systems (FMOODS), pp.57-72

M. Bidoit, C. Choppy, and F. Voisin, Validation d'une spécification algébrique du "Transit-node" par prototypage et démonstration de théorèmes. Chapitre du Rapport final de l'Opération VTT, Validation et vérification de propriétés Temporelles et de Types de données, LaBRI

M. Bidoit, Types abstraits algébriques : spécifications structurées et présentations gracieuses, Colloque AFCET, Les mathématiques de l'informatique, pp.347-357

B. W. Boehm, Verifying and Validating Software Requirements and Design Specifications, IEEE Software, vol.1, issue.1, pp.75-88

E. Boiten, H. Bowman, J. Derrick, and M. Steen, Viewpoint consistency in Z and LOTOS: A case study, FME'97, Formal Methods: Their Industrial Application and Strengthened Foundations

T. Bolognesi and E. Brinksma, Introduction to the ISO Specification Language LOTOS. Computer Networks and ISDN Systems, vol.14, pp.25-29

P. Borovansky, C. Kirchner, H. Kirchner, P. Moreau, and C. Ringeissen, An Overview of ELAN, réds., 2nd International Workshop on Rewriting Logic and its Applications, WRLA'98, vol.15
URL : https://hal.archives-ouvertes.fr/inria-00098518

R. Boulton, A. Gorgon, M. Gordon, J. Hebert, and J. Van-tassel, Experience with embedding hardware description language in hol, International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, pp.129-156

E. Börger and D. Rosenzweig, A Mathematical Definition of Full Prolog, Science of Computer Programming, vol.24, issue.3, pp.249-286

E. Börger and W. Schulte, Programmer Friendly Modular Definition of the Semantics of Java, Lecture Notes in Computer Science, vol.1523, pp.353-404

J. Briot and R. Guerraoui, Objets pour la programmation parallèle et répartie : intérêts, évolutions et tendances. Technique et science informatiques, vol.15, pp.765-800

S. D. Brookes, C. A. Hoare, and A. W. Roscoe, A Theory of Communicating Sequential Processes, Journal of the ACM, vol.31, issue.3, pp.560-599

M. Broy-;-h, C. Ehrig, M. Floyd, J. Nivat, and . Thatcher, Specification and top down design of distributed systems, Lecture Notes in Computer Science, vol.185, pp.4-28

M. Broy, C. Facchi, R. Grosu, R. Hettler, H. Hussmann et al., The Requirement and Design Specification Language SPECTRUM. Rapport technique TUM-I9140

M. Broy and M. Wirsing, Algebraic State Machines, T. RUS, réd., International Conference on Algebraic Methodology And Software Technology (AMAST'2000), vol.1816, pp.89-118

G. Bruns, Distributed Systems Analysis with CCS. International Series in Computer Science

N. Busi, L. Capra, and A. Chizzoni, Representing Dynamic Aspects of a Concurrent OO Formalism by Mobile Nets, 11th European Conference on Object-Oriented Programming (ECOOP'97)

R. Büssow, R. Geisler, W. Grieskamp, and M. Klar, The µSZ Notation Version 1.0, vol.13

R. Büssow, R. Geisler, W. Grieskamp, and M. Klar, Integrating Z with Dynamic Modeling Techniques for the Specification of Reactive Systems

R. Büssow, W. Grieskamp, F. Lattemann, and E. Lehmann, The Definition of Dynamic Z. ESPRESS Projektbericht

M. Butler, csp2B: A practical approach to combining CSP and B, réds., FM'99-Formal Methods, vol.I, pp.490-508

A. J. Camilleri, P. Inverardi, and M. Nesi, Combining interaction and automation in process algebra verification, Advances in Distributed Computing (ADC) and Colloquium on Combining Paradigms for Software Developmemnt (CCPSD), vol.2, pp.283-296

E. Canver and F. W. Henke, Formal Specification and Verification of Object-Based Systems in a Temporal Logic Setting

D. Caromel and J. Vayssière, A Java Framework for Seamless Sequential, Multi-threaded, and Distributed Programming, ACM Workshop "Java for High-Performance Network Computing, pp.141-150

, Recommendation Z.100: Specification and Description Language SDL, blue book, volume x.1 édition, ????

K. M. Chandy and J. Misra, Parallel Program Design: A Fundation

B. Chetali-;-in, U. H. Eng-berg, K. G. Larsen, and A. Skou, Formal verification of concurrent program using the Larch Prover, Proceedings of the Workshop on Tools and Algorithms for The Construction and Analysis of Systems, pp.174-186, 1995.

C. Choppy, P. Poizat, and J. Royer, A Global Semantics for Views, T. RUS, réd., International Conference on Algebraic Methodology And Software Technology (AMAST'2000), vol.1816, pp.165-180
URL : https://hal.archives-ouvertes.fr/hal-01135611

C. Choppy, P. Poizat, J. Royer-;-h, M. Ehrig, F. Grosse-rhode et al., Integration and Composition of Static and Dynamic "Views": Unifying Approach to Complex System Specification, Workshop on Integration of Specification Techniques with Applications in Engineering, pp.12-20, 2000.
URL : https://hal.archives-ouvertes.fr/hal-01135631

C. Choppy, P. Poizat, and J. Royer, Specification of Mixed Systems in KORRIGAN with the Support of an UML-Inspired Graphical Notation, Fundamental Approaches to Software Engineering (FASE'2001)

C. Choppy, P. Poizat, J. R. The, and . Environment, Journal of Universal Computer Science, ????. Special issue: Tools for System Design and Verification, pp.948-6968

S. Christensen, J. B. Jørgensen, and L. M. Kristensen, Design/CPN -A Computer Tool for Coloured Petri Nets, E. BRINKSMA, réd., Tools and Algorithms for Construction and Analysis of Systems, TACAS'97, vol.1217, pp.209-223

R. Clark-;-c, R. Rat-tray, and . Clark, Using LOTOS in the Object-Based Development of Embedded Systems, pp.307-319

E. Clarke, O. Grumberg, and D. Long, Verification tools for finite-state concurrent systems, A Decade of concurrency -Reflections and Perspectives, vol.803

E. M. Clarke, E. A. Emerson, and A. P. Sistla, Automatic Verification of Finite-State Concurrent Systems using Temporal Logic Specifications, ACM Transactions on Programming Languages and Systems, vol.8, issue.2, pp.244-263

C. Examples, , vol.79

, The Common Framework Initiative for Algebraic specification and development, electronic archives. Notes and Documents accessible by WWW 1 and FTP 2 , ????

. Cofi, . Design, and . Group, CASL -The CoFI Algebraic Specification Language -Summary (version 1.0). Documents/CASL/Summary

C. Reactive and . Group, The CoFI-Reactive Systems Group Home Page . ReactiveSys-temsTaskGroup.html

S. Conrad, Compositional Object Specification and Verification, I. ROZ-MAN et M. PIVKA, réds., Proc. of the Int. Conf. on Software Quality (ICSQ'95), pp.55-64

E. Coscia and G. Reggio, JTN: A Java-Targeted Graphic Formal Notation for Reactive and Concurrent Systems, Fundamental Approaches to Software Engineering (FASE'99), vol.1577, pp.77-97

G. Costa and G. Reggio, Specification of abstract dynamic data types: A temporal logic approach, Theoretical Computer Science, vol.73, issue.2

P. Dauchy and M. Gaudel, Algebraic Specifications with Implicit State, Working papers of the international Workshop on Information System Correctness and Reusability, IS-CORE'93, ????

J. Davies and S. Schneider, A brief history of Timed CSP, Theoretical Computer Science, vol.138, issue.2, pp.243-271

G. Delzanno and A. Podelski, Model checking in clp, R. CLEAVELAND, réd., TACAS'99, International Conference on Tools and Algorithms for the Construction and Analysis of Systems, vol.1579, pp.223-239

G. Denker and H. E. , Specifying Distributed Information Systems: Fundamentals of an Object-Oriented Approach Using Distributed Temporal Logic, 2nd International IFIP Workshop on Formal Methods for Open Object-Based Distributed Systems

G. Denker and P. Hartel, TROLL -An Object Oriented Formal Method for Distributed Information System Design: Syntax and Pragmatics

G. Denker and J. Küster-filipe, Towards a Model for Asynchronously Communicating Objects, H.-M. HAAV et B. THALHEIM, réds., 2nd Int. Baltic Workshop on Databases and Information Systems, pp.182-193

G. Denker, J. Ramos, C. Caleiro, and A. Sernadas, A Linear Temporal Logic Approach to Objects with Transactions, M. JOHNSON, réd., Sixth Int. Conf. on Algebraic Methodology and Software Technology (AMAST'97), vol.1349, pp.170-184

J. Derrick, E. Boiten, H. Bowman, and M. Steen, Weak refinement in Z, Lecture Notes in Computer Science, vol.1212, p.369

J. Derrick, H. Bowman, E. A. Boiten, and M. Steen, Comparing LOTOS and Z refinement relations, FORTE/PSTV'96, pp.501-516

N. Dershowitz and J. Jouannaud, Rewrite Systems, volume B of Handbook of Theoretical Computer Science, pp.243-320

R. Diaconescu and K. Futatsugi, CafeOBJ Report -The Language, Proof Techniques, and Methodologies for Object-Oriented Algebraic Specification, AMAST Series in Computing. World Scientific, vol.6

A. M. Dinis-moreira, Rigorous Object-Oriented Analysis

R. Duke, G. Rose, and G. Smith, Object-Z: A specification language advocated for the description of standards, Computer Standards and Interfaces, vol.17, pp.511-533

H. Ehrich, C. Caleiro, A. Sernadas, and G. Denker, Logics for Databases and Information Systems, chapter Logics for Specifying Concurrent Information Systems, pp.167-198

H. Ehrich, G. Denker, A. Sernadas-;-c, J. Gaudel, and . Jouannaud, Constructing Systems as Object Communities, Theory and Practice of Software Development (TAPSOFT'93), vol.668, pp.453-467

H. Ehrig and B. Mahr, Fundamentals of Algebraic Specification, vol.1

H. Ehrig and F. Orejas, integration paradigm for data type and process specification techniques". Bulletin of EATCS -Formal Specification Column

H. Ehrig, R. Geisler, M. Klar, and J. Padberg, Horizontal and vertical structuring techniques for statecharts, CONCUR'97 : Concurrency Theory, vol.1243, pp.181-195

H. Ehrig and F. Orejas, Integration and Classification of Data Type and Process Specification Techniques

R. Ekkart, P. Graubmann, and J. Grabowski, Tutorial on Message Sequence Charts. Computer Networks and ISDN Systems, vol.28, pp.1629-1641

R. Ekkart, P. Graubmann, and J. Grabowski, Tutorial on Message Sequence Charts (MSC'96), Tutorials of the First Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, and Protocol Specification, Testing, and Verification (FORTE/PSTV'96)

J. Ellsberger, D. Hogrefe, and A. Sarma, SDL : Formal Object-oriented Language for Communicating Systems

U. Engberg, P. Grønning, and L. Lamport, Mechanical Verification of Concurrent Systems with TLA, Fourth International Workshop on Computer-Aided Verification, CAV'92

M. N. Orejas and A. Sanchez, Implementation and behavioural equivalence: a survey, Lecture Notes in Computer Science, vol.655, pp.93-125

J. Fernandez, C. Jard, T. Jéron, and C. Viho, Using on-the-fly verification techniques for the generation of test suites, A. ALUR et T. HENZINGER, réds., Conference on Computer-Aided Verification (CAV '96), vol.1102
URL : https://hal.archives-ouvertes.fr/inria-00073711

J. Fernandez, ALDEBARAN : un système de vérification par réduction de processus communicants

J. Fernandez, H. Garavel, A. Kerbrat, R. Mateescu, L. Mounier et al., CADP: A Protocol Validation and Verification Toolbox, 8th Conference on Computer-Aided Verification, pp.437-440

J. L. Fiadeiro and T. M. , Sometimes "Tomorrow" is "Sometime". Action Refinement in a Temporal Logic of Objects, D. GABBAY et H. OHLBACH, réds., Temporal Logic, vol.827, pp.48-66

A. Finkel and L. Petrucci, Propriétés de la composition/décomposition de réseaux de Petri et de leurs graphes de couverture, vol.28, pp.73-124

C. Fischer, Combining csp and z. Rapport technique TRCF-97-1

C. F. Csp-oz-;-z, C. In, H. Bowman, and J. Derrick, Proc. 2nd IFIP Workshop on Formal Methods for Open Object-Based Distributed Systems (FMOODS), pp.423-438

C. P. Fischer-;-j, A. Bowen, M. G. Fett, and . Hinchey, How to Combine Z with a Process Algebra, Lecture Notes in Computer Science, vol.1493, pp.5-23

F. Moller and C. Tofte, A temporal calculus of communicating systems (tccs), CONCUR-90: Theories of Concurrency, vol.458, pp.401-415

C. Fournet and G. Gonthier, The reflexive chemical abstract machine and the join-calculus, Proceedings of the 23rd ACM Symposium on Principles of Programming Languages, pp.21-24

C. Fournet, G. Gonthier, J. Lévy, L. Maranget, and D. Rémy, A calculus of mobile agents, 7th International Conference on Concurrency Theory (CONCUR'96), pp.26-29

R. France and B. Rumpe, UML'99 -The Unified Modelling Language, Lecture Notes in Computer Science, vol.1723

N. E. , FUCHS. Specifications are (Preferably) Executable. Software Engineering Journal, vol.7, issue.5, pp.323-334

K. Futatsugi, J. A. Goguen, J. Jouannaud, and J. Meseguer, Principles of OBJ2, Conference Record of the Twelfth Annual ACM Symposium on Principles of Programming Languages, pp.52-66

A. J. Galloway and W. Stoddart, An operationnal semantics for zccs, réds., International Conference of Formal Engineering Methods (IFCEM)

A. Galloway, Integrated Formal Methods with Richer Methodological Profiles for the Development of Multi-Perspective Systems

H. Garavel, Compilation et vérification de programmes LOTOS

H. Garavel, Introduction au langage LOTOS. Rapport technique, VERILOG, Centre d'Etudes, Forum du Pré Milliet

H. Garavel and C. Rodriguez, An example of LOTOS Specification : The Matrix Switch Problem, Rapport SPECTRE C22, Laboratoire de Génie Informatique -Institut IMAG

S. Garland and J. Guttag, An overview of LP, the Larch Prover, Proc. of the Third International Conference on Rewriting Techniques and Applications, vol.355, pp.137-151

M. Gaudel, A first introduction to PLUSS

J. Goguen, C. Kirchner, H. Kirchner, A. Megrelis, J. Meseguer et al., An introduction to OBJ-3, Proceedings 1st International Workshop on Conditional Term Rewriting Systems, vol.308, pp.88-89

M. J. Gordon and T. F. Melham, Introduction to HOL: A theorem proving environment for higher order logic

J. Gosling and . Steele, The Java Language Specification

B. Grahlmann, Combining Finite Automata, Parallel Programs and SDL Using Petri Nets, Proceedings of TACAS'98 (Tools and Algorithms for the Construction and Analysis of Systems), vol.1384, pp.102-117

W. Grieskamp, M. Heisel, and H. Dörr, Specifying Embedded Systems with Statecharts and Z: An Agenda for Cyclic Software Components, E. ASTESIANO, réd., FASE'98, vol.1382, pp.88-106

N. Guelfi, O. Biberstein, D. Buchs, E. Canver, M. Gaudel et al., Comparison of object-oriented formal methods. Technical report of the esprit long term research project 20072 "design for validation

P. Guernic, T. Gautier, M. Borgne, and C. Maire, Programming real-time applications with SIGNAL, Proceedings of the IEEE, vol.79, issue.9, pp.1305-1320
URL : https://hal.archives-ouvertes.fr/inria-00075114

R. G. , Les langages concurrents à objets, Technique et science informatiques, vol.14, issue.8, pp.945-971

Y. G. , draft of the asm guide, 1997.

N. Halbwachs, F. Lagnier, and C. Ratel, Programming and verifying critical systems by means of the synchronous data-flow programming language Lustre, septembre ????. Special Issue on the Specification and Analysis of Real-Time Systems, vol.18

N. Halbwachs, X. Nicollin, P. Raymond, D. Weber-;-f, C. Cassez et al., MOVEP'98 -MOdélisation et VErification des processus Parallèles, pp.1-7

D. Harel, On Visual Formalisms, Communications of the ACM, vol.31, issue.5, pp.514-530

D. Harel, H. Lachover, A. Naamad, A. Pnueli, M. Politi et al., STATEMATE: A Working Environment for the Development of Complex Reactive Systems, IEEE Transactions on Software Engineering, vol.16, issue.3, pp.403-414

D. Harel and A. Naamad, The statemate semantics of statecharts, ACM Transactions on Software Engineering and Methodology, vol.5, issue.4, pp.293-333

I. J. Hayes and C. B. Jones, Specifications are not Necessary Executable. Software Engineering Journal, vol.4, issue.6, pp.330-338

M. Heisel, Agendas -A Concept to Guide Software Development Activities, pp.19-32, 2000.

M. Heisel and N. Lévy, Using LOTOS Patterns to Characterize Architectural Styles, M. BI-DOIT et M. DAUCHET, réds., TAPSOFT'97, vol.1214, pp.818-832

M. Heisel and C. Suhl, Formal specification of safety-critical software with Z and real-time CSP, E. SCHOITSCH, réd., SAFECOMP'96: 15th International Conference on Computer Safety, Reliability and Security, p.31

M. Heisel and C. Suhl, Methodological Support for Formally Specifying Safety-Critical Software, 16th International Conference on Computer Safety, Reliability and Security, pp.295-308

M. Hennessy and H. Lin, Symbolic Bisimulations. Theoretical Computer Science, vol.138, issue.2, pp.353-389

B. Hnatkowska and H. Zbigniew, Extending the UML with a Multicast Synchronisation, Proceedings of the third Rigorous Object-Oriented Methods Workshop (ROOM), pp.1-902505

C. Hoare, Proof of Correctness of Data Representations, Acta Informatica, vol.1, pp.271-281

C. Hoare, Communicating Sequential Processes, Communications of the ACM, vol.21, issue.8, pp.666-677

G. J. Holzmann, The Spin Model Checker, IEEE Transactions on Software Engineering, vol.23, issue.5, pp.279-295

. Iso/iec and . Estelle, A Formal Description Technique based on an Extended State Transition Model. ISO/IEC 9074, International Organization for Standardization

. Iso/iec and . Lotos, A Formal Description Technique based on the Temporal Ordering of Observational Behaviour. ISO/IEC 8807, International Organization for Standardization

Z. Itu-t.-recommendation, Message Sequence Chart (MSC), vol.120

C. S. Jensen, J. Clifford, R. Elmasri, S. K. Gadia, P. Hayes et al., A Consensus Glossary of Temporal Database Concepts, SIGMOD Record (ACM Special Interest Group on Management of Data), vol.23, issue.1, pp.52-64

K. Jensen, Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use. Monographs in Theoretical Computer Science

C. B. Jones, Systematic Software Development Using VDM

M. Jourdan and F. Maraninchi, A modular state/transition approach for programming realtime systems, ACM Sigplan Workshop on Language, compiler and tool support for real-time systems

H. Järvinen and R. Kurki-suonio, DisCo specification language: marriage of actions and objects, 11th International Conference on Distributed Computing Systems, pp.142-151

S. T. Kalvala-;-e, P. J. Schubert, J. Windley, and R. Alves-foss, Higher Order Logic Theorem Proving and Its Applications, TPHOLs'95, Lecture Notes in Computer Science, vol.971, pp.214-228

J. V. Katwijk and H. Toetenel, Loose specification of real time systems, Informatica; an international journal of computing and informatics, vol.19, issue.1, pp.25-42

C. Khoury, Définition d'une approche orientée-objet de la spécification algébrique de systémes informatiques

G. Kiczales, J. Riviéres, and D. G. Bobrow, The art of meta-object protocol

C. Kirkwood and M. Thomas, Towards a Symbolic Modal Logic for LOTOS, Northern Formal Methods Workshop NFM'96, eWIC

T. Knapik, Concurrency and real-time specification with many-sorted logic and abstract data types: an example, J. TANKOANO, réd., 2nd African Conference on Research in Computer Science, pp.401-418

S. Kolyang and T. Wolff, A structure preserving encoding of z in isabelle/hol, International Conference on Theorem Proving in Higher Order Logic, vol.1125

P. Kosiuczenko and M. Wirsing, Timed rewriting logic with an application to object-based specification, Science of Computer Programming, vol.28, issue.2-3, pp.225-246

D. Kozen, Results on the Propositional µ-calculus, Theoretical Computer Science, vol.27, pp.333-354

B. Krieg-brückner, J. Peleska, E. Olderog, and A. Baer, The UniForM Workbench, a Universal Development Environment for Formal Methods, Proceedings of the International FM'99, pp.1187-1205

. Bibliographie,

C. Lakos, The Consistent Use of Names and Polymorphism in the Definition of Object Petri Nets, 17th International Conference, vol.1091, pp.380-399, 1996.

T. Lambolais, N. Lévy, and J. Souquières, Assistance au développement de spécifications de protocoles de communication, AFADL'97 Approches Formelles dans l'Assistance au Développement de Logiciel, pp.73-84

L. Lamport, Sometime" is Sometimes "Not Never, 7th Annual ACM Symposium on Principles of Programming Languages, POPL'80, pp.163-173

L. Lamport, Hybrid Systems in TLA+, Hybrid Systems, Lecture Notes in Computer Science

L. Lamport, Introduction to TLA. SRC Technical Note 1994-001, DIGITAL

L. Lamport, The Temporal Logic of Actions, ACM Transactions on Programming Languages and Systems, vol.16, issue.3, pp.872-923

L. Lamport, TLA in Pictures, IEEE Transactions on Software Engineering, vol.21, issue.9, pp.768-775

L. Lamport, The Operators of TLA+. SRC Technical Note 1997-006a, DIGITAL

K. G. Larsen, P. Pettersson, and W. Yi, UPPAAL in a Nutshell. Int. Journal on Software Tools for Technology Transfer, vol.1, issue.1-2, pp.134-152

K. G. Larsen, P. Pettersson, and W. Yi, UPPAAL: Status and developments, Number 1254 in Lecture Notes in Computer Science, pp.456-459

G. J. Leduc, LOTOS, un outil utile ou un autre langage académique ?, Actes des Neuvièmes Journées Francophones sur l'Informatique -Les réseaux de communication -Nouveaux outils et tendances actuelles

F. Lesske, Constructive Specifications of Abstract Data Types Using Temporal Logic, A. NE-RODE et M. A. TAITSLIN, réds., Logical Foundations of Computer Science, LFCS'92, vol.620, pp.269-280

D. Lightfoot, Formal Specification using Z

L. Logrippo, M. Faci, and M. Haj-hussein, An Introduction to LOTOS: Learning by Examples, Computer Networks and ISDN Systems, vol.23, pp.325-342

M. Lutz, Programming Python

M. Magnan and C. Oussalah, Objets et composition, chapter 2, pp.61-92

F. M. , The Argos language: Graphical Representation of Automata and Description of Reactive Systems, IEEE Workshop on Visual Languages

F. Maraninchi, Operational and compositional semantics of synchronous automaton compositions, CONCUR, vol.630

D. A. Marca and M. C. , SADT -Structured Analysis and Design Technique

R. M. , Vérification des propriétés temporelles des programmes parallèles

R. Mateescu and H. Garavel, XTL: A Meta-Language and Tool for Temporal Logic Model-Checking, International Workshop on Software Tools for Technology Transfer STTT'98

S. Matsuoka and A. Yonezawa, Research Directions in Concurrent Object-Oriented Programming, chapter 4: Analysis of inheritance anomaly in object-oriented concurrent programming languages, pp.107-150

S. Mauw and M. A. Reniers, An Algebraic Semantics of Basic Message Sequence Charts, The Computer Journal, vol.37, issue.4, pp.269-277

S. Mauw and G. J. Veltink, An introduction to psf d, Lecture Notes in Computer Science, vol.352

S. Merz-;-f, C. Cassez, O. Jard, B. Roux, and . Rozoy, MO-VEP'98 -MOdélisation et VErification des processus Parallèles, pp.29-44

J. Meseguer-;-g, P. Agha, A. Wegner, and . Yonezawa, A logical theory of concurrent objects and its realization in the maude language, pp.314-390

J. Meseguer, T. Winkler-;-p, D. L. Banatre, and . Metayer, Research Directions in High-Level Parallel Programming Languages, Lecture Notes in Computer Science, vol.574, pp.253-293

J. Meseguer, A Logical Theory of Concurrent Objects, ECOOP/OOPSLA, pp.101-115

J. Meseguer, Conditional rewriting logic as a unified model of concurrency, Theoretical Computer Science, vol.96, issue.1, pp.73-155

J. Meseguer, Rewriting logic as a semantic framework for concurrency: a progress report, CONCUR'96 : Concurrency Theory, vol.1119, pp.331-372

B. Meyer, Object-oriented Software Construction. International Series in Computer Science

R. Milner, J. Parrow, and D. Walker, A calculus of mobile processes. Information and Computation, pp.1-77

R. M. , A Calculus of Communicating Systems, Lecture Notes in Computer Science, vol.92

R. Milner, Communication and Concurrency. International Series in Computer Science

A. Morzenti, D. Mandrioli, and C. Ghezzi, A Model-Parametric Real-Time Logic, ACM TOPLAS-Transactions on Programming Languages and Systems, vol.14, issue.4, pp.521-573

T. Mossakowski and B. Krieg-brückner, Static semantic analysis and theorem proving for CASL, Lecture Notes in Computer Science, vol.1376, pp.333-348

P. D. Mosses and . Casl, A Guided Tour of Its Design, J. FIADEIRO, réd., Recent Trends in Algebraic Development Techniques, Selected Papers of the 13th International Workshop on Algebraic Development Techniques (WADT'98), vol.1589, pp.216-240

L. Mounier, A LOTOS Specification of a "Transit-Node

J. M. Murillo, J. Hernández, F. Sánchez, and L. A. Álvarez, Coordinated Roles: Promoting Re-usability of Coordinated Active Objects Using Event Notification Protocols, P. CIANCARINI et A. L. WOLF, réds., Third International Conference, COORDINATION'99, vol.1594

M. Nesi, Value-passing ccs in hol, réds., 6th Workshop on Higher Order Logic Theorem Proving and Applications, vol.780, pp.352-365

M. Nielsen, V. Sassone, and G. Winskel, Relationships between Models of Concurrency, REX'93 : A Decade of Concurrency, vol.803, pp.425-475

T. Nipkow and L. C. Paulson, Isabelle-91, D. KAPUR, réd., 11th International Conference on Automated Deduction, pp.673-676

S. Owre, S. Rajan, J. Rushby, N. Shankar, and M. Srivas, PVS: Combining specification, proof checking, and model checking, R. ALUR et T. A. HENZINGER, réds., Computer-Aided Verification, CAV '96, number 1102 in Lecture Notes in Computer Science, pp.411-414

S. Owre, J. M. Rushby, and N. Shankar, PVS: A prototype verification system, D. KAPUR, réd., Proceedings of the 11th International Conference on Automated Deduction, pp.748-752

J. Padberg, Recent Trends in Algebraic Development Techniques, Selected Papers of the 13th International Workshop on Algebraic Development Techniques (WADT'98), volume 1589 of Lecture Notes in Computer Science, pp.241-260

M. Papathomas, J. Hernàndez, J. M. Murillo, and F. Sànchez, Inheritance and expressive power in concurrent object-oriented programming, LMO'97 Langages et Modèles à Objets, pp.45-60

B. C. Pierce and D. N. Turner, Theory and Practice of Parallel Programming (TPPP), Lecture Notes in Computer Science, vol.907

A. Podelski, Model checking as constraint solving, J. PALSBERG, réd., SAS'2000: Static Analysis Symposium, vol.1824, pp.221-237

T. P. Lotos, D. Rapport-de-stage-de, and . Informatique,

P. Poizat, Applications de la réécriture de termes aux modèles à objet

P. Poizat, Software Specification Methods: An Overview Using a Case Study, chapter SDL: a Specification and Description Language based on an Extended Finite State Machine Model with Abstract Data Types. Formal Approaches to Computing and Information Technology

?. Springer-verlag,

P. Poizat, C. Choppy, and J. Royer, Concurrency and Data Types: A Specification Method. An Example with LOTOS, Selected Papers of the 13th International Workshop on Algebraic Development Techniques (WADT'98), vol.1589, pp.276-291
URL : https://hal.archives-ouvertes.fr/hal-01135605

P. Poizat, C. Choppy, J. Royer-;-j, J. Wing, J. Woodcock et al., From Informal Requirements to COOP: a Concurrent Automata Approach, FM'99 -Formal Methods, World Congress on Formal Methods in the Development of Computing Systems, vol.1709, pp.939-962
URL : https://hal.archives-ouvertes.fr/hal-01135580

P. Queinnec, M. Filali, G. Padiou, P. Mauran, and P. Papaix, Système de contrôle d'accès. Développement d'une spécification formelle en Unity. Rapport technique 97-33-R

. Raise and . Group, The RAISE Specification Language, BCS Practitioner Series

J. Ramos and A. Sernadas, A Brief Introduction to GNOME, 1096.

J. Rathke and M. Hennessy, Local Model Checking for Value-Passing Processes (Extended Abstract), M. ABADI et T. ITO, réds., Third International Symposium on Theoretical Aspects of Computer Software TACS'97, vol.1281, pp.250-266

G. Reggio, M. Cerioli, and E. Astesiano, An Algebraic Semantics of UML Supporting its Multiview Approach, D. HEYLEN, A. NIJHOLT et G. SCOLLO, réds., Twente Workshop on Language Technology, 2000.

G. Reggio and L. Repetto, CASL-Chart : A Combination of Statecharts and of the Algebraic Specification Language CASL, T. RUS, réd., International Conference on Algebraic Methodology And Software Technology (AMAST'2000), vol.1816, pp.243-257

G. Reggio and R. Wieringa, Thirty one Problems in the Semantics of UML 1.3 Dynamics, OOPSLA'99 workshop "Rigorous Modelling and Analysis of the UML: Challenges and Limitations

G. Reggio, E. Astesiano, and C. Choppy, Casl-ltl: A casl extension for dynamic reactive systems -summary, 2000.

G. Reggio and M. Larosa, A graphic notation for formal specifications of dynamic systems, réds., Formal Methods Europe (FME'97), vol.1313, pp.40-61

W. Reif, The KIV-approach to Software Verification. In M. BROY et S. JAHNICHEN, réds., KORSO: Methods, Languages, and Tools for the Construction of Correct Software -Final Report, vol.1009

W. Reisig, Petri Nets: an Introduction, EATCS Monographs on Theoretical Computer Science

A. W. Roscoe, G. Barett-;-m, A. Main, M. Melton, D. Mislove et al., Unbounded Nondeterminism in CSP, 9th International Conference in Mathematical Foundation of Programming Semantics, vol.442, pp.160-193

A. W. Roscoe, J. C. Woodcock, and L. Wulf, Non-Interference Through Determinism, D. GOLLMANN, réd., Third European Symposium on Research in Computer Security, ESO-RICS'94, vol.875, pp.3-18

J. Rumbaugh, M. Blaha, W. Lorensen, F. Eddy, and W. Premerlani, Object-Oriented Modeling and Design

V. Sassone, M. Nielsen, and G. Winskel, A Classification of Models for Concurrency, Proceedings of Fourth International Conference on Concurrency Theory, CONCUR'93, vol.715, pp.82-96

S. Schneider, An operational semantics for timed CSP. Information and Computation, vol.116, pp.193-213

A. Sernadas, C. Sernadas, and H. Ehrich, Object-Oriented Specification of Databases: An Algebraic Approach, P. M. STOECKER et W. KENT, réds., 1"th International Conference on Very Large Databases VLDB'87, pp.107-116

A. Sernadas, C. Sernadas, and J. F. Costa, Object Specification Logic, Journal of Logic and Computation, vol.5, issue.5, pp.603-630

C. Shankland, M. Thomas, and E. Brinksma, Symbolic Bisimulation for Full LOTOS, Algebraic Methodology and Software Technology (AMAST'97), vol.1349, pp.479-493

M. S. Lotos and . User's-manual,

S. Skidmore, G. Mills, and L. Formen, SSADM Models & Methods, Version 4 -Revised edition

G. Smith, A Fully-Abstract Semantics of Classes for Object, Formal Aspects of Computing, vol.7, pp.30-65

G. Smith, A Semantic Integration of Object-Z and CSP for the Specification of Concurrent Systems, réds., Formal Methods Europe (FME'97), vol.1313, pp.62-81

G. Smolka, The Oz programming model, Lecture Notes in Computer Science, vol.1000, pp.324-343

R. S. , Unified Modeling Language, Version 1.3. Rapport technique, Rational Software Corp

J. Souquières and N. Lévy, PROPLANE: A Specification Development Environment, M. WIRSING et M. NIVAT, réds., International Conference on Algebraic Methodology and Software Technology (AMAST'96), vol.1101, pp.612-615

M. Spivey, The Z Notation: a Reference Manual. Series in Computer Science

C. Stirling, An introduction to modal and temporal logics for ccs, Joint UK/Japan workshop on Concurrency, vol.491, pp.2-20, 1989.

W. J. Stoddart, The Event Calculus, Specification and Modelling of Real Time Systems using Diagrams and Z. Rapport technique

W. J. Stoddart-;-j, M. G. Bowen, D. Hinchey, and . Till, ZUM'97: The Z Formal Specification Notation, Lecture Notes in Computer Science, vol.1212, pp.10-34

W. J. Stoddart, The Event Calculus Extensions for Modelling Hybrid Systems

W. J. Stoddart, The Event Calculus vsn 2. Rapport technique

B. Stroustrup, The C++ Programming Language

K. Taguchi, K. G. Araki-;-m, S. Hinchey, and . Liu, The state-based CCS semantics for concurrent Z specification, Formal Engineering Methods: Proc. 1st International Conference on Formal Engineering Methods (ICFEM'97), pp.12-14

J. Talpin, A. Benveniste, B. Caillaud, C. Jard, Z. Bouziane et al., BDL, a language of distributed reactive objects, The 1st IEEE International Symposium on Object-oriented Real-time Distributed Computing
URL : https://hal.archives-ouvertes.fr/inria-00073336

, The Raise Method GROUP. The RAISE Development Method. The Practitioner Series

H. Treharne and S. Schneider, Using a process algebra to control B OPERATIONS, IFM'99 1st International Conference on Integrated Formal Methods, pp.437-457

K. T. , Relating architecture and specification, Computer Networks and ISDN Systems, vol.29, issue.4, pp.437-456

K. J. Turner, S. Wiley, and . ????, Using Formal Description Techniques, An introduction to Estelle

R. Udink and J. Kok, On the relation between Unity properties and sequences of states, Semantics: Foundations and Applications, vol.666, pp.594-608

C. A. Vissers, G. Scollo, M. Van-sinderen, and E. Brinksma, Specification Styles in Distributed Systems Design and Verification, Theoretical Computer Science, vol.89, issue.1, pp.179-206

R. Wieringa, R. Jungclaus, P. Hartel, G. Saake, and T. Hartmann, OMTROLL -Object Modeling in Troll, U. W. LIPECK et G. KOSCHORREK, réds., International Worskshop on Information Systems -Correctness and Reusability (IS-CORE'93), pp.267-283

G. Winskel, The Formal Semantics of Programming Languages, An Introduction

M. Wirsing, Structured algebraic specifications: A kernel language

M. Wirsing, Algebraic Specification, volume B of Handbook of Theoretical Computer Science, vol.13, pp.675-788

S. Yovine, Kronos: A verification tool for real-time systems, Springer International Journal of Software Tools for Technology Transfer, pp.1-1

Y. Yu, P. Manolios, and L. Lamport, Model Checking TLA+ Specifications, L. PIERRE et T. KROPF, réds., Correct Hardware Design and Verification Methods (CHARME'99), vol.1703, pp.54-66

A. V. Zamulin, Object-Oriented Abstract State Machines, International Workshop on Abstract State Machines, ????

.. .. Tableau-récapitulatif--formalismes-statiques,

, Formalismes utilisés pour les aspects

. .. Tableau-récapitulatif--zccs,

. .. Tableau-récapitulatif--objectz-csp,

. .. Correspondance-entre-offres--lotos,

. .. Tableau-récapitulatif--lotos,

. .. Tableau-récapitulatif--?sz, 28 1.10 Tableau récapitulatif -Machines à configuration

. .. Choix-de-communication,

. Sous-Étapes, . Diagrammes, . .. Korrigan, . Cc, and . .. Oc, 93 3.2 Ensembles C

. .. Correspondance, , p.139

. .. Liste-bornée--casl,

. .. -tla, Cellule, vol.2

. .. Concepts-de-structuration--sdl,

. .. Sémantique-des-signaux--sdl,

, 55 2.3 Buffer non borné -Système de transitions symboliques

. .. Sémantique-de-sender,

.. .. Syntaxe-korrigan-vues, , p.61

.. .. Syntaxe-korrigan-alternative--vues,

, Principe de structuration par vue (Séquence)

. .. Diagramme-de-classes--structuration-interne and . .. ;--vue-statique, 68 2.14 Principe de masquage d'information dans les intégrations de vues

K. .. Syntaxe, 71 2.19 Diagramme de classes -Voitures

K. .. Syntaxe, 72 2.23 Gestionnaire de mots de passe -Intégration des aspects

, Règles

L. Règle,

K. Règle,

A. Règle,

, Gestionnaire de mots de passe -STS global

. .. Approche-orientée-contraintes,

. .. Approche-orientée-États,

.. .. Dépendances,

, Agenda de la description informelle

, Dépendances entre étapes : activité concurrente

, Agenda

, Notation pour les interfaces de communication

, Agenda de la décomposition et de la répartition

K. .. Transitnode-in,

.. .. Controlports--diagramme-de-composition,

.. .. Dataports--diagramme-de-composition,

.. .. Vue,

, Agenda de la composition parallèle

. .. , DataPorts -Diagramme de communication (partiel), p.101

). .. Dataports,

. .. , TransitNode -Diagramme de communication (partiel), p.102

.. .. Patron-client-serveur,

, Agenda des composants séquentiels -Partie 1

, Agenda des composants séquentiels -Partie

(. Inputdataport--diagramme-de-comportement and . .. Sts), , p.111

. .. Ask-architecture,

, Diagramme de classes -CLIS (partie)

, Diagramme de classes -CLAP (partie)

, Principes d'analyse syntaxique basés sur SPARK [29]

. .. , Diagramme de classes -Analyse syntaxique dans ASK (partie), Processus de, vol.122

, Traduction LOTOS -Spécification par simplification pour les éléments de C et CC, p.128

. .. , Traduction SDL -Traduction des offres d'émission/réception, p.131

, Traduction SDL -Traduction des offres ?x:T / ?x:T

.. .. Schéma-de-génération-de-code-orienté-objet, 21 Structuration et contrôleurs pour le noeud de transit

, Exemple de communication en 3 phases

A. .. De, 141 4.24 Classe active pour le DPI (partie)

. .. , Notation textuelle KORRIGAN-Vue (syntaxe alternative), p.181

A. , Notation graphique -simplification des STS (1)

, 10 Notation graphique -simplification des STS (3), A.9

A. , 11 Notation graphique -STS et activités

A. , 12 Notation graphique -Diagrames d'interfaces

A. , 14 Notation graphique -Vues (complète)

A. , 15 Notation graphique -Vues (complète, alternative)

A. , 16 Notation graphique -Vues statiques

A. , 18 Notation graphique -Diagrames de composition

A. ;. , Notation graphique -Diagrames de composition (IV, 1), p.191

A. , Notation graphique -Diagrames de composition (IV, 2)

A. , 21 Notation graphique -Diagrames de communication

A. ;. , 22 Notation graphique -Diagrames de composition (IV, représentation temporaire), p.193

B. , Gestionnaire de mots de passe -Vue Statique

. .. , Gestionnaire de mots de passe -STS dynamique (activités)

, Gestionnaire de mots de passe -Activité de modification de mot de passe

. .. , Gestionnaire de mots de passe -Activité de création de mot de passe

. .. , Gestionnaire de mots de passe -STS dynamique (intégration des activités)

, Gestionnaire de mots de passe -Vue d'intégration

. .. Messagerie--composants,

.. .. Set--vue-statique,

, Utilisateurs de base -Vue dynamique

C. , Utilisateurs de base -STS dynamique

C. , Utilisateurs de base -Vue d'intégration

C. , Utilisateurs complets -Vue d'intégration

C. , Unité de connexion -Vue dynamique

C. , Unité de connexion -STS dynamique

C. , Unité de connexion -Vue d'intégration

C. , Unité de déconnexion -Vue dynamique

C. , Unité de déconnexion -STS dynamique

, Unité de déconnexion -Vue d'intégration

C. , Unité de gestion -STS dynamique

C. , Unité de gestion -Vue d'intégration

C. , Unité de base de données -Vue dynamique

C. , Unité de base de données -STS dynamique

, Unité de base de données -Vue d'intégration

, INDEXED-INDENTIFIER 1.TRANSITION-FORMULA 1, INDEXED-INDENTIFIER 2.TRANSITION-FORMULA 2)

, la notation graphique, il est possible de réunir plus de deux interfaces : si on a (i 1 .a, i 2 .b) et (i 1 .a, i 3 .c) (modulo le fait que la présence de (x, y) dans ? est équivalent à celle de (y, x)), il est possible de créer un lien unique correspondant à

, avant la décomposition finale des composants en aspect statique et aspect dynamique), les ESV sont représentées de façon temporaire avec une forme textuelle de leur partie statique (ESV et partie dynamique des composants l'ESV sont alors confondues). La figure A.22 montre cette notation (un exemple en est la figure 3, Il faut remarquer que, dans les première étapes de décomposition de la méthode (i.e, vol.13

A. Figure, 22 : Notation graphique -Diagrames de composition (IV

, En fait, la notation finale (après toutes les étapes de décomposition, y compris celle correspondant à la séparation des aspects)

, Description de l'étude de cas

, Les utilisateurs de base peuvent modifier leur mot de passe. L'utilisateur privilégié peut agir comme un utilisateur de base (et changer son mot de passe), mais peut aussi créer des comptes utilisateurs (i.e. ajouter un identifiant d'utilisateur et un mot de passe lui correspondant). La création d'un compte utilisateur se passe comme suit : 1. l'identifiant de l'utilisateur est demandé puis (a) soit il existe déjà

, (b) soit il n'existe pas, et le mot de passe est demandé

, est survenue, le mot de passe est demandé à nouveau puis (a) soit il est différent du mot de passe précédemment entré, et une erreur est signalée

, (b) soit il est identique

, La modification d'un mot de passe par un utilisateur se passe comme pour la création, mis à part les deux différences suivantes : -l'identifiant de l'utilisateur doit déjà exister

, ancien mot de passe est démandé (et vérifié) avant la partie concernant la saisie du nouveau mot de passe

, Il est possible de modéliser des systèmes plus complexes, avec par exemple des restrictions concernant le mot de passe. Nous verrons plus bas

, Spécification du gestionnaire de mots de passe Nous donnons ici la spécification complète, en KORRIGAN

, La vue statique du gestionnaire de mots de passe en KORRIGAN est donnée dans la figure B.1. Nous avons fait ici le choix de la définir "from scratch

, 2. modifier les transitions de la partie dynamique du gestionnaire (dans les deux activités) et rajouter une garde à chaque réception de mot de passe pour imposer le respect des restrictions : la transition

, Il peut, lorsqu'il n'est pas en communication, demander au serveur de devenir abonné

, Il peut être appelé par le serveur lorsqu'un appelant abonné en fait la demande

, Il peut refuser de prendre une communication

, Il peut accepter une communication en provenance d'un appelant abonné

, Un client abonné a les mêmes droits qu'un client simple

, Il peut, lorsqu'il n'est pas en cours ou en demande de communication, demander au serveur d'annuler son abonnement

, Il peut demander au serveur d'enregistrer un nouveau client comme l'un de ses appelés potentiels

, Il peut demander au serveur de supprimer un client de la liste de ses appelés potentiels

, Il peut demander au serveur une communication avec un autre client

, Le serveur central est composé de quatre unités : une unité de connexion, une unité de gestion

, Elle s'occupe des demandes de connexion

, Elle envoie une requête à l'appelé pour lui signaler qu'une demande de connexion a été faite

, Elle établit la connexion entre l'appelant et l'appelé

, Unité de gestion

, Elle gère toutes les demandes de changement de statut (client simple / client abonné)

, Elle gère les demandes de mise à jour de la liste des appelés potentiels des clients abonnés

, Unité de déconnexion

, Elle s'occupe des demandes de déconnexion

, Elle peut décider d'elle-même d'interrompre une connexion

, Unité de base de données

, La base de données contient l'ensemble des numéros d'abonnés, et pour chaque abonné l'ensemble des numéros de ses appelés potentiels

, Elle prend en compte les changements de statut des clients, et toute modification éventuelle des listes d'appelés potentiels

, Elle dispose d'informations sur les communications en cours, l'appelant et l'appelé

, Une communication entre un appelant i et un appelé j est possible quand

L. ,

, Ici nous définissons d'abord quelques spécifications de base (usuelles). Ensuite, nous spécifions les utilisateurs de la messagerie : d'abord le comportement de clients de base (i.e. clients simples sans possibilité d'abonnement), puis le comportement de clients complets (simples, abonnés) en utilisant le principe d'héritage de KORRIGAN. Enfin, nous spécifions chacune des unités du serveur central, Spécification de la messagerie Nous donnons dans cette annexe la spécification KORRIGAN complète de la messagerie