M. Abadi and L. Lamport, Composing specifications, ACM Transactions on Programming Languages and Systems, vol.15, issue.1, pp.73-132, 1993.
DOI : 10.1145/151646.151649
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.33.1637

M. Abadi and L. Lamport, Conjoining specifications, ACM Transactions on Programming Languages and Systems, vol.17, issue.3, pp.507-534, 1995.
DOI : 10.1145/203095.201069
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.33.4928

S. Aggarwal, C. Courcoubetis, and P. Wolper, Adding liveness properties to coupled finite-state machines, ACM Transactions on Programming Languages and Systems, vol.12, issue.2, pp.303-339, 1990.
DOI : 10.1145/78942.78948

P. Alexander, A practical semantics for design facet interaction, Proceedings. Eighth Annual IEEE International Conference and Workshop On the Engineering of Computer Based Systems-ECBS 2001, 2000.
DOI : 10.1109/ECBS.2001.922427

R. Allen and D. Garlan, Formalizing architectural connection, Proceedings of 16th International Conference on Software Engineering, pp.71-80, 1994.
DOI : 10.1109/ICSE.1994.296767

R. Allen and D. Garlan, A formal basis for architectural connection, ACM Transactions on Software Engineering and Methodology, vol.6, issue.3, pp.213-249, 1997.
DOI : 10.1145/258077.258078
URL : https://hal.archives-ouvertes.fr/hal-00444067

R. Allen and D. Garlan, Errata: a formal basis for architectural connection, ACM Transactions on Software Engineering and Methodology, vol.7, issue.3, pp.333-334, 1998.
DOI : 10.1145/287000.287031

A. Board and O. , Model Driven Architecture (MDA) [Online] Document number ormsc/01-07-01 Available at http://www.omg. org/cgi-bin/doc?, 2001.

. Aster-project, Aster project's Home Page, Solidor group

. Automated-reasoning-system and . Itc-irst, NuSMV: a new symbolic model checker, 2001.

S. Bensalem, Y. Lakhnech, and S. Owre, Computing abstractions of infinite state systems compositionally and automatically, pp.319-331
DOI : 10.1007/BFb0028755

S. Bensalem, Y. Lakhnech, and S. Owre, InVeSt : A tool for the verification of invariants, pp.505-510
DOI : 10.1007/BFb0028771

J. Bentley, D. E. Knuth, and M. D. Mcilroy, Programming pearls, Communications of the ACM, vol.29, issue.6, pp.471-483, 1986.
DOI : 10.1145/5948.315654

L. Bergmans and M. Aksits, Composing crosscutting concerns using composition filters, Communications of the ACM, vol.44, issue.10, pp.51-57, 2001.
DOI : 10.1145/383845.383857

P. Besnard and A. Hunter, Quasi-classical logic: Non-trivializable classical reasoning from inconsistent information, Proceedings of the EC- SQARU European Conference on Symbolic and Quantitive Approaches to Reasoning and Uncertainty, pp.44-51, 1995.
DOI : 10.1007/3-540-60112-0_6

N. Bjørner, A. Browne, M. A. Colón, B. Finkbeiner, Z. Manna et al., Verifying Temporal Properties of Reactive Systems: A STeP Tutorial. Formal Methods in System Design, pp.227-270, 2000.

D. Blostein and A. Schürr, Computing with Graphs and Graph Transformations . Software ? Practice and Experience, pp.197-217, 1999.

J. Bowen and V. Stavridou, Safety-critical systems, formal methods and standards, Software Engineering Journal, vol.8, issue.4, pp.189-209, 1993.
DOI : 10.1049/sej.1993.0025

A. W. Brown and K. C. Wallnau, The current state of CBSE, IEEE Software, vol.15, issue.5, pp.37-46, 1998.
DOI : 10.1109/52.714622

A. Browne, H. Sipma, and T. Zhang, Linking STeP with SPIN, SPIN-7, pp.181-186

R. E. Bryant, Symbolic Manipulation of Boolean Functions Using a Graphical Representation, Proceedings of the 22nd ACM/IEEE Design Automation Conference, pp.688-694, 1985.

R. E. Bryant, Binary decision diagrams and beyond: enabling technologies for formal verification, Proceedings of IEEE International Conference on Computer Aided Design (ICCAD), pp.236-245, 1995.
DOI : 10.1109/ICCAD.1995.480018

