%
%
%
% automatically generated
% % bibtex2html acidispo.bib -force
% Date: Wed Oct 29 14:44:30 2003
% Author: jensen
%
%
%
@BOOK{Szyperski-2002,
PUBLISHER = {Addison-Wesley},
TITLE = {Component Software},
YEAR = {2002},
AUTHOR = {C. Szyperski},
ALTEDITOR = {},
OPTADDRESS = {},
OPTEDITION = {},
OPTMONTH = {},
NOTE = {2nd edition},
OPTNUMBER = {},
OPTSERIES = {},
OPTVOLUME = {}
}
@PROCEEDINGS{icse2002,
TITLE = {Proceedings of the 24th International Conference on
Software Engineering},
YEAR = {2002},
ADDRESS = {Orlando, FL, USA},
OPTEDITOR = {},
MONTH = {May},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
PUBLISHER = {ACM Press},
OPTSERIES = {},
OPTVOLUME = {},
BOOKTITLE = {Proceedings of the 24th International Conference on Software Engineering}
}
@PROCEEDINGS{reflection2001,
TITLE = {Meta-Level Architectures and Separation of Crosscutting
Concerns, Third International Conference, Reflection 2001},
YEAR = {2001},
ADDRESS = {Kyoto, Japan},
EDITOR = {A. Yonezawa and S. Matsuoka},
MONTH = {September},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {2192},
BOOKTITLE = {Meta-Level Architectures and Separation of Crosscutting Concerns, Third International Conference, Reflection 2001}
}
@BOOK{Sessions:2000,
PUBLISHER = {Wiley},
TITLE = {COM+ and the battle for the Middle Tier},
YEAR = {2000},
AUTHOR = {R. Sessions},
ALTEDITOR = {},
OPTADDRESS = {},
OPTEDITION = {},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
OPTSERIES = {},
OPTVOLUME = {}
}
@PROCEEDINGS{ase2000,
TITLE = {Proceedings of the 15th IEEE International Conference on
Automated Software Engineering (ASE 2000)},
YEAR = {2000},
ADDRESS = {Grenoble, France},
EDITOR = {V. Gruhn},
MONTH = {September},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
PUBLISHER = {ieee},
OPTSERIES = {},
OPTVOLUME = {},
BOOKTITLE = {Proceedings of the 15th IEEE International Conference on Automated Software Engineering (ASE 2000)}
}
@PROCEEDINGS{Naur-Randell:68,
TITLE = {Proceedings of the NATO Conference on Software
Engineering},
YEAR = {1968},
ADDRESS = {Garmish, Germany},
EDITOR = {P. Naur and Randell B.},
MONTH = {October},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
PUBLISHER = {NATO Science Committee},
OPTSERIES = {},
OPTVOLUME = {},
BOOKTITLE = {Proceedings of the NATO Conference on Software Engineering}
}
@ARTICLE{Myers:03:InformationFlow,
AUTHOR = {A. Myers and A. Sabelfeld},
JOURNAL = {IEEE Journal on Selected Areas in Communications},
TITLE = {Language-Based Information-Flow Security},
YEAR = {2003},
OPTMONTH = {},
OPTNOTE = {},
NUMBER = {1},
PAGES = {5--19},
VOLUME = {21}
}
@ARTICLE{[BF99c],
AUTHOR = {J.-P. Bodeveix and M. Filali},
JOURNAL = {Formal Methods in System Design},
TITLE = {Reduction and quantifier elimination techniques for
program validation},
YEAR = {2002},
OPTMONTH = {},
OPTNOTE = {},
NUMBER = {1},
PAGES = {69--89},
VOLUME = {20}
}
@ARTICLE{informatica,
AUTHOR = {Jean-Claude Royer},
JOURNAL = {Informatica},
TITLE = {The GAT Approach to Specify Mixed Systems},
YEAR = {2002},
OPTMONTH = {},
NOTE = {to appear, ISSN 0350-5596, \texttthttp://ai.ijs.si/informatica/},
OPTNUMBER = {},
OPTPAGES = {},
OPTVOLUME = {}
}
@ARTICLE{Besson:01:ModelChecking,
AUTHOR = {F. Besson and T. Jensen and D. Le Métayer and T. Thorn},
JOURNAL = {Journal of Computer Security},
TITLE = {Model ckecking security prperties of control flow graphs},
YEAR = {2001},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
PAGES = {217--250},
VOLUME = {9}
}
@ARTICLE{[BFM01],
AUTHOR = {J.-P. Bodeveix and M. Filali and C.A. Munoz},
JOURNAL = {Technique et Science Informatiques},
TITLE = {Formalisation de la méthode B en Coq et PVS},
YEAR = {2001},
MONTH = {July},
OPTNOTE = {},
NUMBER = {7},
PAGES = {901--926},
VOLUME = {20},
PUBLISHER = {Hermes}
}
@ARTICLE{jucs2000,
AUTHOR = {Christine Choppy and Pascal Poizat and Jean-Claude Royer},
JOURNAL = {Journal of Universal Computer Science},
TITLE = {The Korrigan Environment},
YEAR = {2001},
OPTMONTH = {},
NOTE = {Special issue: Tools for System Design and Verification, ISSN: 0948-6968},
NUMBER = {1},
PAGES = {19-36},
VOLUME = {7},
EDITOR = { Springer},
URL = {http://www.jucs.org/jucs_7_1}
}
@ARTICLE{CCSC01,
AUTHOR = {F. Cuppens and L. Cholvy and C. Saurel and J. Carrère},
JOURNAL = {International Journal of Intelligent Systems},
TITLE = {Merging regulations : analysis of a practical example},
YEAR = {2001},
MONTH = {November},
OPTNOTE = {},
NUMBER = {11},
OPTPAGES = {},
VOLUME = {16}
}
@ARTICLE{CG01,
AUTHOR = {F. Cuppens and A. Gabillon},
JOURNAL = {Data and Knowledge Engineering},
TITLE = {Cover Story Management},
YEAR = {2001},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
PAGES = {177--201},
VOLUME = {37}
}
@ARTICLE{CG99,
AUTHOR = {F. Cuppens and A. Gabillon},
JOURNAL = {Data and Knowledge Engineering},
TITLE = {Logical Foundations of Multilevel Databases},
YEAR = {1999},
MONTH = {March},
OPTNOTE = {},
NUMBER = {3},
PAGES = {259--291},
VOLUME = {29}
}
@ARTICLE{abcc+96a,
AUTHOR = {M. Aksit and A. Black and L. Cardelli and P. Cointe and
al},
JOURNAL = {ACM Computing Surveys},
TITLE = {Strategic Research Directions in Object Oriented
Programming},
YEAR = {1996},
MONTH = {December},
OPTNOTE = {},
NUMBER = {4},
PAGES = {691-700},
VOLUME = {28},
EDITOR = {R. Gerraoui},
KEYWORDS = {object-oriented programming,
aspect-oriented programming, distributed programming, design pattern,
framework},
URL = {http://lsewww.epfl.ch/~rachid/conferences/oowg/report3.ps}
}
@ARTICLE{kru95a,
AUTHOR = {P.B. Kruchten},
JOURNAL = {IEEE Software},
TITLE = {The $4+1$ View Model of Architecture},
YEAR = {1995},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
PAGES = {42-50},
OPTVOLUME = {}
}
@ARTICLE{alur94theory,
AUTHOR = {Rajeev Alur and David L. Dill},
JOURNAL = {Theoretical Computer Science},
TITLE = {A theory of timed automata},
YEAR = {1994},
OPTMONTH = {},
OPTNOTE = {},
NUMBER = {2},
PAGES = {183--235},
VOLUME = {126},
URL = {citeseer.nj.nec.com/alur94theory.html}
}
@ARTICLE{BC92a,
AUTHOR = {P. Bieber and F. Cuppens},
JOURNAL = {Journal of Computer Security},
TITLE = {A Logical View of Secure Dependencies},
YEAR = {1992},
OPTMONTH = {},
OPTNOTE = {},
NUMBER = {1},
PAGES = {99--129},
VOLUME = {1}
}
@ARTICLE{YG90,
AUTHOR = {C. Yu and V. Gligor},
JOURNAL = {IEEE Transactions on Software Engineering},
TITLE = {A Specification and Verification Method for Preventing
Denial of Service},
YEAR = {1990},
MONTH = {June},
OPTNOTE = {},
NUMBER = {6},
PAGES = {581--592},
VOLUME = {16}
}
@INPROCEEDINGS{Besson:03:Modular,
AUTHOR = {F. Besson and T. Jensen},
BOOKTITLE = {Proc. of 10th Int. Static Analysis Symposium (SAS'2003)},
TITLE = {Modular class analysis with datalog},
YEAR = {2003},
OPTADDRESS = {},
OPTCROSSREF = {},
EDITOR = {R. Cousot},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
PUBLISHER = {To appera in Springer LNCS},
OPTSERIES = {},
OPTVOLUME = {}
}
@INPROCEEDINGS{KBBBCDMST03,
AUTHOR = {A. Abou El Kalam and R. El Baida and P. Balbiani and
S. Benferhat and F. Cuppens and Y. Deswarte and A. Miège and
C. Saurel and G. Trouessin},
BOOKTITLE = {Policy'2003},
TITLE = {Organization Based Access Control},
YEAR = {2003},
ADDRESS = {Como, Italie},
OPTCROSSREF = {},
OPTEDITOR = {},
MONTH = {June},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
OPTPUBLISHER = {},
OPTSERIES = {},
OPTVOLUME = {}
}
@INPROCEEDINGS{segura-menaud.lmo2003,
AUTHOR = {M. Ségura-Devillechaise and J.-M. Menaud},
BOOKTITLE = {LMO 2003},
TITLE = {microDyner : Un noyau efficace pour le tissage dynamique
d'aspects sur processus natif en cours d'exécution},
YEAR = {2003},
ADDRESS = {Vannes},
OPTCROSSREF = {},
OPTEDITOR = {},
MONTH = {February},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
PAGES = {119-133},
PUBLISHER = {Hermès},
OPTSERIES = {},
OPTVOLUME = {}
}
@INPROCEEDINGS{segura-menaud-al.aosd2003,
AUTHOR = {M. Ségura-Devillechaise and J.-M. Menaud and G. Muller and
J. Lawall},
BOOKTITLE = {Proceedings of the 2nd international conference on Aspect-oriented software development},
TITLE = {Web Cache Prefetching as an aspect: Towards a
Dynamic-Weaving Based Solution},
YEAR = {2003},
ADDRESS = {Enschede, The Netherlands},
OPTCROSSREF = {},
OPTEDITOR = {},
OPTMONTH = {},
NOTE = {À paraître},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
PUBLISHER = {ACM Press},
OPTSERIES = {},
OPTVOLUME = {},
ABSTRACT = {Given the high proportion of HTTP traffic in the
Internet, Web caches are crucial to reduce user access time, network
latency, and bandwidth consumption. Prefetching in a Web cache can
further enhance these benefits. Nevertheless, to achieve the best
performance, the prefetching policy must match user and Web server
characteristics. This implies that new prefetching policies must be
loaded dynamically as needs change. Most Web caches are large C
programs, and thus adding a single prefetching policy to an existing
Web cache is a daunting task. Providing multiple policies is even
more complex. The essential problem is that prefetching concerns
crosscut the cache structure. Aspect-oriented programming is a
natural technique to address this issue. Nevertheless, existing
approaches do not provide dynamic weaving of aspects targeted toward
C applications. In this paper, we present $\mu$Dyner, which addresses
these needs. $\mu$Dyner also provides lower overhead for aspect
invocation than other dynamic approaches, thus meeting the
performance needs of Web caches.}
}
@INPROCEEDINGS{Aldrich-Chambers-Notkin:icse2002,
AUTHOR = {J. Aldrich and C. Chambers and D. Notkin},
BOOKTITLE = {Proceedings of the 24th International Conference on Software Engineering},
TITLE = {ArchJava: Connecting Software Architecture to
Implementation},
YEAR = {2002},
ADDRESS = {Orlando, FL, USA},
CROSSREF = {icse2002},
OPTEDITOR = {},
MONTH = {May},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
PAGES = {187-197},
PUBLISHER = {ACM Press},
OPTSERIES = {},
OPTVOLUME = {}
}
@INPROCEEDINGS{fmppta2002,
AUTHOR = {Michel Allemand and Jean-Claude Royer},
BOOKTITLE = {Proceedings of the 15th IPDPS 2002 Symposium, FMPPTA},
TITLE = {Mixed Formal Specification with PVS},
YEAR = {2002},
OPTADDRESS = {},
OPTCROSSREF = {},
OPTEDITOR = {},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
PUBLISHER = {IEEE Computer Society},
OPTSERIES = {},
OPTVOLUME = {}
}
@INPROCEEDINGS{Besson:02:CallingContexts,
AUTHOR = {F. Besson and de Grenier de Latour, T. and T. Jensen},
BOOKTITLE = {Proc. of 4th Int Conf. on Principles and Practice of Declarative Programming (PPDP 2002)},
TITLE = {Secure calling contexts for stack inspection},
YEAR = {2002},
OPTADDRESS = {},
OPTCROSSREF = {},
OPTEDITOR = {},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
PAGES = {76--87},
PUBLISHER = {ACM Press},
OPTSERIES = {},
OPTVOLUME = {}
}
@INPROCEEDINGS{bobeff-noye.jc2002,
AUTHOR = {G. Bobeff and J. Noyé},
BOOKTITLE = {Syste`mes a` composants adaptables et extensibles},
TITLE = {Component Specialization: Towards Deeper Adaptation},
YEAR = {2002},
ADDRESS = {Grenoble, France},
OPTCROSSREF = {},
OPTEDITOR = {},
MONTH = {October},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
OPTPUBLISHER = {},
OPTSERIES = {},
OPTVOLUME = {}
}
@INPROCEEDINGS{bobeff-noye.inhw-ecoop2002,
AUTHOR = {G. Bobeff and J. Noyé},
BOOKTITLE = {First Inheritance Workshop at ECOOP 2002},
TITLE = {On the Interaction of Partial Evaluation and Inheritance},
YEAR = {2002},
ADDRESS = {Malaga, Spain},
OPTCROSSREF = {},
OPTEDITOR = {},
MONTH = {June},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
OPTPUBLISHER = {},
OPTSERIES = {},
OPTVOLUME = {},
ABSTRACT = {In this paper, we consider a direct, source-to-source,
specialization of Java programs. In this setting, specialization does
not boil down to partially evaluating functions (here called methods)
any longer. Indeed, specialized methods have also to be encapsulated
into residual classes. We show that inheritance offers new
specialization opportunities but that these opportunities are not so
easy to benefit from because of some deep incompatibilities between
specialization as partial evaluation and specialization as
inheritance in standard object-oriented languages.}
}
@INPROCEEDINGS{Cup02,
AUTHOR = {F. Cuppens and A. Miège},
BOOKTITLE = {IEEE Symposium on Security and Privacy},
TITLE = {Alert Correlation in a Cooperative Intrusion Detection
Framework},
YEAR = {2002},
ADDRESS = {Oakland, USA},
OPTCROSSREF = {},
OPTEDITOR = {},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
OPTPUBLISHER = {},
OPTSERIES = {},
OPTVOLUME = {}
}
@INPROCEEDINGS{dfs02a,
AUTHOR = {R. Douence and P. Fradet and M. Südholt},
BOOKTITLE = {Proceedings of the ACM SIGPLAN/SIGSOFT Conference on Generative Programming and Component Engineering (GPCE'02)},
TITLE = {A framework for the detection and resolution of aspect
interactions},
YEAR = {2002},
OPTADDRESS = {},
OPTCROSSREF = {},
OPTEDITOR = {},
MONTH = {October},
NOTE = {preprint version is ftp://ftp.inria.fr/INRIA/publication/publi-pdf/RR/RR-4435.pdf},
OPTNUMBER = {},
OPTORGANIZATION = {},
PAGES = {173--188},
OPTPUBLISHER = {},
OPTSERIES = {},
OPTVOLUME = {},
KEYWORDS = {aop, static analysis},
ABSTRACT = {Aspect-Oriented Programming (AOP) promises separation of
concerns at the implementation level. However, aspects are not always
orthogonal and aspect interaction is an important problem. Currently
there is almost no support for the detection and resolution of such
interactions. The programmer is responsible for identifying
interactions between conflicting aspects and implementing conflict
resolution code. In this paper, we propose a solution to this problem
based on a generic framework for AOP. The contributions are
threefold: we present a formal and expressive crosscut language, two
static conflict analyses and some linguistic support for conflict
resolution.}
}
@INPROCEEDINGS{Douence:02:AspectInteraction,
AUTHOR = {Rémi Douence and Pascal Fradet and Mario Südholt},
BOOKTITLE = {Proceedings of the ACM SIGPLAN/SIGSOFT Conference on Generative Programming and Component Engineering},
TITLE = {A framework for the detection and resolution of aspect
interactions},
YEAR = {2002},
OPTADDRESS = {},
OPTCROSSREF = {},
OPTEDITOR = {},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
PUBLISHER = {Springer-Verlag, Lecture Notes in Computer Science 2487},
OPTSERIES = {},
OPTVOLUME = {}
}
@INPROCEEDINGS{Eluard:02:JavaCard,
AUTHOR = {Marc Eluard and Thomas Jensen},
BOOKTITLE = {Proc. of 5th Smart Card Research and Advanced Application Conference (Cardis'02)},
TITLE = {Secure object flow analysis for Java Card},
YEAR = {2002},
OPTADDRESS = {},
OPTCROSSREF = {},
OPTEDITOR = {},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
ORGANIZATION = {IFIP/USENIX},
PAGES = {97--110},
OPTPUBLISHER = {},
OPTSERIES = {},
OPTVOLUME = {}
}
@INPROCEEDINGS{farias-gueheneuc-sudholt.bs-oopsla2002,
AUTHOR = {A. Farias and Y.-G. Guéhéneuc and M. Südholt},
BOOKTITLE = {Eleventh OOPSLA Workshop on Behavioral Semantics: Serving the Customer},
TITLE = {Integrating Behavioral Protocols in Enterprise Java
Beans},
YEAR = {2002},
OPTADDRESS = {},
OPTCROSSREF = {},
EDITOR = {B. Kenneth and K. Haim},
MONTH = {October},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
PAGES = {80--89},
OPTPUBLISHER = {},
OPTSERIES = {},
OPTVOLUME = {},
KEYWORDS = {protocols, component models, detection, verification,
EJB, JavaBeans}
}
@INPROCEEDINGS{farias-sudholt.doa2002,
AUTHOR = {Andrés Farìas and Mario Südholt},
BOOKTITLE = {International Symposium on Distributed Objects and Applications (DOA)},
TITLE = {On components with explicit protocols satisfying a
notion of correctness by construction},
YEAR = {2002},
OPTADDRESS = {},
OPTCROSSREF = {},
OPTEDITOR = {},
OPTMONTH = {},
NOTE = {to appear},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
OPTPUBLISHER = {},
SERIES = {LNCS},
OPTVOLUME = {}
}
@INPROCEEDINGS{fs02b,
AUTHOR = {Andrés Farìas and Mario Südholt},
BOOKTITLE = {International Symposium on Distributed Objects and Applications (DOA)},
TITLE = {On components with explicit protocols satisfying a
notion of correctness by construction},
YEAR = {2002},
OPTADDRESS = {},
OPTCROSSREF = {},
OPTEDITOR = {},
OPTMONTH = {},
NOTE = {to appear},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
OPTPUBLISHER = {},
SERIES = {LNCS},
OPTVOLUME = {}
}
@INPROCEEDINGS{GD02,
AUTHOR = {S. Gombault and M. Diop},
BOOKTITLE = {NATO Information Systems Technology Panel Symposium on Real Time Intrusion Detection},
TITLE = {Mirador : reaction facility},
YEAR = {2002},
ADDRESS = {Lisbonne},
OPTCROSSREF = {},
OPTEDITOR = {},
MONTH = {May},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
OPTPUBLISHER = {},
OPTSERIES = {},
OPTVOLUME = {}
}
@INPROCEEDINGS{gueheneuc-douence-jussien.ase2002,
AUTHOR = {Y.-G. Guéhéneuc and R. Douence and N. Jussien},
BOOKTITLE = {Proceedings of ASE 2002 : 17th International IEEE Conference on Automated Software Engineering},
TITLE = {No Java without Caffeine -- A Tool for Dynamic Analysis
of Java Programs},
YEAR = {2002},
ADDRESS = {Edinburgh, UK},
OPTCROSSREF = {},
OPTEDITOR = {},
MONTH = {September},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
OPTPUBLISHER = {},
OPTSERIES = {},
OPTVOLUME = {}
}
@INPROCEEDINGS{tanter-segura-al.gpce2002,
AUTHOR = {E. Tanter and M. Ségura-Devillechaise and J. Noyé and
J. Piquer},
BOOKTITLE = {Proceedings of the ACM SIGPLAN/SIGSOFT Conference on Generative Programming and Component Engineering (GPCE'02)},
TITLE = {Altering Java Semantics via Bytecode Manipulation},
YEAR = {2002},
ADDRESS = {Pittsburgh, USA},
OPTCROSSREF = {},
OPTEDITOR = {},
MONTH = {October},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
OPTVOLUME = {}
}
@INPROCEEDINGS{BLM01,
AUTHOR = {A. Bouabdallah and M. Laurent-Maknavicius},
BOOKTITLE = {I3S International Symposium on Software and Systems},
TITLE = {Formal validation of an ATM security context negotiation
protocol},
YEAR = {2001},
ADDRESS = {Constantine},
OPTCROSSREF = {},
OPTEDITOR = {},
MONTH = {February},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
PAGES = {25--33},
OPTPUBLISHER = {},
OPTSERIES = {},
OPTVOLUME = {}
}
@INPROCEEDINGS{apsec2001,
AUTHOR = {Christine Choppy and Pascal Poizat and Jean-Claude Royer},
BOOKTITLE = {Proceedings of the 8th Asia-Pacific Software Engineering Conference, APSEC'2001},
TITLE = {Formal Specification of Mixed Components with Korrigan},
YEAR = {2001},
OPTADDRESS = {},
OPTCROSSREF = {},
OPTEDITOR = {},
OPTMONTH = {},
NOTE = {ISBN: 0-7695-1408-1},
OPTNUMBER = {},
OPTORGANIZATION = {},
PAGES = {169--176},
PUBLISHER = {IEEE},
OPTSERIES = {},
OPTVOLUME = {}
}
@INPROCEEDINGS{fase2001CCPP,
AUTHOR = {Christine Choppy and Pascal Poizat and Jean-Claude Royer},
BOOKTITLE = {Fundamental Approaches to Software Engineering. 4th International Conference, FASE 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001 Genova, Italy, April 2-6. 2001 Proceedings},
TITLE = {Specification of Mixed Systems in KORRIGAN with the
Support of a UML-Inspired Graphical Notation},
YEAR = {2001},
OPTADDRESS = {},
OPTCROSSREF = {},
EDITOR = {Heinrich Hussmann},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
PAGES = {124--139},
PUBLISHER = {Springer},
SERIES = {LNCS},
VOLUME = {2029}
}
@INPROCEEDINGS{Cup01,
AUTHOR = {F. Cuppens},
BOOKTITLE = {17th Annual Computer Security Applications Conference New-Orleans},
TITLE = {Managing Alerts in a Multi-Intrusion Detection
Environment},
YEAR = {2001},
ADDRESS = {New-Orleans, USA},
OPTCROSSREF = {},
OPTEDITOR = {},
MONTH = {December},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
OPTPUBLISHER = {},
OPTSERIES = {},
OPTVOLUME = {}
}
@INPROCEEDINGS{dms01a,
AUTHOR = {Rémi Douence and Olivier Motelet and Mario Südholt},
BOOKTITLE = {Meta-Level Architectures and Separation of Crosscutting Concerns, Third International Conference, Reflection 2001},
TITLE = {A formal definition of crosscuts},
YEAR = {2001},
ADDRESS = {Kyoto, Japan},
CROSSREF = {reflection2001},
EDITOR = {A. Yonezawa and S. Matsuoka},
MONTH = {September},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
PAGES = {170-186},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {2192},
KEYWORDS = {aop, formal semantics},
URL = {long version: http://www.emn.fr/info/recherche/publications/RR01/INFO-01-3.ps.gz},
ABSTRACT = {Crosscutting, i.e. relating different program points is
one of the key notions of Aspect-Oriented Programming. In this
report, we consider a general and operational model for crosscutting
based on execution monitors. A domain-specific language for the
definition of crosscuts constitutes the core of the report. The
semantics of this language is formally defined by means of parser
operators matching event patterns in execution traces. We define an
operational semantics of the matching process by means of rules
relating the operators. The use of the language is exemplified by
several sophisticated crosscut definitions. We sketch a prototype
implementation in Java default which has been systematically derived
from the language definition.}
}
@INPROCEEDINGS{fmppta2001,
AUTHOR = {Jean-Claude Royer},
BOOKTITLE = {Proceedings of the 15th IPDPS 2001 Symposium, FMPPTA},
TITLE = {Formal Specification and Temporal Proof Techniques for
Mixed Systems},
YEAR = {2001},
ADDRESS = {San Francisco, USA},
OPTCROSSREF = {},
OPTEDITOR = {},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
PUBLISHER = {IEEE Computer Society},
OPTSERIES = {},
OPTVOLUME = {}
}
@INPROCEEDINGS{[BF00],
AUTHOR = {Jean-Paul Bodeveix and Mamoun Filali},
BOOKTITLE = {Tools and algorithms for the construction and analysis of systems TACAS, Berlin},
TITLE = {FMona: a tool for expressing validation techniques over
infinite state systems},
YEAR = {2000},
ADDRESS = {Berlin},
OPTCROSSREF = {},
EDITOR = {Susanne Graf and Michael Schwartzbach},
MONTH = {27-31 mars},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
PAGES = {204-219},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {1785},
KEYWORDS = {abstraction, transition systems, model checkers,
monadic second order logic}
}
@INPROCEEDINGS{POPL2000,
AUTHOR = {T. Colcombet and P. Fradet},
BOOKTITLE = {Proc. of Principles of Programming Languages},
TITLE = {Enforcing trace properties by program transformation},
YEAR = {2000},
OPTADDRESS = {},
OPTCROSSREF = {},
OPTEDITOR = {},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
PAGES = {54-66},
PUBLISHER = {ACM Press},
OPTSERIES = {},
OPTVOLUME = {}
}
@INPROCEEDINGS{CO00,
AUTHOR = {F. Cuppens and R. Ortalo},
BOOKTITLE = {Third International Workshop on the Recent Advances in Intrusion Detection (RAID'2000)},
TITLE = {LAMBDA: A Language to Model a Database for Detection of
Attacks},
YEAR = {2000},
ADDRESS = {Toulouse, France},
OPTCROSSREF = {},
OPTEDITOR = {},
MONTH = {October},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
OPTPUBLISHER = {},
OPTSERIES = {},
OPTVOLUME = {}
}
@INPROCEEDINGS{CS99,
AUTHOR = {F. Cuppens and C. Saurel},
BOOKTITLE = {Information Systems Technology Panel Symposium on Protecting Nato Information Systems in the 21st Century},
TITLE = {Towards a formalization of availability and denial of
service},
YEAR = {1999},
ADDRESS = {Washington},
OPTCROSSREF = {},
OPTEDITOR = {},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
OPTPUBLISHER = {},
OPTSERIES = {},
OPTVOLUME = {}
}
@INPROCEEDINGS{Jensen:99:Verification,
AUTHOR = {T. Jensen and Le Métayer, D. and T. Thorn},
BOOKTITLE = {Proc. of the 20th IEEE Symp. on Security and Privacy},
TITLE = {Verification of control flow based security properties},
YEAR = {1999},
OPTADDRESS = {},
OPTCROSSREF = {},
OPTEDITOR = {},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
PAGES = {89--103},
PUBLISHER = {New York: IEEE Computer Society},
OPTSERIES = {},
OPTVOLUME = {}
}
@INPROCEEDINGS{[BF98],
AUTHOR = {J.-P. Bodeveix and M. Filali},
BOOKTITLE = {Workshop on formal methods for parallel programming: theory and applica tions},
TITLE = {On the automatic validation of parameterized Unity
programs},
YEAR = {1998},
ADDRESS = {Berlin, Germany},
OPTCROSSREF = {},
EDITOR = {J. Rolim},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
PAGES = {807-819},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {1388}
}
@INPROCEEDINGS{CC97,
AUTHOR = {L. Cholvy and F. Cuppens},
BOOKTITLE = {IEEE Symposium on Security and Privacy},
TITLE = {Analyzing Consistency of Security Policies},
YEAR = {1997},
ADDRESS = {Oakland},
OPTCROSSREF = {},
OPTEDITOR = {},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
OPTPUBLISHER = {},
OPTSERIES = {},
OPTVOLUME = {}
}
@INPROCEEDINGS{CD97,
AUTHOR = {F. Cuppens and R. Demolombe},
BOOKTITLE = {Foundations of Intelligent Systems. 10th International Symposium ISMIS'97. LNAI 1325},
TITLE = {A modal logical framework for security policies},
YEAR = {1997},
OPTADDRESS = {},
OPTCROSSREF = {},
OPTEDITOR = {},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
PUBLISHER = {Springer},
OPTSERIES = {},
OPTVOLUME = {}
}
@INPROCEEDINGS{[HJJKPRS95],
AUTHOR = {J.G. Henriksen and J.L. Jensen and M.S. Jorgensen and
N. Klarlund and R. Paige and T. Rauhe and A.B. Sandholm},
BOOKTITLE = {Workshop on Tools and Algorithms for the Construction and Analysis of Systems},
TITLE = {MONA: Monadic second-order logic in practice},
YEAR = {1995},
ADDRESS = {Aarhus},
OPTCROSSREF = {},
OPTEDITOR = {},
MONTH = {May},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
PAGES = {58-73},
OPTPUBLISHER = {},
SERIES = {http://www.brics.dk/ mona},
OPTVOLUME = {}
}
@INPROCEEDINGS{BCC94,
AUTHOR = {N. Boulahia-Cuppens and F. Cuppens},
BOOKTITLE = {IEEE Symposium on Security and Privacy},
TITLE = {Asynchronous composition and required security condition},
YEAR = {1994},
ADDRESS = {Oakland},
OPTCROSSREF = {},
OPTEDITOR = {},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
OPTPUBLISHER = {},
OPTSERIES = {},
OPTVOLUME = {}
}
@INPROCEEDINGS{Bou94b,
AUTHOR = {N. Boulahia-Cuppens and F. Cuppens and A. Gabillon and
K. Yazdanian},
BOOKTITLE = {European symposium on research in computer security},
TITLE = {Decomposition of Multilevel Objects in an
Object-Oriented Database},
YEAR = {1994},
ADDRESS = {Brighton, UK},
OPTCROSSREF = {},
OPTEDITOR = {},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
PUBLISHER = {Springer Verlag},
OPTSERIES = {},
OPTVOLUME = {}
}
@INPROCEEDINGS{McL94,
AUTHOR = {J. McLean},
BOOKTITLE = {IEEE Symposium on Security and Privacy},
TITLE = {A General Theory of Composition for Trace Sets Closed
under Selective Interleaving Functions},
YEAR = {1994},
ADDRESS = {Oakland},
OPTCROSSREF = {},
OPTEDITOR = {},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
OPTPUBLISHER = {},
OPTSERIES = {},
OPTVOLUME = {}
}
@INPROCEEDINGS{Cup93,
AUTHOR = {F. Cuppens},
BOOKTITLE = {IEEE Symposium on Security and Privacy},
TITLE = {A Logical Analysis of Authorized and Prohibited
Information Flows},
YEAR = {1993},
ADDRESS = {Oakland},
OPTCROSSREF = {},
OPTEDITOR = {},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
OPTPUBLISHER = {},
OPTSERIES = {},
OPTVOLUME = {}
}
@INPROCEEDINGS{[BCMD90],
AUTHOR = {J.R. Burch and E.M. Clarke and K.L. McMillan and
D.L. Dill},
BOOKTITLE = {5th Symposium on Logic in Computer Science},
TITLE = {Symbolic model checking: 10E20 states and beyond},
YEAR = {1990},
OPTADDRESS = {},
OPTCROSSREF = {},
OPTEDITOR = {},
MONTH = {June},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
OPTPUBLISHER = {},
OPTSERIES = {},
OPTVOLUME = {}
}
@INPROCEEDINGS{Mil90,
AUTHOR = {J. Millen},
BOOKTITLE = {Proc. of the computer security foundations workshop},
TITLE = {Hookup Security for Synchronous Machines},
YEAR = {1990},
ADDRESS = {Franconia},
OPTCROSSREF = {},
OPTEDITOR = {},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
OPTPUBLISHER = {},
OPTSERIES = {},
OPTVOLUME = {}
}
@INPROCEEDINGS{JT89,
AUTHOR = {D. Johnson and F. Thayer},
BOOKTITLE = {Proc. of the computer security foundations workshop},
TITLE = {Security and the Composition of Machines},
YEAR = {1988},
ADDRESS = {Franconia},
OPTCROSSREF = {},
OPTEDITOR = {},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
OPTPUBLISHER = {},
OPTSERIES = {},
OPTVOLUME = {}
}
@INPROCEEDINGS{McCu88a,
AUTHOR = {D. McCullough},
BOOKTITLE = {IEEE Symposium on Security and Privacy},
TITLE = {Noninterference and the Composability of Security
Properties},
YEAR = {1988},
ADDRESS = {Oakland},
OPTCROSSREF = {},
OPTEDITOR = {},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
OPTPUBLISHER = {},
OPTSERIES = {},
OPTVOLUME = {}
}
@INPROCEEDINGS{McCu87,
AUTHOR = {D. McCullough},
BOOKTITLE = {IEEE Symposium on Security and Privacy},
TITLE = {Specifications for Multi-Level Security and a Hook-Up
Property},
YEAR = {1987},
ADDRESS = {Oakland},
OPTCROSSREF = {},
OPTEDITOR = {},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
OPTPUBLISHER = {},
OPTSERIES = {},
OPTVOLUME = {}
}
@INPROCEEDINGS{Suth86,
AUTHOR = {D. Sutherland},
BOOKTITLE = {Proceedings of the 9th National Computer Security Conference},
TITLE = {A Model of Information},
YEAR = {1986},
OPTADDRESS = {},
OPTCROSSREF = {},
OPTEDITOR = {},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
OPTPUBLISHER = {},
OPTSERIES = {},
OPTVOLUME = {}
}
@INPROCEEDINGS{GM84,
AUTHOR = {J. Goguen and J. Meseguer},
BOOKTITLE = {IEEE Symposium on Security and Privacy},
TITLE = {Unwinding and Inference Control},
YEAR = {1984},
ADDRESS = {Oakland},
OPTCROSSREF = {},
OPTEDITOR = {},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
OPTPUBLISHER = {},
OPTSERIES = {},
OPTVOLUME = {}
}
@INPROCEEDINGS{McIlroy:68,
AUTHOR = {M.D. McIlroy},
BOOKTITLE = {Proceedings of the NATO Conference on Software Engineering},
TITLE = {Mass produced software components},
YEAR = {1968},
ADDRESS = {Garmish, Germany},
CROSSREF = {Naur-Randell:68},
EDITOR = {P. Naur and Randell B.},
MONTH = {October},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
PAGES = {138-155},
PUBLISHER = {NATO Science Committee},
OPTSERIES = {},
OPTVOLUME = {}
}
@INPROCEEDINGS{k+97a,
AUTHOR = {G. Kiczales and J. Lamping and A. Mendhekar and C. Maeda and
C. Lopes and J.-M. Loingtier and J. Irwin},
BOOKTITLE = {},
TITLE = {Aspect-Oriented Programming},
YEAR = {},
OPTADDRESS = {},
CROSSREF = {ecoop97},
OPTEDITOR = {},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
PAGES = {220-242},
OPTPUBLISHER = {},
OPTSERIES = {},
OPTVOLUME = {}
}
@TECHREPORT{farias-sudholt.tr2002,
AUTHOR = {A. Farias and M. Südholt},
INSTITUTION = {E'cole des Mines de Nantes},
TITLE = {On the construction of components with explicit
protocols},
YEAR = {2002},
OPTADDRESS = {},
OPTMONTH = {},
OPTNOTE = {},
NUMBER = {02/4/INFO},
OPTTYPE = {},
ABSTRACT = {Component-based programming promises to facilitate the
construction of large-scale applications, which is supported by the
important concept of interfaces. In most current component models,
interfaces essentially declare types and sets of services that a
component implements. They are not expressive enough to formulate
many properties important for component collaboration. In this paper
we consider an important class of such properties, sequencing
constraints, which components must obey when calling one another
services. We consider the integration into interfaces of sequencing
properties by means of protocols formalized in terms of finite-state
machines. The paper presents three contributions. First, a set of
protocol composition operators and a discussion of correctness
properties of such operators useful for component assembly. Second,
we provide a first step toward the integration of additional state
information into protocols. Finally, we show how JavaBeans can
benefit from the techniques we present. }
}
@TECHREPORT{CCM:2002,
AUTHOR = {Object Management Group},
INSTITUTION = {OMG},
TITLE = {CORBA Components},
YEAR = {2002},
OPTADDRESS = {},
MONTH = {June},
NOTE = {Version 3.0},
NUMBER = {formal/02-06-65},
TYPE = {Adopted Specification},
URL = {http://www.omg.org/technology/documents/formal/components.htm}
}
@TECHREPORT{[BF99b],
AUTHOR = {J.-P. Bodeveix and M. Filali},
INSTITUTION = {IRIT},
TITLE = {The FMONA tool},
YEAR = {1999},
OPTADDRESS = {},
MONTH = {May},
OPTNOTE = {},
NUMBER = {http://www.irit.fr/ACTIVITES/EQ_COS/MF/FMONA},
OPTTYPE = {}
}
@TECHREPORT{[SC99],
AUTHOR = {C. Saurel and F. Cuppens},
INSTITUTION = {ONERA DTIM},
TITLE = {Modélisation du concept de disponibilité},
YEAR = {1999},
OPTADDRESS = {},
MONTH = {January},
OPTNOTE = {},
NUMBER = {1/3740.00 DTIM},
OPTTYPE = {}
}
@TECHREPORT{hl95a,
AUTHOR = {W. Hürsch and C. Videira Lopes},
INSTITUTION = {Northeastern University},
TITLE = {Separation of Concerns},
YEAR = {1995},
OPTADDRESS = {},
OPTMONTH = {},
OPTNOTE = {},
NUMBER = {NU-CCS-95-03},
OPTTYPE = {},
KEYWORDS = {aop, metaprogramming},
URL = {ftp://www.ccs.neu.edu/pub/people/crista/papers/separation.ps},
ABSTRACT = {
http://www.ccs.neu.edu/research/demeter/papers/publications-abstracts.html#SEP-CONCERNS}
}
@MANUAL{DeMichiel-UmitYalcinalp-Krishnan:2001,
TITLE = {Enterprise JavaBeans$^{TM}$ Specification},
OPTADDRESS = {},
AUTHOR = {L.G. DeMichiel and L.Ü. Yalçinalp and S. Krishnan},
OPTEDITION = {},
MONTH = {August},
NOTE = {Version 2.0, Final Release},
ORGANIZATION = {SUN Microsystems},
YEAR = {2001}
}
@MISC{Mil92,
AUTHOR = {J. Millen},
OPTHOWPUBLISHED = {},
OPTMONTH = {},
OPTNOTE = {},
TITLE = {A Ressource Allocation Model for Denial of Service},
YEAR = {1992},
ADDRESS = {Oakland},
BOOKTITLE = {IEEE Symposium on Security and Privacy}
}
@MISC{kronosurl,
OPTAUTHOR = {},
OPTHOWPUBLISHED = {},
OPTMONTH = {},
OPTNOTE = {},
TITLE = {The tool Kronos
http://www-verimag.imag.fr/TEMPORISE/kronos/},
OPTYEAR = {},
KEY = {Kronos}
}
@MISC{uppaalurl,
OPTAUTHOR = {},
OPTHOWPUBLISHED = {},
OPTMONTH = {},
OPTNOTE = {},
TITLE = {UPPAAL - A Tool Suite for Verification of Real-Time
Systems - http:// www.docs.uu.se/docs/rtmv/uppaal/},
OPTYEAR = {},
KEY = {Uppaal}
}