A major challenge in the analysis of gene expression microarray data
is to extract meaningful biological knowledge out of the huge volume
of raw data. Expander (EXPression ANalyzer and DisplayER) is an integrated
software platform for the analysis of gene expression data, which
is freely available for academic use. It is designed to support all
the stages of microarray data analysis, from raw data normalization
to inference of transcriptional regulatory networks. The microarray
analysis described in this protocol starts with importing the data
into Expander 5.0 and is followed by normalization and filtering.
Then, clustering and network-based analyses are performed. The gene
groups identified are tested for enrichment in function (based on
Gene Ontology), co-regulation (using transcription factor and microRNA
target predictions) or co-location. The results of each analysis
step can be visualized in a number of ways. The complete protocol
can be executed in ≈1 h.
close
@ARTICLE{UMS2010,
author = {Ulitsky, Igor and Maron-Katz, Adi and Shavit, Seagull and Sagir,
Dorit and Linhart, Chaim and Elkon, Ran and Tanay, Amos and Sharan,
Roded and Shiloh, Yosef and Shamir, Ron},
title = {{E}xpander: from expression microarrays to networks and functions},
journal = {Nature Protocols},
year = {2010},
volume = {5},
pages = {303--322},
number = {2},
abstract = {A major challenge in the analysis of gene expression microarray data
is to extract meaningful biological knowledge out of the huge volume
of raw data. Expander (EXPression ANalyzer and DisplayER) is an integrated
software platform for the analysis of gene expression data, which
is freely available for academic use. It is designed to support all
the stages of microarray data analysis, from raw data normalization
to inference of transcriptional regulatory networks. The microarray
analysis described in this protocol starts with importing the data
into Expander 5.0 and is followed by normalization and filtering.
Then, clustering and network-based analyses are performed. The gene
groups identified are tested for enrichment in function (based on
Gene Ontology), co-regulation (using transcription factor and microRNA
target predictions) or co-location. The results of each analysis
step can be visualized in a number of ways. The complete protocol
can be executed in ≈1 h.},
doi = {10.1038/nprot.2009.230},
owner = {raphael},
timestamp = {2010.10.04}
}
close
@ARTICLE{LN2010,
author = {Laube, Ulrich and Nebel, Markus E.},
title = {{M}aximum likelihood analysis of algorithms and data structures},
journal = {Theoretical Computer Science},
year = {2010},
volume = {411},
pages = {188--212},
number = {1},
comment = {02-08},
doi = {10.1016/j.tcs.2009.09.025},
owner = {raphael},
timestamp = {2010.10.04}
}
close
@ARTICLE{YamBo2009,
author = {Takuji Yamada and Peer Bork},
title = {{E}volution of biomolecular networks — lessons from metabolic and
protein interactions},
journal = {Nature Reviews Molecular Cell Biology},
year = {2009},
volume = {10},
pages = {791--803},
month = {November},
comment = {01-13},
owner = {raphael},
timestamp = {2010.03.24},
url = {http://www.nature.com/nrm/journal/v10/n11/abs/nrm2787.html}
}
close
Molecular function is the result of proteins working together, mediated
by highly specific interactions. Maintenance and change of protein
interactions can thus be considered one of the main links between
molecular function and mutation. As a consequence, protein interaction
datasets can be used to study functional evolution directly. In terms
of constraining change, the co-evolution of interacting molecules
is a very subtle process. This has implications for the signal being
used to predict protein–protein interactions. In terms of functional
change, the ‘rewiring’ of interaction networks, gene duplication
is critically important. Interestingly, once duplication has occurred,
the genes involved have different probabilities of being retained
related to how they were generated. In the present paper, we discuss
some of our recent work in this area.
close
@ARTICLE{RobLo2009,
author = {David L. Robertson and Simon C. Lovell},
title = {{E}volution in protein interaction networks: co-evolution, rewiring
and the role of duplication},
journal = {Biochemical Society Transactions},
year = {2009},
volume = {37},
pages = {768--771},
abstract = {Molecular function is the result of proteins working together, mediated
by highly specific interactions. Maintenance and change of protein
interactions can thus be considered one of the main links between
molecular function and mutation. As a consequence, protein interaction
datasets can be used to study functional evolution directly. In terms
of constraining change, the co-evolution of interacting molecules
is a very subtle process. This has implications for the signal being
used to predict protein–protein interactions. In terms of functional
change, the ‘rewiring’ of interaction networks, gene duplication
is critically important. Interestingly, once duplication has occurred,
the genes involved have different probabilities of being retained
related to how they were generated. In the present paper, we discuss
some of our recent work in this area.},
comment = {01-15},
doi = {10.1042/BST0370768},
keywords = {co-evolution, duplication, protein interaction network, protein–protein
interaction, rewiring},
owner = {raphael},
timestamp = {2010.03.24},
url = {http://www.biochemsoctrans.org/bst/037/0768/bst0370768.htm}
}
close
@ARTICLE{MLK2008,
author = {Muller, Franz-Josef and Laurent, Louise C. and Kostka, Dennis and
Ulitsky, Igor and Williams, Roy and Lu, Christina and Park, In-Hyun
and Rao, Mahendra S. and Shamir, Ron and Schwartz, Philip H. and
Schmidt, Nils O. and Loring, Jeanne F.},
title = {{R}egulatory networks define phenotypic classes of human stem cell
lines},
journal = {Nature},
year = {2008},
volume = {455},
pages = {401--405},
comment = {02-07},
doi = {10.1038/nature07213},
owner = {raphael},
timestamp = {2010.10.04}
}
close
@ARTICLE{BaHuT2006,
author = {Nizar N. Batada and Laurence D. Hurst and Mike Tyers},
title = {{E}volutionary and {P}hysiological {I}mportance of {H}ub {P}roteins},
journal = {PLoS Computational Biology},
year = {2006},
volume = {2},
pages = {748--756},
month = {July},
note = {Issue 7, e88},
comment = {01-14},
owner = {raphael},
timestamp = {2010.03.24},
url = {http://www.ncbi.nlm.nih.gov/pmc/articles/PMC1500817/}
}
close
BACKGROUND:RNA secondary structure prediction methods based on probabilistic
modeling can be developed using stochastic context-free grammars
(SCFGs). Such methods can readily combine different sources of information
that can be expressed probabilistically, such as an evolutionary
model of comparative RNA sequence analysis and a biophysical model
of structure plausibility. However, the number of free parameters
in an integrated model for consensus RNA structure prediction can
become untenable if the underlying SCFG design is too complex. Thus
a key question is, what small, simple SCFG designs perform best for
RNA secondary structure prediction?
RESULTS:Nine different small SCFGs were implemented to explore the
tradeoffs between model complexity and prediction accuracy. Each
model was tested for single sequence structure prediction accuracy
on a benchmark set of RNA secondary structures.
CONCLUSIONS:Four SCFG designs had prediction accuracies near the performance
of current energy minimization programs. One of these designs, introduced
by Knudsen and Hein in their PFOLD algorithm, has only 21 free parameters
and is significantly simpler than the others.
close
@ARTICLE{DowEd2004,
author = {Robin Dowell and Sean Eddy},
title = {{E}valuation of several lightweight stochastic context-free grammars
for {RNA} secondary structure prediction},
journal = {BMC Bioinformatics},
year = {2004},
volume = {5},
pages = {71},
number = {1},
abstract = {BACKGROUND:RNA secondary structure prediction methods based on probabilistic
modeling can be developed using stochastic context-free grammars
(SCFGs). Such methods can readily combine different sources of information
that can be expressed probabilistically, such as an evolutionary
model of comparative RNA sequence analysis and a biophysical model
of structure plausibility. However, the number of free parameters
in an integrated model for consensus RNA structure prediction can
become untenable if the underlying SCFG design is too complex. Thus
a key question is, what small, simple SCFG designs perform best for
RNA secondary structure prediction?
RESULTS:Nine different small SCFGs were implemented to explore the
tradeoffs between model complexity and prediction accuracy. Each
model was tested for single sequence structure prediction accuracy
on a benchmark set of RNA secondary structures.
CONCLUSIONS:Four SCFG designs had prediction accuracies near the performance
of current energy minimization programs. One of these designs, introduced
by Knudsen and Hein in their PFOLD algorithm, has only 21 free parameters
and is significantly simpler than the others.},
comment = {01-01},
doi = {10.1186/1471-2105-5-71},
issn = {1471-2105},
owner = {raphael},
pubmedid = {15180907},
timestamp = {2010.03.22},
url = {http://www.biomedcentral.com/1471-2105/5/71}
}
close
The secondary structure of a RNA molecule is of great importance and
possesses inuence, e.g. on the interaction of tRNA molecules with
proteins or on the stabilization of mRNA molecules. The classication
of secondary structures by means of their order proved useful with
respect to numerous applications. In 1978 Waterman, who gave the
rst precise formal framework for the topic, suggested to determine
the number a n;p of secondary structures of size n and given order
p. Since then, no satisfactory result has been found. Based on an
observation due to Viennot et al. we will derive generating functions
for the secondary structures of order p from generating functions
for binary tree structures with Horton-Strahler number p. These generating
functions enable us to compute a precise asymptotic equivalent for
a n;p . Furthermore, we will determine the related number of structures
when the number of unpaired bases shows up as an additional parameter.
Our approach proves to be general enough to compute the average order
of a secondary structure together with all the r-th moments and to
enumerate substructures such as hairpins or bulges in dependence
on the order of the secondary structures considered.
close
@ARTICLE{Nebel2001,
author = {Markus E. Nebel},
title = {{C}ombinatorial {P}roperties of {RNA} {S}econdary {S}tructures},
journal = {Journal of Computational Biology},
year = {2001},
volume = {9},
pages = {541--573},
abstract = {The secondary structure of a RNA molecule is of great importance and
possesses inuence, e.g. on the interaction of tRNA molecules with
proteins or on the stabilization of mRNA molecules. The classication
of secondary structures by means of their order proved useful with
respect to numerous applications. In 1978 Waterman, who gave the
rst precise formal framework for the topic, suggested to determine
the number a n;p of secondary structures of size n and given order
p. Since then, no satisfactory result has been found. Based on an
observation due to Viennot et al. we will derive generating functions
for the secondary structures of order p from generating functions
for binary tree structures with Horton-Strahler number p. These generating
functions enable us to compute a precise asymptotic equivalent for
a n;p . Furthermore, we will determine the related number of structures
when the number of unpaired bases shows up as an additional parameter.
Our approach proves to be general enough to compute the average order
of a secondary structure together with all the r-th moments and to
enumerate substructures such as hairpins or bulges in dependence
on the order of the secondary structures considered.},
citeseerurl = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.22.1643},
comment = {01-04},
owner = {raphael},
timestamp = {2010.03.22},
url = {http://wwwagak.informatik.uni-kl.de/staff/nebel/index.html}
}
close
Secondary structures of polynucleotides can be view as a certain class
of planar vertex-labeled graphs. We construct recursion formulae
enumerating various sub-classes of these graphs as well as certain
structural elements (sub-graphs). First order asymptotics are derived
and their dependence on the logic of base pairing is computed and
discussed.
close
@ARTICLE{HoScS1996,
author = {Ivo L. Hofacker and Peter Schuster and Peter F. Stadler},
title = {{C}ombinatorics of {RNA} {S}econdary {S}tructures},
journal = {Discr. Appl. Math},
year = {1996},
volume = {89},
pages = {-},
abstract = {Secondary structures of polynucleotides can be view as a certain class
of planar vertex-labeled graphs. We construct recursion formulae
enumerating various sub-classes of these graphs as well as certain
structural elements (sub-graphs). First order asymptotics are derived
and their dependence on the logic of base pairing is computed and
discussed.},
citeseerurl = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.56.5965},
comment = {01-02},
owner = {raphael},
timestamp = {2010.03.22}
}
close
In this paper, properties of normalized stochastic languages are discussed
and alternative procedures for constructing the Comsky and Greibach
normal forms for normalized stochastic context-free grammar (nscfg)
are presented. A normalized stochastic context-free language (nscfl)
is defined in terms of a nscfg. Furthermore, stochstic languages
accepted by stochastic pushdown automata (spda) are defined, and
relationships between stochastic context-free languages and spda
are studied. The class of languages accepted by a spda with a 0 cutpoint
is precisely the class of scfl.
close
@ARTICLE{HuaFu1971,
author = {T. Huang and K.S. Fu},
title = {{O}n {S}tochastic {C}ontext-{F}ree {L}anguages},
journal = {Information Sciences},
year = {1971},
volume = {3},
pages = {201--224},
number = {3},
abstract = {In this paper, properties of normalized stochastic languages are discussed
and alternative procedures for constructing the Comsky and Greibach
normal forms for normalized stochastic context-free grammar (nscfg)
are presented. A normalized stochastic context-free language (nscfl)
is defined in terms of a nscfg. Furthermore, stochstic languages
accepted by stochastic pushdown automata (spda) are defined, and
relationships between stochastic context-free languages and spda
are studied. The class of languages accepted by a spda with a 0 cutpoint
is precisely the class of scfl.},
comment = {01-03},
owner = {raphael},
timestamp = {2010.03.22}
}
close
@ARTICLE{Kuich1970,
author = {Werner Kuich},
title = {{O}n the {E}ntropy of {C}ontext-{F}ree {L}anguages},
journal = {Information and Control},
year = {1970},
volume = {16},
pages = {173--200},
number = {2},
owner = {raphael},
timestamp = {2010.03.22}
}
close
@BOOK{Wunsc2009,
title = {{C}omplex {V}ariables with {A}pplications},
publisher = {Dorling Kindersley (India) Pvt. Ltd.},
year = {2009},
author = {A. David Wunsch},
pages = {677},
edition = {3rd},
owner = {raphael},
timestamp = {2010.08.16},
url = {http://faculty.uml.edu/awunsch/wunsch_complex_variables/}
}
close
@BOOK{CoLRS2009,
title = {{I}ntroduction to {A}lgorithms},
publisher = {The MIT Press},
year = {2009},
author = {Thomas H. Cormen and Charles E. Leiserson and Ronald L. Rivest and
Clifford Stein},
edition = {3rd},
owner = {raphael},
timestamp = {2010.03.24}
}
close
@BOOK{Spers2008,
title = {{B}ioinformatics - {P}roblem {S}olving {P}aradigms},
publisher = {Springer-Verlag},
year = {2008},
author = {Volker Sperschneider},
owner = {raphael},
timestamp = {2010.03.22}
}
close
@BOOK{HamKl2006,
title = {{L}ineare {O}ptimierung und {N}etzwerkoptimierung},
publisher = {vieweg},
year = {2006},
author = {Horst W. Hamacher and Kathrin Klamroth},
edition = {2nd},
note = {Deutsch und Englisch},
owner = {raphael},
timestamp = {2010.03.24}
}
close
@BOOK{Ahn2006,
title = {{A}dvances in {E}volutionary {A}lgorithms},
publisher = {Springer-Verlag},
year = {2006},
editor = {Janusz Kacprzyk},
author = {Chang Wook Ahn},
volume = {18},
pages = {171},
series = {{S}tudies in {C}omputational {I}ntelligence},
owner = {raphael},
timestamp = {2010.09.23}
}
close
@BOOK{Sch2001,
title = {{T}heoretische {I}nformatik - kurzgefasst},
publisher = {Spektrum Akademischer Verlag},
year = {2001},
author = {Uwe Schöning},
edition = {4th},
owner = {raphael},
timestamp = {2010.03.22}
}
close
@BOOK{Sch2001a,
title = {{A}lgorithmik},
publisher = {Spektrum Akademischer Verlag},
year = {2001},
author = {Uwe Schöning},
edition = {1st},
owner = {raphael},
timestamp = {2010.03.24}
}
close
@BOOK{Stanl2000,
title = {{E}numerative {C}ombinatorics},
publisher = {Cambridge University Press},
year = {2000},
author = {Richard P. Stanley},
volume = {2},
edition = {2nd},
owner = {raphael},
timestamp = {2010.03.22}
}
close
@BOOK{Sch2000,
title = {{L}ogik für {I}nformatiker},
publisher = {Spektrum Akademischer Verlag},
year = {2000},
author = {Uwe Schöning},
edition = {5th},
owner = {raphael},
timestamp = {2010.03.24}
}
close
@BOOK{DuEKM1998,
title = {{B}iological {S}equence {A}nalysis: {P}robabilistic models of proteins
and nucleic acids},
publisher = {Press Syndicate of the University of Cambridge},
year = {1998},
author = {Richard Durbin and Sean R. Eddy and Anders Krogh and Graeme Mitchison},
owner = {raphael},
timestamp = {2010.03.22}
}
close
@BOOK{Wilf1990,
title = {generatingfunctionology},
publisher = {Academic Press},
year = {1990},
author = {Herbert S. Wilf},
edition = {Second Edition, Internet Edition},
owner = {raphael},
timestamp = {2010.03.22},
url = {http://www.math.upenn.edu/~wilf/DownldGF.html}
}
close
@BOOK{GrKnP1989,
title = {{C}oncrete {M}athematics},
publisher = {Addison-Wesley},
year = {1989},
author = {Ronald L. Graham and Donald E. Knuth and Oren Patashnik},
edition = {Second Edition, 27nd Printing},
owner = {raphael},
timestamp = {2010.03.22}
}
close
@BOOK{Kemp1984,
title = {{F}undamentals of the {A}verage {C}ase {A}nalysis of {P}articular
{A}lgorithms},
publisher = {John Wiley \& Sons and B. G. Teubner},
year = {1984},
author = {Rainer Kemp},
series = {Wiley-Teubner Series in Computer Science},
owner = {raphael},
timestamp = {2010.03.22}
}
close
@BOOK{Menge1972,
title = {{S}tatistik 1: {T}heorie},
publisher = {Westdeutscher Verlag},
year = {1972},
author = {Günter Menges},
edition = {2cnd},
owner = {raphael},
timestamp = {2010.03.24}
}
close
@INBOOK{JGJ1999,
chapter = {An introduction to variational methods for graphical models},
pages = {183-233},
title = {{L}earning in {G}raphical {M}odels},
publisher = {Kluwer Academic Press},
year = {1999},
author = {M. I. Jordan and Z. Ghahramani and T. S. Jaakkola and L. K. Saul},
note = {02-04},
owner = {raphael},
timestamp = {2010.09.23}
}
close
@INBOOK{ChoSc1963,
chapter = {The Algebraic Theory of Context-Free Languages},
pages = {118--161},
title = {{C}omputer {P}rogramming and {F}ormal {S}ystems},
publisher = {North-Holland Publishing Company},
year = {1963},
author = {N. Chomsky and M. P. Schützenberger},
series = {Studies in Logic and the Foundations of Mathematics},
edition = {Third Printing, 1970},
owner = {raphael},
timestamp = {2010.03.22}
}
close
Adaptation is important in dependable embedded systems to cope with
changing environmental conditions. However, adaptation significantly
complicates system design and poses new challenges to system correctness.
We propose an integrated model-based development approach facilitating
intuitive modelling as well as formal verification of dynamic adaptation
behaviour. Our modelling concepts ease the specification of adaptation
behaviour and improve the design of adaptive embedded systems by
hiding the increased complexity from the developer. Based on a formal
framework for representing adaptation behaviour, our approach allows
to employ theorem proving, model checking as well as specialised
verification techniques to prove properties characteristic for adaptive
systems such as stability.
close
@INPROCEEDINGS{AdSSV2007,
author = {Rasmus Adler and Ina Schaefer and Tobias Schuele and Eric Vecchié},
title = {{F}rom {M}odel-{B}ased {D}esign to {F}ormal {V}erification of {A}daptive
{E}mbedded {S}ystems},
booktitle = {In Proc. of ICFEM 2007},
year = {2007},
publisher = {Springer-Verlag},
abstract = {Adaptation is important in dependable embedded systems to cope with
changing environmental conditions. However, adaptation significantly
complicates system design and poses new challenges to system correctness.
We propose an integrated model-based development approach facilitating
intuitive modelling as well as formal verification of dynamic adaptation
behaviour. Our modelling concepts ease the specification of adaptation
behaviour and improve the design of adaptive embedded systems by
hiding the increased complexity from the developer. Based on a formal
framework for representing adaptation behaviour, our approach allows
to employ theorem proving, model checking as well as specialised
verification techniques to prove properties characteristic for adaptive
systems such as stability.},
citeseerurl = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.85.5419},
comment = {01-07},
owner = {raphael},
timestamp = {2010.03.23}
}
close
@INPROCEEDINGS{BG2002,
author = {Matthew J. Beal and Zoubin Ghahramani},
title = {{T}he {V}ariational {B}ayesian {EM} {A}lgorithm for {I}ncomplete
{D}ata: with {A}pplication to {S}coring {G}raphical {M}odel {S}tructures},
booktitle = {Bayesian Statistics 7},
year = {2002},
note = {02-02},
owner = {raphael},
timestamp = {2010.09.23}
}
close
A long-standing issue regarding algorithms that manipulate context-free
grammars (CFGs) in a "top-down" left-to-right fashion is that left
recursion can lead to nontermination. An algorithm is known that
transforms any CFG into an equivalent nonleft-recursive CFG, but
the resulting grammars are often too large for practical use. We
present a new method for removing left recursion from CFGs that is
both theoretically superior to the standard algorithm, and produces
very compact non-left-recursive CFGs in practice.
close
@INPROCEEDINGS{Moore2000,
author = {Robert C. Moore},
title = {{R}emoving left recursion from context-free grammars},
booktitle = {Proceedings of the 1st North American chapter of the Association
for Computational Linguistics conference},
year = {2000},
pages = {249--255},
address = {San Francisco, CA, USA},
publisher = {Morgan Kaufmann Publishers Inc.},
abstract = {A long-standing issue regarding algorithms that manipulate context-free
grammars (CFGs) in a "top-down" left-to-right fashion is that left
recursion can lead to nontermination. An algorithm is known that
transforms any CFG into an equivalent nonleft-recursive CFG, but
the resulting grammars are often too large for practical use. We
present a new method for removing left recursion from CFGs that is
both theoretically superior to the standard algorithm, and produces
very compact non-left-recursive CFGs in practice.},
comment = {01-08},
owner = {raphael},
timestamp = {2010.03.23},
url = {http://portal.acm.org/citation.cfm?id=974338#}
}
close
The authors present a technique for reducing the search-space of the
genetic algorithm (GA) to improve its performance in searching for
the globally optimal set of connection-weights. They use the notion
of equivalent solutions in the search space, and include in the reduced
search-space only one solution, called the base solution, from each
set of equivalent solutions. The iteration of the GA consists of
an additional step where the solutions are mapped to the respective
base solutions. Experiments were conducted to compare the performance
of the GAs with and without search-space reduction. The experimental
results are presented and discussed
close
@INPROCEEDINGS{SP1991,
author = {Srinivas, M. and Patnaik, L.M.},
title = {{L}earning neural network weights using genetic algorithms-improving
performance by search-space reduction},
booktitle = {Neural Networks, 1991. 1991 IEEE International Joint Conference on},
year = {1991},
pages = {2331 -2336 vol.3},
month = {nov.},
note = {02-03},
abstract = {The authors present a technique for reducing the search-space of the
genetic algorithm (GA) to improve its performance in searching for
the globally optimal set of connection-weights. They use the notion
of equivalent solutions in the search space, and include in the reduced
search-space only one solution, called the base solution, from each
set of equivalent solutions. The iteration of the GA consists of
an additional step where the solutions are mapped to the respective
base solutions. Experiments were conducted to compare the performance
of the GAs with and without search-space reduction. The experimental
results are presented and discussed},
doi = {10.1109/IJCNN.1991.170736},
keywords = {connection-weights; genetic algorithm; learning systems; learning
weights; neural network; search-space reduction; genetic algorithms;
learning systems; neural nets; search problems;},
owner = {raphael},
timestamp = {2010.09.23}
}
close
@INPROCEEDINGS{GogMe1982,
author = {Joseph A. Goguen and Jos{\'e} Meseguer},
title = {{S}ecurity {P}olicies and {S}ecurity {M}odels},
booktitle = {IEEE Symposium on Security and Privacy},
year = {1982},
pages = {11-20},
comment = {01-06},
owner = {raphael},
timestamp = {2010.03.23}
}
close
@MISC{Murphy2001,
author = {Kevin P. Murphy},
title = {{A}n {I}ntroduction to {G}raphical {M}odels},
year = {2001},
note = {02-05},
citeseerurl = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.11.1543},
doi = {10.1.1.11.1543},
owner = {raphael},
timestamp = {2010.09.23}
}
close
@PHDTHESIS{Schae2008,
author = {Ina Schaefer},
title = {{I}ntegrating {F}ormal {V}erification into the {M}odel-{B}ased {D}evelopment
of {A}daptive {E}mbedded {S}ystems},
school = {Technische Universität Kaiserslautern},
year = {2008},
month = {October},
owner = {raphael},
timestamp = {2010.03.24}
}
close
We consider noninterference formulations of security policies [7]
in
which the “interferes” relation is intransitive. Such policies provide
a
formal basis for several real security concerns, such as channel control
[17,
18], and assured pipelines [4]. We show that the appropriate formulation
of noninterference for the intransitive case is that developed by
Haigh
and Young for “multidomain security” (MDS) [9, 10]. We construct an
“unwinding theorem” [8] for intransitive polices and show that it
differs
significantly from that of Haigh and Young. We argue that their theorem
is incorrect. A companion report [22] presents a mechanically-checked
formal specification and verification of our unwinding theorem.
We consider the relationship between transitive and intransitive
for-
mulations of security. We show that the standard formulations of non-
interference and unwinding [7, 8] correspond exactly to our intransitive
formulations, specialized to the transitive case. We show that transi-
tive polices are precisely the “multilevel security” (MLS) polices,
and
that any MLS secure system satisfies the conditions of the unwinding
theorem.
We also consider the relationship between noninterference formula-
tions of security and access control formulations, and we identify
the
“reference monitor assumptions” that play a crucial role in establishing
the soundness of access control implementations.
close
@TECHREPORT{Rushb1992,
author = {John Rushby},
title = {{N}oninterference, transitivity and channel-control security policies},
institution = {-},
year = {1992},
abstract = {We consider noninterference formulations of security policies [7]
in
which the “interferes” relation is intransitive. Such policies provide
a
formal basis for several real security concerns, such as channel control
[17,
18], and assured pipelines [4]. We show that the appropriate formulation
of noninterference for the intransitive case is that developed by
Haigh
and Young for “multidomain security” (MDS) [9, 10]. We construct an
“unwinding theorem” [8] for intransitive polices and show that it
differs
significantly from that of Haigh and Young. We argue that their theorem
is incorrect. A companion report [22] presents a mechanically-checked
formal specification and verification of our unwinding theorem.
We consider the relationship between transitive and intransitive
for-
mulations of security. We show that the standard formulations of non-
interference and unwinding [7, 8] correspond exactly to our intransitive
formulations, specialized to the transitive case. We show that transi-
tive polices are precisely the “multilevel security” (MLS) polices,
and
that any MLS secure system satisfies the conditions of the unwinding
theorem.
We also consider the relationship between noninterference formula-
tions of security and access control formulations, and we identify
the
“reference monitor assumptions” that play a crucial role in establishing
the soundness of access control implementations.},
citeseerurl = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.140.8996},
comment = {01-05},
owner = {raphael},
timestamp = {2010.03.23}
}
close
@UNPUBLISHED{JBD2010,
author = {Vinay Jethava and Chiranjib Bhattacharyya and Devdatt Dubhashi and
Goutham N. Vemuri},
title = {{NETGEM}: {N}etwork embedded temporal generative model for gene expression
data},
note = {Preliminary Version},
month = {09},
year = {2010},
comment = {02-01},
owner = {raphael},
timestamp = {2010.09.23}
}
close
@UNPUBLISHED{GieSi2009,
author = {Robert Giegerich and Christian Höner zu Siederdissen},
title = {{S}emantics and {A}mbiguity of {S}tochastic {RNA} {F}amily {M}odels},
note = {TCBB Submission},
year = {2009},
comment = {01-11},
keywords = {RNA secondary structure, RNA family models, covariance models, semantic
ambiguity},
owner = {raphael},
timestamp = {2010.03.23}
}
close
@UNPUBLISHED{AdSTP2009,
author = {R. Adler and I. Schaefer and M. Trapp and A. Poetzsch-Heffter:},
title = {{C}omponent-{B}ased {M}odeling and {V}erification of {D}ynamic {A}daptation
in {S}afety-{C}ritical {E}mbedded {S}ystems},
note = {ACM Transactions on Embedded Computing Systems, 2009. (to appear)},
year = {2009},
comment = {01-10},
keywords = {Design, Reliability, Verification, Adaptive Embedded Systems, Component-Based
Modeling},
owner = {raphael},
timestamp = {2010.03.23}
}
close
@UNPUBLISHED{AdScS2008,
author = {R. Adler and I. Schaefer and T. Schüle},
title = {{M}odel-based {D}evelopment of an {A}daptive {V}ehicle {S}tability
{C}ontrol {S}ystem},
note = {Workshop "Modellbasierte Entwicklung von eingebetteten Fahrzeugfunktionen",
Modellierung 2008, Berlin},
year = {2008},
comment = {01-09},
keywords = {Adaptive Systems, Model-Based Development, Formal Verification},
owner = {raphael},
timestamp = {2010.03.23},
url = {http://softech.cs.uni-kl.de/twiki/pub/Homepage/InaSchaefer/MBEFF.pdf}
}
close
@UNPUBLISHED{Kelle2004,
author = {Wolfgang Keller},
title = {{P}ersistence {O}ptions for {O}bject-{O}riented {P}rograms},
note = {-},
year = {2004},
comment = {01-12},
owner = {raphael},
timestamp = {2010.03.23}
}
close