M. Büchi and W. Weck, A Plea for Grey-Box Components, Proceedings of the First Workshop on the Foundations of Component-Based Systems, pp.39-49, 1997.

A. Cimatti, E. Clarke, F. Giunchiglia, and M. Roveri, NuSMV: A New Symbolic Model Verifier, Proc. 11th International Computer Aided Verification Conference, pp.495-499, 1999.
DOI : 10.1007/3-540-48683-6_44

E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith, Counterexample-Guided Abstraction Refinement, pp.154-169

E. M. Clarke and J. , Orna Grumberg, and Doron A. Peled. Model Checking, 2000.

C. Paul and . Clements, From Subroutines to Subsystems: Component- Based Software Development

Y. Coady, G. Kiczales, M. Feeley, N. Hutchinson, and J. Ong, Structuring operating system aspects: using AOP to improve OS structure modularity, Communications of the ACM, vol.44, issue.10, pp.79-82, 2001.
DOI : 10.1145/383845.383863

A. Michael, T. E. Colón, and . Uribe, Generating Finite-State Abstractions of Reactive Systems Using Decision Procedures, pp.293-304

R. Gregory and . Crane, The Perseus Project, 2001.

S. J. Creese and A. W. Roscoe, Verifying an infinite family of inductions simultaneously using data independence and FDR Also available from the Concurrency Research Group's publication web page

D. Dams, R. Gerth, S. Leue, and M. Massink, Theoretical and Practical Aspects of SPIN Model Checking -5th and 6th International SPIN Workshops, Lecture Notes in Computer Science, vol.1680, 1999.

. Springer-verlag, Also available from http

D. Dennis-rené, Abstract Interpretation and Partition Refinement for Model Checking, P.O. Box, vol.513, 1996.

D. System, Darwin system's Home Page, Distributed Software Engineering Research group, Imperial College, 2001.

W. Edsger and . D?kstra, Why is software so expensive? " An explanation to the hardware designer, 1977.

W. Edsger and . D?kstra, EWD690: The pragmatic engineer versus the scientific designer. Circulated privately Available from http, 1978.

W. Edsger and . D?kstra, Why is software so expensive? " An explanation to the hardware designer, Selected Writings on Computing: A Personal Perspective, pp.338-348, 1982.

B. Dutertre and S. Schneider, Using a PVS embedding of CSP to verify authentication protocols, Theorem Proving in Higher Order Logics: 10th International Conference . TPHOLs'97, number 1275 in Lecture Notes in Computer Science, pp.121-136, 1997.
DOI : 10.1007/BFb0028390

S. Easterbrook, A. Finkelstein, J. Kramer, and B. Nuseibeh, Co-ordinating distributed ViewPoints: the anatomy of a consistency check, School of Cognitive and Computing Sciences, 1994.

H. Ehrig and G. Engels, Handbook of Graph Grammars and Computing by Graph Transformation, -Applications, Languages and Tools. World scientific, 1999.

H. Ehrig and G. Engels, Handbook of Graph Grammars and Computing by Graph Transformation, volume 3 -Concurrency, Parallelism and Distribution, World scientific, 1999.

T. Elrad, M. Aksits, G. Kiczales, K. Lieberherr, and H. Ossher, Discussing aspects of AOP, Communications of the ACM, vol.44, issue.10, pp.33-38, 2001.
DOI : 10.1145/383845.383854

T. Elrad, R. E. Filman, and A. Bader, Aspect-oriented programming: Introduction, Communications of the ACM, vol.44, issue.10, pp.29-32, 2001.
DOI : 10.1145/383845.383853

A. Emerson and J. Y. Halpern, ???Sometimes??? and ???not never??? revisited: on branching versus linear time temporal logic, Journal of the ACM, vol.33, issue.1, pp.151-178, 1986.
DOI : 10.1145/4904.4999

A. S. Evans and S. Kent, Core Meta-Modelling Semantics of UML: The pUML Approach, 2nd International Conference on the Unified Modeling Language, 1999.
DOI : 10.1007/3-540-46852-8_11

A. Finkelstein, J. Kramer, B. Nuseibeh, L. Finkelstein, and M. Goedicke, VIEWPOINTS: A FRAMEWORK FOR INTEGRATING MULTIPLE PERSPECTIVES IN SYSTEM DEVELOPMENT, International Journal of Software Engineering and Knowledge Engineering, vol.02, issue.01, pp.31-58, 1992.
DOI : 10.1142/S0218194092000038

