, Xfig version 3.2 user manual
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 ,
, Conjoining Specifications. ACM Toplas, vol.17, issue.3, pp.507-534
The B Book -Assigning Programs to Meanings ,
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
Verification of properties involving logical and physical timing features, Génie Logiciel & Ingénierie de Systèmes & leurs Applications, ICSSEA'2000 ,
International Workshop on Comparing Systems Specification Techniques -What questions are prompted by ones particular method of specification? ,
ActiveJava, un modelo de programación concurrente orientado a objeto, III Jornadas de Ingenería del Software ,
Process algebra with probabilistic choice, Lecture Notes in Computer Science, vol.1601, pp.111-129 ,
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 ,
, Méthodes formelles et à objets pour le développement du logiciel : Etudes et propositions
Spécification de l'atelier ASFO ,
The formal class model, Joint Modular Languages Conference, pp.59-78 ,
How To Easily Extract an Abstract Data Type From a Dynamic Description, Research Report, vol.159 ,
An Algebraic Approach to Heterogeneous Software Systems ,
Etude sur l'application de méthodes formelles à la compilation et à la validation de programmes Electre ,
Systèmes de transitions finis et sémantique des processus communicants. Etudes et recherches en informatique ,
Formalism and method, M. BIDOIT et M. DAUCHET, réds., TAPSOFT'97, vol.1214, pp.93-114 ,
UML as heterogeneous multiview notation. strategies for a formal foundation, Proceedings of the OOPSLA'98 Workshop on Formalizing UML. Why? How?, ???? ,
Algebraic Foundations of System Specification, chapter Algebraic Specification of Concurrent Systems ,
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 ,
Algebraic Specification of Concurrency, M. BIDOIT et C. CHOPPY, réds., Recent Trends in Data Type Specification, vol.655, pp.1-39 ,
Labelled Transition Logic: An Outline ,
, 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
D-oids: a model for dynamic data-types, Mathematical Structures in Computer Science, vol.5, issue.2, pp.257-282 ,
Configuration Machines: A Simple Formalism for Specifying Multifaceted Systems ,
Génération de code Promela pour la simulation et la vérification, International Conference on Software and Systems Engineering and their Applications, ICSSEA, ???? ,
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, ???? ,
Compiling Little Languages in Python, 7th International Python Conference ,
The Coq Proof Assistant Reference Manual: Version 6.2.4. Rapport technique, INRIA, ???? ,
URL : https://hal.archives-ouvertes.fr/inria-00069968
Process Algebra in PVS, R. CLEAVELAND, réd., Tools and Algorithms for Construction and Analysis of Systems (TACAS), vol.1579, pp.270-284 ,
Cooperative Objects : a Concurrent Petri Net Based Object-Oriented Language, IEEE / System Man and Cybernetics 93 ,
Approaches in unifying Petri nets and the Object-Oriented Approach, 1st Workshop on Object-Oriented Programming and Models of Concurrency ,
Inheritance and Concurrency in CLOWN, 1st Workshop on Object-Oriented Programming and Models of Concurrency ,
Modular Algebraic Nets to Specify Concurrent Systems, IEEE Transactions on Software Engineering, vol.22, issue.10, pp.689-705 ,
SWIG : An Easy to Use Tool For Integrating Scripting Languages with C and C++, 4th Annual USENIX Tcl/Tk Workshop, pp.287-294 ,
Algebraic Specification ,
of CWI Monograph, chapter Process algebra: Specification and verification in bisimulation semantics, KLOP. Math. & Comp. Sci, vol.II ,
The ESTEREL synchronous programming language : design, semantics, implementation, Inria ,
URL : https://hal.archives-ouvertes.fr/inria-00075711
Workshop on Object-Oriented Programming and Models of Concurrency'95, pp.131-145 ,
Advances in Petri Nets on Object-Orientation, Lecture Notes in Computer Science ,
CO-OPN/2: A Concurrent Object-Oriented Formalism, Second IFIP Conf. on Formal Methods for Open Object-Based Distributed Systems (FMOODS), pp.57-72 ,
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 ,
Types abstraits algébriques : spécifications structurées et présentations gracieuses, Colloque AFCET, Les mathématiques de l'informatique, pp.347-357 ,
Verifying and Validating Software Requirements and Design Specifications, IEEE Software, vol.1, issue.1, pp.75-88 ,
Viewpoint consistency in Z and LOTOS: A case study, FME'97, Formal Methods: Their Industrial Application and Strengthened Foundations ,
Introduction to the ISO Specification Language LOTOS. Computer Networks and ISDN Systems, vol.14, pp.25-29 ,
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
Experience with embedding hardware description language in hol, International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, pp.129-156 ,
A Mathematical Definition of Full Prolog, Science of Computer Programming, vol.24, issue.3, pp.249-286 ,
Programmer Friendly Modular Definition of the Semantics of Java, Lecture Notes in Computer Science, vol.1523, pp.353-404 ,
, Objets pour la programmation parallèle et répartie : intérêts, évolutions et tendances. Technique et science informatiques, vol.15, pp.765-800
A Theory of Communicating Sequential Processes, Journal of the ACM, vol.31, issue.3, pp.560-599 ,
Specification and top down design of distributed systems, Lecture Notes in Computer Science, vol.185, pp.4-28 ,
The Requirement and Design Specification Language SPECTRUM. Rapport technique TUM-I9140 ,
Algebraic State Machines, T. RUS, réd., International Conference on Algebraic Methodology And Software Technology (AMAST'2000), vol.1816, pp.89-118 ,
Distributed Systems Analysis with CCS. International Series in Computer Science ,
Representing Dynamic Aspects of a Concurrent OO Formalism by Mobile Nets, 11th European Conference on Object-Oriented Programming (ECOOP'97) ,
The µSZ Notation Version 1.0, vol.13 ,
Integrating Z with Dynamic Modeling Techniques for the Specification of Reactive Systems ,
, The Definition of Dynamic Z. ESPRESS Projektbericht
csp2B: A practical approach to combining CSP and B, réds., FM'99-Formal Methods, vol.I, pp.490-508 ,
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 ,
Formal Specification and Verification of Object-Based Systems in a Temporal Logic Setting ,
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, ????
Parallel Program Design: A Fundation ,
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. ,
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
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
Specification of Mixed Systems in KORRIGAN with the Support of an UML-Inspired Graphical Notation, Fundamental Approaches to Software Engineering (FASE'2001) ,
, Journal of Universal Computer Science, ????. Special issue: Tools for System Design and Verification, pp.948-6968
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 ,
Using LOTOS in the Object-Based Development of Embedded Systems, pp.307-319 ,
Verification tools for finite-state concurrent systems, A Decade of concurrency -Reflections and Perspectives, vol.803 ,
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 ,
, , vol.79
, The Common Framework Initiative for Algebraic specification and development, electronic archives. Notes and Documents accessible by WWW 1 and FTP 2 , ????
CASL -The CoFI Algebraic Specification Language -Summary (version 1.0). Documents/CASL/Summary ,
The CoFI-Reactive Systems Group Home Page . ReactiveSys-temsTaskGroup.html ,
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 ,
JTN: A Java-Targeted Graphic Formal Notation for Reactive and Concurrent Systems, Fundamental Approaches to Software Engineering (FASE'99), vol.1577, pp.77-97 ,
Specification of abstract dynamic data types: A temporal logic approach, Theoretical Computer Science, vol.73, issue.2 ,
Algebraic Specifications with Implicit State, Working papers of the international Workshop on Information System Correctness and Reusability, IS-CORE'93, ???? ,
A brief history of Timed CSP, Theoretical Computer Science, vol.138, issue.2, pp.243-271 ,
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 ,
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 ,
TROLL -An Object Oriented Formal Method for Distributed Information System Design: Syntax and Pragmatics ,
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 ,
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 ,
Weak refinement in Z, Lecture Notes in Computer Science, vol.1212, p.369 ,
Comparing LOTOS and Z refinement relations, FORTE/PSTV'96, pp.501-516 ,
Rewrite Systems, volume B of Handbook of Theoretical Computer Science, pp.243-320 ,
CafeOBJ Report -The Language, Proof Techniques, and Methodologies for Object-Oriented Algebraic Specification, AMAST Series in Computing. World Scientific, vol.6 ,
Rigorous Object-Oriented Analysis ,
Object-Z: A specification language advocated for the description of standards, Computer Standards and Interfaces, vol.17, pp.511-533 ,
Logics for Databases and Information Systems, chapter Logics for Specifying Concurrent Information Systems, pp.167-198 ,
Constructing Systems as Object Communities, Theory and Practice of Software Development (TAPSOFT'93), vol.668, pp.453-467 ,
Fundamentals of Algebraic Specification, vol.1 ,
integration paradigm for data type and process specification techniques". Bulletin of EATCS -Formal Specification Column ,
Horizontal and vertical structuring techniques for statecharts, CONCUR'97 : Concurrency Theory, vol.1243, pp.181-195 ,
Integration and Classification of Data Type and Process Specification Techniques ,
, Tutorial on Message Sequence Charts. Computer Networks and ISDN Systems, vol.28, pp.1629-1641
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) ,
SDL : Formal Object-oriented Language for Communicating Systems ,
Mechanical Verification of Concurrent Systems with TLA, Fourth International Workshop on Computer-Aided Verification, CAV'92 ,
Implementation and behavioural equivalence: a survey, Lecture Notes in Computer Science, vol.655, pp.93-125 ,
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
ALDEBARAN : un système de vérification par réduction de processus communicants ,
CADP: A Protocol Validation and Verification Toolbox, 8th Conference on Computer-Aided Verification, pp.437-440 ,
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 ,
Propriétés de la composition/décomposition de réseaux de Petri et de leurs graphes de couverture, vol.28, pp.73-124 ,
Combining csp and z. Rapport technique TRCF-97-1 ,
, Proc. 2nd IFIP Workshop on Formal Methods for Open Object-Based Distributed Systems (FMOODS), pp.423-438
How to Combine Z with a Process Algebra, Lecture Notes in Computer Science, vol.1493, pp.5-23 ,
A temporal calculus of communicating systems (tccs), CONCUR-90: Theories of Concurrency, vol.458, pp.401-415 ,
The reflexive chemical abstract machine and the join-calculus, Proceedings of the 23rd ACM Symposium on Principles of Programming Languages, pp.21-24 ,
A calculus of mobile agents, 7th International Conference on Concurrency Theory (CONCUR'96), pp.26-29 ,
UML'99 -The Unified Modelling Language, Lecture Notes in Computer Science, vol.1723 ,
, FUCHS. Specifications are (Preferably) Executable. Software Engineering Journal, vol.7, issue.5, pp.323-334
Principles of OBJ2, Conference Record of the Twelfth Annual ACM Symposium on Principles of Programming Languages, pp.52-66 ,
An operationnal semantics for zccs, réds., International Conference of Formal Engineering Methods (IFCEM) ,
Integrated Formal Methods with Richer Methodological Profiles for the Development of Multi-Perspective Systems ,
Compilation et vérification de programmes LOTOS ,
Introduction au langage LOTOS. Rapport technique, VERILOG, Centre d'Etudes, Forum du Pré Milliet ,
An example of LOTOS Specification : The Matrix Switch Problem, Rapport SPECTRE C22, Laboratoire de Génie Informatique -Institut IMAG ,
An overview of LP, the Larch Prover, Proc. of the Third International Conference on Rewriting Techniques and Applications, vol.355, pp.137-151 ,
A first introduction to PLUSS ,
An introduction to OBJ-3, Proceedings 1st International Workshop on Conditional Term Rewriting Systems, vol.308, pp.88-89 ,
Introduction to HOL: A theorem proving environment for higher order logic ,
The Java Language Specification ,
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 ,
Specifying Embedded Systems with Statecharts and Z: An Agenda for Cyclic Software Components, E. ASTESIANO, réd., FASE'98, vol.1382, pp.88-106 ,
Comparison of object-oriented formal methods. Technical report of the esprit long term research project 20072 "design for validation ,
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
Les langages concurrents à objets, Technique et science informatiques, vol.14, issue.8, pp.945-971 ,
draft of the asm guide, 1997. ,
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 ,
MOVEP'98 -MOdélisation et VErification des processus Parallèles, pp.1-7 ,
On Visual Formalisms, Communications of the ACM, vol.31, issue.5, pp.514-530 ,
STATEMATE: A Working Environment for the Development of Complex Reactive Systems, IEEE Transactions on Software Engineering, vol.16, issue.3, pp.403-414 ,
The statemate semantics of statecharts, ACM Transactions on Software Engineering and Methodology, vol.5, issue.4, pp.293-333 ,
, Specifications are not Necessary Executable. Software Engineering Journal, vol.4, issue.6, pp.330-338
Agendas -A Concept to Guide Software Development Activities, pp.19-32, 2000. ,
Using LOTOS Patterns to Characterize Architectural Styles, M. BI-DOIT et M. DAUCHET, réds., TAPSOFT'97, vol.1214, pp.818-832 ,
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 ,
Methodological Support for Formally Specifying Safety-Critical Software, 16th International Conference on Computer Safety, Reliability and Security, pp.295-308 ,
, Symbolic Bisimulations. Theoretical Computer Science, vol.138, issue.2, pp.353-389
Extending the UML with a Multicast Synchronisation, Proceedings of the third Rigorous Object-Oriented Methods Workshop (ROOM), pp.1-902505 ,
Proof of Correctness of Data Representations, Acta Informatica, vol.1, pp.271-281 ,
Communicating Sequential Processes, Communications of the ACM, vol.21, issue.8, pp.666-677 ,
The Spin Model Checker, IEEE Transactions on Software Engineering, vol.23, issue.5, pp.279-295 ,
A Formal Description Technique based on an Extended State Transition Model. ISO/IEC 9074, International Organization for Standardization ,
A Formal Description Technique based on the Temporal Ordering of Observational Behaviour. ISO/IEC 8807, International Organization for Standardization ,
, Message Sequence Chart (MSC), vol.120
A Consensus Glossary of Temporal Database Concepts, SIGMOD Record (ACM Special Interest Group on Management of Data), vol.23, issue.1, pp.52-64 ,
Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use. Monographs in Theoretical Computer Science ,
Systematic Software Development Using VDM ,
A modular state/transition approach for programming realtime systems, ACM Sigplan Workshop on Language, compiler and tool support for real-time systems ,
DisCo specification language: marriage of actions and objects, 11th International Conference on Distributed Computing Systems, pp.142-151 ,
Higher Order Logic Theorem Proving and Its Applications, TPHOLs'95, Lecture Notes in Computer Science, vol.971, pp.214-228 ,
Loose specification of real time systems, Informatica; an international journal of computing and informatics, vol.19, issue.1, pp.25-42 ,
Définition d'une approche orientée-objet de la spécification algébrique de systémes informatiques ,
The art of meta-object protocol ,
Towards a Symbolic Modal Logic for LOTOS, Northern Formal Methods Workshop NFM'96, eWIC ,
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 ,
A structure preserving encoding of z in isabelle/hol, International Conference on Theorem Proving in Higher Order Logic, vol.1125 ,
Timed rewriting logic with an application to object-based specification, Science of Computer Programming, vol.28, issue.2-3, pp.225-246 ,
Results on the Propositional µ-calculus, Theoretical Computer Science, vol.27, pp.333-354 ,
The UniForM Workbench, a Universal Development Environment for Formal Methods, Proceedings of the International FM'99, pp.1187-1205 ,
,
The Consistent Use of Names and Polymorphism in the Definition of Object Petri Nets, 17th International Conference, vol.1091, pp.380-399, 1996. ,
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 ,
Sometime" is Sometimes "Not Never, 7th Annual ACM Symposium on Principles of Programming Languages, POPL'80, pp.163-173 ,
Hybrid Systems in TLA+, Hybrid Systems, Lecture Notes in Computer Science ,
Introduction to TLA. SRC Technical Note 1994-001, DIGITAL ,
The Temporal Logic of Actions, ACM Transactions on Programming Languages and Systems, vol.16, issue.3, pp.872-923 ,
TLA in Pictures, IEEE Transactions on Software Engineering, vol.21, issue.9, pp.768-775 ,
The Operators of TLA+. SRC Technical Note 1997-006a, DIGITAL ,
, UPPAAL in a Nutshell. Int. Journal on Software Tools for Technology Transfer, vol.1, issue.1-2, pp.134-152
UPPAAL: Status and developments, Number 1254 in Lecture Notes in Computer Science, pp.456-459 ,
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 ,
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 ,
Formal Specification using Z ,
An Introduction to LOTOS: Learning by Examples, Computer Networks and ISDN Systems, vol.23, pp.325-342 ,
Programming Python ,
Objets et composition, chapter 2, pp.61-92 ,
The Argos language: Graphical Representation of Automata and Description of Reactive Systems, IEEE Workshop on Visual Languages ,
Operational and compositional semantics of synchronous automaton compositions, CONCUR, vol.630 ,
SADT -Structured Analysis and Design Technique ,
Vérification des propriétés temporelles des programmes parallèles ,
XTL: A Meta-Language and Tool for Temporal Logic Model-Checking, International Workshop on Software Tools for Technology Transfer STTT'98 ,
Research Directions in Concurrent Object-Oriented Programming, chapter 4: Analysis of inheritance anomaly in object-oriented concurrent programming languages, pp.107-150 ,
An Algebraic Semantics of Basic Message Sequence Charts, The Computer Journal, vol.37, issue.4, pp.269-277 ,
An introduction to psf d, Lecture Notes in Computer Science, vol.352 ,
MO-VEP'98 -MOdélisation et VErification des processus Parallèles, pp.29-44 ,
A logical theory of concurrent objects and its realization in the maude language, pp.314-390 ,
Research Directions in High-Level Parallel Programming Languages, Lecture Notes in Computer Science, vol.574, pp.253-293 ,
A Logical Theory of Concurrent Objects, ECOOP/OOPSLA, pp.101-115 ,
Conditional rewriting logic as a unified model of concurrency, Theoretical Computer Science, vol.96, issue.1, pp.73-155 ,
Rewriting logic as a semantic framework for concurrency: a progress report, CONCUR'96 : Concurrency Theory, vol.1119, pp.331-372 ,
Object-oriented Software Construction. International Series in Computer Science ,
A calculus of mobile processes. Information and Computation, pp.1-77 ,
A Calculus of Communicating Systems, Lecture Notes in Computer Science, vol.92 ,
Communication and Concurrency. International Series in Computer Science ,
A Model-Parametric Real-Time Logic, ACM TOPLAS-Transactions on Programming Languages and Systems, vol.14, issue.4, pp.521-573 ,
Static semantic analysis and theorem proving for CASL, Lecture Notes in Computer Science, vol.1376, pp.333-348 ,
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 ,
A LOTOS Specification of a "Transit-Node ,
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 ,
Value-passing ccs in hol, réds., 6th Workshop on Higher Order Logic Theorem Proving and Applications, vol.780, pp.352-365 ,
Relationships between Models of Concurrency, REX'93 : A Decade of Concurrency, vol.803, pp.425-475 ,
Isabelle-91, D. KAPUR, réd., 11th International Conference on Automated Deduction, pp.673-676 ,
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 ,
PVS: A prototype verification system, D. KAPUR, réd., Proceedings of the 11th International Conference on Automated Deduction, pp.748-752 ,
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 ,
Inheritance and expressive power in concurrent object-oriented programming, LMO'97 Langages et Modèles à Objets, pp.45-60 ,
Theory and Practice of Parallel Programming (TPPP), Lecture Notes in Computer Science, vol.907 ,
Model checking as constraint solving, J. PALSBERG, réd., SAS'2000: Static Analysis Symposium, vol.1824, pp.221-237 ,
,
Applications de la réécriture de termes aux modèles à objet ,
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 ,
,
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
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
Système de contrôle d'accès. Développement d'une spécification formelle en Unity. Rapport technique 97-33-R ,
The RAISE Specification Language, BCS Practitioner Series ,
A Brief Introduction to GNOME, 1096. ,
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 ,
An Algebraic Semantics of UML Supporting its Multiview Approach, D. HEYLEN, A. NIJHOLT et G. SCOLLO, réds., Twente Workshop on Language Technology, 2000. ,
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 ,
Thirty one Problems in the Semantics of UML 1.3 Dynamics, OOPSLA'99 workshop "Rigorous Modelling and Analysis of the UML: Challenges and Limitations ,
Casl-ltl: A casl extension for dynamic reactive systems -summary, 2000. ,
A graphic notation for formal specifications of dynamic systems, réds., Formal Methods Europe (FME'97), vol.1313, pp.40-61 ,
, 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
Petri Nets: an Introduction, EATCS Monographs on Theoretical Computer Science ,
Unbounded Nondeterminism in CSP, 9th International Conference in Mathematical Foundation of Programming Semantics, vol.442, pp.160-193 ,
Non-Interference Through Determinism, D. GOLLMANN, réd., Third European Symposium on Research in Computer Security, ESO-RICS'94, vol.875, pp.3-18 ,
Object-Oriented Modeling and Design ,
A Classification of Models for Concurrency, Proceedings of Fourth International Conference on Concurrency Theory, CONCUR'93, vol.715, pp.82-96 ,
An operational semantics for timed CSP. Information and Computation, vol.116, pp.193-213 ,
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 ,
Object Specification Logic, Journal of Logic and Computation, vol.5, issue.5, pp.603-630 ,
Symbolic Bisimulation for Full LOTOS, Algebraic Methodology and Software Technology (AMAST'97), vol.1349, pp.479-493 ,
,
SSADM Models & Methods, Version 4 -Revised edition ,
A Fully-Abstract Semantics of Classes for Object, Formal Aspects of Computing, vol.7, pp.30-65 ,
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 ,
The Oz programming model, Lecture Notes in Computer Science, vol.1000, pp.324-343 ,
Unified Modeling Language, Version 1.3. Rapport technique, Rational Software Corp ,
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 ,
The Z Notation: a Reference Manual. Series in Computer Science ,
An introduction to modal and temporal logics for ccs, Joint UK/Japan workshop on Concurrency, vol.491, pp.2-20, 1989. ,
The Event Calculus, Specification and Modelling of Real Time Systems using Diagrams and Z. Rapport technique ,
ZUM'97: The Z Formal Specification Notation, Lecture Notes in Computer Science, vol.1212, pp.10-34 ,
The Event Calculus Extensions for Modelling Hybrid Systems ,
The Event Calculus vsn 2. Rapport technique ,
The C++ Programming Language ,
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 ,
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
Using a process algebra to control B OPERATIONS, IFM'99 1st International Conference on Integrated Formal Methods, pp.437-457 ,
Relating architecture and specification, Computer Networks and ISDN Systems, vol.29, issue.4, pp.437-456 ,
Using Formal Description Techniques, An introduction to Estelle ,
On the relation between Unity properties and sequences of states, Semantics: Foundations and Applications, vol.666, pp.594-608 ,
Specification Styles in Distributed Systems Design and Verification, Theoretical Computer Science, vol.89, issue.1, pp.179-206 ,
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 ,
The Formal Semantics of Programming Languages, An Introduction ,
Structured algebraic specifications: A kernel language ,
Algebraic Specification, volume B of Handbook of Theoretical Computer Science, vol.13, pp.675-788 ,
Kronos: A verification tool for real-time systems, Springer International Journal of Software Tools for Technology Transfer, pp.1-1 ,
Model Checking TLA+ Specifications, L. PIERRE et T. KROPF, réds., Correct Hardware Design and Verification Methods (CHARME'99), vol.1703, pp.54-66 ,
Object-Oriented Abstract State Machines, International Workshop on Abstract State Machines, ???? ,
,
, Formalismes utilisés pour les aspects
,
,
,
,
28 1.10 Tableau récapitulatif -Machines à configuration ,
,
93 3.2 Ensembles C ,
, , p.139
,
, Cellule, vol.2
,
,
, 55 2.3 Buffer non borné -Système de transitions symboliques
,
, , p.61
,
, Principe de structuration par vue (Séquence)
68 2.14 Principe de masquage d'information dans les intégrations de vues ,
71 2.19 Diagramme de classes -Voitures ,
72 2.23 Gestionnaire de mots de passe -Intégration des aspects ,
, Règles
,
,
,
, Gestionnaire de mots de passe -STS global
,
,
,
, 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
,
,
,
,
, Agenda de la composition parallèle
DataPorts -Diagramme de communication (partiel), p.101 ,
,
TransitNode -Diagramme de communication (partiel), p.102 ,
,
, Agenda des composants séquentiels -Partie 1
, Agenda des composants séquentiels -Partie
, , p.111
,
, 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
21 Structuration et contrôleurs pour le noeud de transit ,
, Exemple de communication en 3 phases
141 4.24 Classe active pour le DPI (partie) ,
Notation textuelle KORRIGAN-Vue (syntaxe alternative), p.181 ,
Notation graphique -simplification des STS (1) ,
, 10 Notation graphique -simplification des STS (3), A.9
11 Notation graphique -STS et activités ,
12 Notation graphique -Diagrames d'interfaces ,
14 Notation graphique -Vues (complète) ,
15 Notation graphique -Vues (complète, alternative) ,
16 Notation graphique -Vues statiques ,
18 Notation graphique -Diagrames de composition ,
Notation graphique -Diagrames de composition (IV, 1), p.191 ,
Notation graphique -Diagrames de composition (IV, 2) ,
21 Notation graphique -Diagrames de communication ,
22 Notation graphique -Diagrames de composition (IV, représentation temporaire), p.193 ,
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
,
,
, Utilisateurs de base -Vue dynamique
Utilisateurs de base -STS dynamique ,
Utilisateurs de base -Vue d'intégration ,
Utilisateurs complets -Vue d'intégration ,
Unité de connexion -Vue dynamique ,
Unité de connexion -STS dynamique ,
Unité de connexion -Vue d'intégration ,
Unité de déconnexion -Vue dynamique ,
Unité de déconnexion -STS dynamique ,
, Unité de déconnexion -Vue d'intégration
Unité de gestion -STS dynamique ,
Unité de gestion -Vue d'intégration ,
Unité de base de données -Vue dynamique ,
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
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
,
, 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