A. Finkelstein and I. Sommerville, The Viewpoints FAQ Software Engineering Journal: Special Issue on Viewpoints for Software Engineering, pp.2-4, 1996.

C. W. Anthony, D. M. Finkelstein, A. Gabbay, J. Hunter, B. Kramer et al., Inconsistency handling in multiperspective specifications, IEEE Transactions on Software Engineering, vol.20, issue.8, pp.569-578, 1994.

F. Methods-group and C. , Formal Methods -Model Checking, 2001.

P. Fradet, D. L. Métayer, and M. Périn, Consistency checking for multiple view software architectures, Proceedings of the joint 7th European Software Engineering Conference (ESEC) and 7th ACM SIGSOFT International Symposium on the Foundations of Software Engineering (FSE-7), number 1687 in Lecture Notes in Computer Science Also available from ftp, pp.410-428, 1999.

M. Gallardo and P. Merino, A Framework for Automatic Construction of Abstract Promela Models, Dams et al. [37], pp.184-199
DOI : 10.1007/3-540-48234-2_15

D. Garlan, R. Allen, and J. Ockerbloom, Architectural mismatch or why it's hard to build systems out of existing parts, Proceedings of the 17th international conference on Software engineering , ICSE '95, pp.179-185, 1995.
DOI : 10.1145/225014.225031

D. Garlan, Software architecture, Proceedings of the conference on The future of Software engineering , ICSE '00, pp.91-101, 2000.
DOI : 10.1145/336512.336537

D. Garlan and A. J. Kompanek, Reconciling the Needs of Architectural Description with Object-Modeling Notations, pp.498-512

D. Garlan, R. T. Monroe, and D. Wile, Acme, CASCON First Decade High Impact Papers on, CASCON '10, pp.169-183, 1997.
DOI : 10.1145/1925805.1925814

D. Garlan, J. M. Ockerbloom, and D. Wile, Towards an ADL Toolkit, 2000.

D. Giannakopoulou, J. Kramer, and S. C. Cheung, Analysing the Behaviour of Distributed Systems using Tracta, Automated Software Engineering, vol.6, issue.1, pp.7-35, 1999.
DOI : 10.1023/A:1008645800955

P. Godefroid and P. Wolper, A Partial Approach to Model Checking, Information and Computation, vol.110, issue.2, pp.305-328, 1994.
DOI : 10.1006/inco.1994.1035

S. Graf and H. Saidi, Construction of abstract state graphs with PVS, Proceedings of the 9th International Conference on Computer Aided Verification (CAV'97, pp.72-83, 1997.
DOI : 10.1007/3-540-63166-6_10

J. Gray, T. Bapty, S. Neema, and J. Tuck, Handling crosscutting constraints in domain-specific modeling, Communications of the ACM, vol.44, issue.10, pp.87-93, 2001.
DOI : 10.1145/383845.383864

D. Harel, Statecharts: a visual formalism for complex systems, Science of Computer Programming, pp.231-274, 1987.
DOI : 10.1016/0167-6423(87)90035-9

D. Harel and A. Naamad, The STATEMATE semantics of statecharts, ACM Transactions on Software Engineering and Methodology, vol.5, issue.4, pp.293-333, 1996.
DOI : 10.1145/235321.235322

D. Harel and B. Rumpe, Modeling Languages: Syntax, Semantics and All That Stuff The Weizmann Institute of Science, 2000.

J. Harrison, A Machine-Checked Theory of Floating Point Arithmetic, 12th International Conference, Theorem Proving in Higher Order Logics (TPHOLs'99), pp.113-130, 1999.
DOI : 10.1007/3-540-48256-3_9

K. Havelund and J. U. Shakkebaek, Applying Model Checking in Java Verification, Dams et al. [37], p.216
DOI : 10.1007/3-540-48234-2_17

K. Havelund and N. Shankar, Experiments in theorem proving and model checking for protocol verification, FME'96: Industrial Benefit and Advances in Formal Methods, pp.662-681, 1996.
DOI : 10.1007/3-540-60973-3_113

S. Henninger, An evolutionary approach to constructing effective software reuse repositories, ACM Transactions on Software Engineering and Methodology, vol.6, issue.2, pp.111-140, 1997.
DOI : 10.1145/248233.248242

C. A. Hoare, Communicating Sequential Processes. series in Computer Science, N.J, 1985.

C. Hofmeister, R. L. Nord, and D. Soni, Describing Software Architecture with UML, Proceedings of the 1st Working IFIP Conference on Software Architecture (WICSA1), pp.145-159, 1999.
DOI : 10.1007/978-0-387-35563-4_9

J. Gerard and . Holzmann, Design and Validation of Computer Protocols

E. Prentice-hall and N. J. Cliffs, Also available from http: //cm.bell-labs.com/cm, 1991.

J. Gerard and . Holzmann, The Spin Model Checker Also available from http, IEEE Transactions on Software Engineering, vol.23, issue.5, pp.279-295, 1997.

A. Hunter, Reasoning with Conflicting Information using Quasi-Classical Logic, Journal of Logic and Computation

A. Hunter and B. Nuseibeh, Managing inconsistent specifications: reasoning, analysis, and action, ACM Transactions on Software Engineering and Methodology, vol.7, issue.4, pp.335-367, 1998.
DOI : 10.1145/292182.292187

A. Ieee, BSR) approved it as an American National Standard and it is now designated ANSI/IEEE Std 1471-2000. The site of the IEEE Architecture Working Group can be, IEEE AWG. IEEE Recommended Practice for Architectural Description of Software-Intensive Systems, 1471.

I. Iec, Reference Model for Open Distributed Processing Part 1. Overview ISO WWW site: see [91]. IEC WWW site: see [97]. Also available from ftp, 1995.

I. Iec, Reference Model for Open Distributed Processing Part 2. Foundations ISO WWW site: see [91]. IEC WWW site: see [97]. Also available from ftp, 1995.

I. Iec, Reference Model for Open Distributed Processing Part 3. Architecture ISO WWW site: see [91]. IEC WWW site: see [97]. Also available from ftp, 1995.

V. Issarny, C. Kloukinas, and A. Zarras, Systematic Aid in the Development of Middleware Architectures, Comm. ACM, 2002.

V. Issarny, T. Saridakis, and A. Zarras, Multi-view description of software architectures, Proceedings of the third international workshop on Software architecture , ISAW '98, pp.81-84
DOI : 10.1145/288408.288429

M. Jackson and P. Zave, Distributed feature composition: a virtual architecture for telecommunications services, IEEE Transactions on Software Engineering, vol.24, issue.10, pp.831-847, 1998.
DOI : 10.1109/32.729683

C. B. Jones, A pi-calculus semantics for an object-based design notation, International Conference on Concurrency Theory, pp.93-97, 1993.
DOI : 10.1007/3-540-57208-2_12

M. Mancona, K. , and A. Strohmeier, Towards a UML Profile for Software Architecture Descriptions, pp.513-527
DOI : 10.1007/3-540-40011-7_38

Y. Kesten, A. Klein, A. Pnueli, and G. Raanan, A Perfecto Verification: Combining Model Checking with Deductive Analysis to Verify Real-Life Software, Wing et al. [212], pp.173-194
DOI : 10.1007/3-540-48119-2_12

G. Kiczales, E. Hilsdale, J. Hugunin, M. Kersten, J. Palm et al., Getting started with ASPECTJ, Communications of the ACM, vol.44, issue.10, pp.59-65, 2001.
DOI : 10.1145/383845.383858

M. Klein, R. Kazman, L. Bass, S. J. Carriere, M. Barbacci et al., Attribute-Based Architectural Styles, pp.225-243

C. Kloukinas and V. Issarny, Automating the composition of middleware configurations, Proceedings ASE 2000. Fifteenth IEEE International Conference on Automated Software Engineering, pp.241-244, 2000.
DOI : 10.1109/ASE.2000.873668

C. Kloukinas and V. Issarny, SPIN-ning software architectures: a method for exploring complex systems, Proceedings Working IEEE/IFIP Conference on Software Architecture, pp.67-76
DOI : 10.1109/WICSA.2001.948409

D. Ervin and K. , The T E Xbook, volume A of Computers and Typesetting, 1986.

D. T. Ervin-knuth, The Program, volume B of Computers and Typesetting, 1986.

D. Ervin and K. , Literate Programming Number 27 in CSLI Lecture Notes Stanford University Center for the Study of Language and Information -CSLI, 1992.

G. Kotonya and I. Sommerville, Viewpoints for requirements definition, Software Engineering Journal, vol.7, issue.6, pp.375-387, 1992.
DOI : 10.1049/sej.1992.0038

D. Krieger and R. M. Adler, The emergence of distributed component platforms, Computer, vol.31, issue.3, pp.3143-53, 1998.
DOI : 10.1109/2.660189

J. C. Sampaio, P. Leite, and P. A. Freeman, Requirements Validation Through Viewpoint Resolution, IEEE Transactions on Software Engineering, vol.17, issue.12, pp.1253-1269, 1991.

R. Henry-george-liddell, H. S. Scott, and . Jones, Liddell- Scott-Jones Lexicon of Classical Greek. [Online] Available at the Perseus project, 2001.

K. Lieberherr, D. Orleans, and J. Ovlinger, Aspect-oriented programming with adaptive methods, Communications of the ACM, vol.44, issue.10, pp.39-41, 2001.
DOI : 10.1145/383845.383855

J. Lilius and I. Paltor, The Semantics of UML State Machines, 1999.

J. Lilius and I. Paltor, vUML: a tool for verifying UML models, 14th IEEE International Conference on Automated Software Engineering, 1999.
DOI : 10.1109/ASE.1999.802301

J. Lilius, I. Porres-paltor, and H. Sara, vUML WWW site, 2001.

C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani, and S. Bensalem, Property preserving abstractions for the verification of concurrent systems, Formal Methods in System Design, vol.55, issue.1, pp.11-44, 1995.
DOI : 10.1007/BF01384313

M. Lowry, K. Havelund, and J. Penix, Verification and validation of AI systems that control deep-space spacecraft, Foundations of Intelligent Systems -Tenth International Symposium on Methodologies for Intelligent Systems (ISMIS-97, pp.35-47, 1997.
DOI : 10.1007/3-540-63614-5_3

. Springer-verlag, Also available from http

D. C. Luckham, J. Kenney, L. Augustin, J. Verra, D. Bryan et al., Specification and analysis of system architecture using Rapide, IEEE Transactions on Software Engineering, vol.21, issue.4, pp.336-355, 1995.
DOI : 10.1109/32.385971

D. C. Luckham and J. Vera, An event-based architecture definition language, IEEE Transactions on Software Engineering, vol.21, issue.9, pp.717-734, 1995.
DOI : 10.1109/32.464548

C. David, J. Luckham, D. Vera, L. Bryan, F. Augustin et al., Partial Orderings of Event Sets and Their Application to Prototyping Concurrent, Timed Systems, Journal of Systems and Software, vol.21, issue.3, pp.253-265, 1993.

. Merriam-webster, s Collegiate Dictionary, 2001.

J. Magee, N. Dulay, and J. Kramer, Structuring parallel and distributed programs, Software Engineering Journal, vol.8, issue.2, pp.73-82, 1993.
DOI : 10.1049/sej.1993.0011
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.41.330

J. Magee and J. Kramer, Dynamic Structure in Software Architecture, Proceedings of the ACM SIGSOFT'96: Fourth Symposium on the Foundations of Software Engineering (FSE4), pp.3-14, 1996.

Z. Manna and A. Pnueli, Completing the temporal picture, Theoretical Computer Science, vol.83, issue.1, pp.97-130, 1991.
DOI : 10.1016/0304-3975(91)90041-Y

K. L. Mcmillan, Getting started with SMV, 1999.

L. Kenneth and . Mcmillan, Circular compositional reasoning about liveness, 1999.

L. Kenneth and . Mcmillan, Verification of Infinite State Systems by Compositional Model Checking, Conference on Correct Hardware Design and Verification Methods (CHARME'99), volume 1703 of Lecture Notes in Computer Science, pp.219-233, 1999.

K. L. Mcmillan, S. Qadeer, and J. B. Saxe, Induction in Compositional Model Checking, Computer Aided Verification, pp.312-327, 2000.
DOI : 10.1007/10722167_25

N. Medvidovic and D. S. Rosenblum, Assessing the Suitability of a Standard Design Method for Modeling Software Architectures, Software Architecture (Proc. of WICSA'1), pp.161-182, 1999.
DOI : 10.1007/978-0-387-35563-4_10

N. Medvidovic and D. S. Rosenblum, Assessing the Suitability of a Standard Design Method, Proceedings of the 1st Working Conference on Software Architecture, pp.161-182, 1999.

N. Medvidovic and R. N. Taylor, A classification and comparison framework for software architecture description languages, IEEE Transactions on Software Engineering, vol.26, issue.1, pp.70-93, 2000.
DOI : 10.1109/32.825767
URL : https://hal.archives-ouvertes.fr/hal-00444077

R. Melton and D. Garlan, Architectural Unification Also available from http, Proceedings of CASCON'97, 1997.

M. Corporation, COM : Technical Overview, 2001.

M. Corporation, DCOM : Technical Overview, 2001.

W. Milam and A. Chutinan, Model Composition and Analysis Challenge Problems, 2001.

I. Lynette, T. Millet, and . Teitelbaum, Slicing Promela and its Applications to Model Checking, Simulation, and Protocol Understanding, 4th International SPIN Workshop, pp.70-78, 1998.

M. Moriconi and R. A. Riemenschneider, Introduction to SADL 1.0, 1997.

M. Moriconi and X. Qian, Correctness and composition of software architectures, Proceedings of ACM SIGSOFT '94: Symposium on Foundations of Software Engineering, pp.164-174, 1994.
DOI : 10.1145/195274.195403

M. Moriconi, X. Qian, and R. A. Riemenschneider, Correct architecture refinement, IEEE Transactions on Software Engineering, vol.21, issue.4, pp.356-372, 1995.
DOI : 10.1109/32.385972

T. J. Mowbray, Will the Real Architecture Please Sit Down? Component Strategies Also available at the site of the IEEE Architecture Working Group at http, 1998.

C. Gail, R. J. Murphy, E. L. Walker, M. P. Baniassad, A. Robillard et al., Does Aspect-Oriented Programming Work? Comm, pp.4475-77, 2001.

P. Netinant, T. Elrad, and M. E. Fayad, A layered approach to building open aspect-oriented systems: a framework for the design of on-demand system demodularization, Communications of the ACM, vol.44, issue.10, pp.83-85, 2001.
DOI : 10.1145/383845.384200

O. Nierstrasz, S. Gibbs, and D. Tsichritzis, Component-oriented software development, Communications of the ACM, vol.35, issue.9, pp.160-165, 1992.
DOI : 10.1145/130994.131005

O. Nierstrasz and T. D. Me?ler, Research directions in software composition, ACM Computing Surveys, vol.27, issue.2, pp.262-264, 1995.
DOI : 10.1145/210376.210389

B. Nuseibeh, J. Kramer, and A. Finkelstein, A framework for expressing the relationships between multiple views in requirements specification, IEEE Transactions on Software Engineering, vol.20, issue.10, pp.760-773, 1994.
DOI : 10.1109/32.328995

B. Nuseibeh, J. Kramer, and A. Finkelstein, A framework for expressing the relationships between multiple views in requirements specification, IEEE Transactions on Software Engineering, vol.20, issue.10, pp.760-773, 1994.
DOI : 10.1109/32.328995

M. Object and . Group, The Common Object Request Broker: Architecture and Specification -Revision 2.3.1, pp.99-109, 1999.

M. Object and . Group, Model Driven Architecture, 2001.

O. John, X. Leary, R. Zhao, C. Gerth, and H. Seger, Formally Verifying IEEE Compliance of Floating-Point Hardware, Intel Technology Journal, 1999.

H. Ossher and P. Tarr, Using multidimensional separation of concerns to (re)shape evolving software, Communications of the ACM, vol.44, issue.10, pp.43-50, 2001.
DOI : 10.1145/383845.383856

G. Övergaard, Formal Specification of Object-Oriented Modelling Concepts, Royal Institute of Technology in Stockholm, 2000.

G. Övergaard, Interacting Subsystems in UML Also available from http, pp.359-368

G. Övergaard, Using the BOOM Framework for Formal Specification of the UML, Proceedings of Defining Precise Semantics for UML, 2000.

J. Andrés-díaz, M. R. Pace, and . Campo, Analyzing the role of aspects in software design, Communications of the ACM, vol.44, issue.10, pp.66-73, 2001.
DOI : 10.1145/383845.383859

R. F. Paige, A Meta-Method for Formal Method Integration97: Industrial Applications and Strengthened Foundations of Formal Methods, Proc. 4th Intl. Symposium of Formal Methods Europe), volume 1313 of Lecture Notes in Computer Science, pp.473-494, 1997.

R. F. Paige, Comparing Extended Z with a Heterogeneous Notation for Reasoning about Time and Space, Proc. Eleventh International Conference of Z Users (ZUM'98), volume 1493 of Lecture Notes in Computer Science, pp.214-232, 1998.
DOI : 10.1007/978-3-540-49676-2_16

R. F. Paige, Heterogeneous Notations for Pure Formal Method Integration, Formal Aspects of Computing, vol.10, issue.3, pp.233-242, 1998.
DOI : 10.1007/s001650050013

R. Freeman and P. , Formal Method Integration via Heterogeneous Notations, 1997.

R. Freeman and P. , Personal homepage, 2001.

C. Péraire, R. A. Riemenschneider, and V. Stavridou, Integrating the Unified Modeling Language with an Architecture Description Language, OOPSLA'99 Workshop on Rigorous Modeling and Analysis with the UML: Challenges and Limitations, 1999.

G. Priest and K. Tanaka, Logic, Paraconsistent. Stanford Encyclopedia of Philosophy The current version of the encyclopedia can be found at http, 1999.

G. Prophet, System-level design languages: to C or not to C? EDN, Electrical design news Also available from http, pp.42-52, 1999.

. Rapide-design and . Team, Guide to the Rapide 1.0 Language Reference Manuals Available from the Rapide project's Home Page, 1997.

R. Project, Rapide project's Home Page, 2001.

. React-research and . Group, The Stanford Temporal Prover, 2001.

R. A. Riemenschneider, Checking the Correctness of Architectural Transformation Steps via Proof-Carrying Architectures, pp.65-81
DOI : 10.1007/978-0-387-35563-4_5

J. E. Robbins, N. Medvidovic, D. F. Redmiles, and D. S. Rosenblum, Integrating architecture description languages with a standard design method, Proceedings of the 20th International Conference on Software Engineering, pp.209-218, 1998.
DOI : 10.1109/ICSE.1998.671120

A. W. Roscoe and P. J. Broadfoot, Proving security protocols with model checkers by data independence techniques Journal of Computer Security , Special Issue CSFW11 Also available from the Concurrency Research Group's publication web page at, p.147, 1999.

J. Rushby, Integrated Formal Verification: Using Model Checking with Automated Abstraction, Invariant Generation, and Theorem Proving, Dams et al. [37], pp.1-11
DOI : 10.1007/3-540-48234-2_1

J. Rushby, Mechanized Formal Methods: Where Next?, pp.48-51
DOI : 10.1007/3-540-48119-2_3

S. Project, SADL project's Home Page, System Design Laboratory, SRI International, 2001.

T. Saridakis, Robust Development of Dependable Software Systemes, 1999.

N. Shankar, Combining Theorem Proving and Model Checking through Symbolic Analysis, International Conference on Concurrency Theory, pp.1-16, 2000.
DOI : 10.1007/3-540-44618-4_1

M. Shaw, R. Deline, and G. Zelesnik, Abstractions and implementations for architectural connections, Proceedings of International Conference on Configurable Distributed Systems, 1996.
DOI : 10.1109/CDS.1996.509340

M. Shaw, R. Deline, D. Klein, T. Ross, D. Young et al., Abstractions for software architecture and tools to support them, IEEE Transactions on Software Engineering, vol.21, issue.4, pp.314-335, 1995.
DOI : 10.1109/32.385970

M. Shaw and D. Garlan, Software Architecture: Perspectives on an Emerging Discipline, Science and Math N.J, 1996.

J. Sifakis, Integration, the Price of Success ? Extended Abstract, pp.52-55

J. H. Anthony, I. Simons, and . Graham, 37 Things that Don't Work in Object-Oriented Modelling with UML, 2nd. ECOOP Workshop on Precise Behavioural Semantics, pp.209-232, 1998.

J. H. Anthony, I. Simons, and . Graham, 30 Things that go wrong in object modelling with UML 1.3, chapter 17, Kilov et al. [104], pp.237-257, 1999.

R. Soley, T. Omg-staff-strategy, and . Group, Model Driven Architecture, 2000.

. Springer-verlag, Also available from http

B. Spitznagel and D. Garlan, A compositional approach for constructing connectors, Proceedings Working IEEE/IFIP Conference on Software Architecture, pp.148-157
DOI : 10.1109/WICSA.2001.948424

B. Steffen, T. Margaria, M. Von, and . Beeck, Automatic Synthesis of Linear Process Models from Temporal Constraints: Bibliography An Incremental Approach, Proceedings of the AAS'97, pp.127-141, 1997.

T. Gregory and . Sullivan, Aspect-Oriented Programming Using Reflection and Metaobject Protocols, Comm. ACM, vol.44, issue.10, pp.95-97, 2001.

R. N. Taylor, N. Medvidovic, K. Anderson, E. J. Whitehead, K. A. Nies et al., A component- and message-based architectural style for GUI software, IEEE Transactions on Software Engineering, vol.22, issue.6, pp.390-406, 1996.
DOI : 10.1109/32.508313

S. Tripakis and C. Courcoubetis, Extending Promela and Spin for Real Time In Tools and Algorithms for the Construction and Analysis of Systems, TACAS'96, 1996.

S. Tripakis, Automated Module Composition, 2001.
DOI : 10.1007/3-540-36577-X_25

U. Rtf and . Uml, Semantics, version 1.1. [Online] Document ad/97- 08-04, 1997.

U. Rtf and . Omg, Unified Modeling Language Specification, version 1.3. [Online] Document ad/99-06-08. OMG UML v. 1.3 is the UML RTF's (Revision Task Force) proposed final revision, 1999.

M. Vaziri and G. Holzmann, Automatic Generation of Invariants in SPIN, SPIN [195], pp.124-133

W. Visser and H. Barringer, CTL* Model Checking for SPIN, SPIN [195], pp.32-51

T. Weigert, D. Garlan, and J. Knapman, Birger Møller-Pedersen, and Bran Selic. Modeling of Architectures with UML -Panel, Evans et al. [54], pp.556-569

D. Wile, AML: an Architecture Meta-Language, 14th IEEE International Conference on Automated Software Engineering, 1999.
DOI : 10.1109/ASE.1999.802241

R. Wirfs-brock and B. Wilkerson, Object-Oriented Design: A Responsibility-Driven Approach, Meyrowitz [138], pp.71-75

P. Wolper, Expressing Interesting Properties of Programs in Propositional Temporal Logic (extended abstract), POPL86 [169], pp.184-193

A. Zarras, Systematic Customization of Middleware, 2000.

A. Zarras and V. Issarny, Assessing Software Reliability at the Architectural Level, Proceedings of the 4th International Software Architecture Workshop, 2000.

A. Zarras, V. Issarny, C. Kloukinas, and V. Nguyen, A Base UML Extension for Architecture Description, Kruchten [113], pp.22-26

P. Zave, An Experiment in Feature Engineering Also available from http, Essays by the Members of the IFIP Technical Committee 2, Working Group 2.3 on Programming Methodology

P. Zave, Secrets of call forwarding: A specification case study, Formal Description Techniques VIIIProceedings of the Eighth International Bibliography IFIP Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, p.153
DOI : 10.1007/978-0-387-34945-9_13

P. Zave, ???Calls considered harmful??? and other observations: A tutorial on telephony, Lecture Notes in Computer Science, vol.1385, pp.8-27, 1998.
DOI : 10.1007/BFb0053493

P. Zave, An Architecture for Three Challenging Features

P. Zave, Feature-Oriented Description, Formal Methods, and DFC, FIREworks Workshop on Language Constructs for Describing Features, pp.11-26, 2001.
DOI : 10.1007/978-1-4471-0287-8_2

P. Zave, Requirements for Evolving Systems: A Telecommunications Perspective Also available from http, RE'01 Fifth IEEE International Symposium on Requirements Engineering, 2001.

P. Zave and M. Jackson, Where do operations come from? A multiparadigm specification technique, IEEE Transactions on Software Engineering, vol.22, issue.7, pp.508-528, 1996.
DOI : 10.1109/32.538607

P. Zave and M. Jackson, A component-based approach to telecommunication software, IEEE Software, vol.15, issue.5, pp.70-78, 1998.
DOI : 10.1109/52.714823

P. Zave and M. Jackson, DFC modifications II: Protocol extensions . AT&T Technical Memorandum Available from http, 1999.

P. Zave and M. Jackson, DFC modifications I (Version 2): Routing extensions Available from http, AT&T Technical Memorandum, 2000.