@ARTICLE{AbadiL93,
AUTHOR = {Mart\'{\i}n Abadi and Leslie Lamport},
TITLE = {Composing Specifications},
VOLUME = 15,
JOURNAL = {{ACM Transactions on Programming Languages and Systems
(TOPLAS)}},
PAGES = {73-132},
PS = {AbadiL93.ps},
YEAR = 1993
}
@ARTICLE{Holzmann97,
AUTHOR = {Gerard J. Holzmann},
TITLE = {The {S}pin {M}odel {C}hecker},
JOURNAL = {IEEE Trans. on Software Engineering},
YEAR = {1997},
VOLUME = {23},
NUMBER = {5},
PAGES = {279-295},
MONTH = {May},
PS = {Holzmann97.ps.gz}
}
@MISC{SpinPage,
AUTHOR = {Gerard J. Holzmann},
TITLE = {{SPIN}-Formal Verification},
HOWPUBLISHED = {Web Page},
NOTE = {Available at \url{http://netlib.bell-labs.com/netlib/spin/whatispin.html}}
}
@BOOK{MannaP91,
AUTHOR = {Z. Manna and A. Pnueli},
TITLE = {The Temporal Logic of Reactive and Concurrent Systems},
PUBLISHER = {Springer-Verlag},
YEAR = {1991}
}
@INPROCEEDINGS{JZ95,
AUTHOR = {Michael Jackson and Pamela Zave},
TITLE = {Deriving specifications from requirements: an Example},
BOOKTITLE = {Proceedings of the Seventeenth International
Conference on Software Engineering},
YEAR = {1995},
PAGES = {15-24},
PDF = {JZ95.pdf},
PUBLISHER = {IEEE Computer Society Press}
}
@ARTICLE{ZJ97,
AUTHOR = {Pamela Zave and Michael Jackson},
TITLE = {Four dark corners of requirements engineering},
JOURNAL = {{\em ACM Transactions on Software Engineering and
Methodology}},
YEAR = {1997},
VOLUME = {6},
NUMBER = {1},
PAGES = {1-30},
PDF = {ZJ97.pdf},
MONTH = {January}
}
@INPROCEEDINGS{JZ92,
AUTHOR = {Michael Jackson and Pamela Zave},
TITLE = {Domain descriptions},
BOOKTITLE = {Proceedings of the IEEE International Symposium on
Requirements Engineering},
YEAR = {1992},
PAGES = {56-64},
PUBLISHER = {IEEE Computer Society Press}
}
@INPROCEEDINGS{KimVBKLS99,
AUTHOR = {Moonjoo Kim and Mahesh Viswanathan and Han\^ene Ben-Abdallah
and Sampath Kannan and Insup Lee and Oleg Sokolsky},
TITLE = {Formally Specified Monitoring of Temporal Properties},
BOOKTITLE = {Proceedings European Conference on Real-Time Systems},
YEAR = 1999
}
@TECHREPORT{KimVBKLS98,
AUTHOR = {Moonjoo Kim and Mahesh Viswanathan and Han\^ene Ben-Abdallah
and Sampath Kannan and Insup Lee and Oleg Sokolsky},
TITLE = {A Framework for Run-time Correctness Assurance of Real-Time
Systems},
INSTITUTION = {University of Pennsylvania},
YEAR = 1998,
NUMBER = {MS-CIS-98-37},
PS = {http://www.cis.upenn.edu/~rtg/mac/lang-man.ps}
}
@INPROCEEDINGS{LeeKKSV99,
AUTHOR = {I. Lee and S. Kannan and M. Kim and O. Sokolsky and
M.Viswanathan},
TITLE = {Runtime Assurance Based On Formal Specifications},
BOOKTITLE = {Proceedings International Conference on Parallel and Distributed
Processing Techniques and Applications},
PS = {http://www.cis.upenn.edu/~rtg/mac/doc/99pdpta.ps.gz},
YEAR = 1999
}
@INCOLLECTION{MitchellSS98,
AUTHOR = {J. C. Mitchell and V. Shmatikov and U. Stern},
TITLE = {Finite-State Analysis of {SSL} 3.0},
BOOKTITLE = {Seventh USENIX Security Symposium},
PUBLISHER = {USENIX},
YEAR = 1998,
PAGES = {201-216},
ADDRESS = {San Antonio},
PS = {MitchellSS98.ps}
}
@TECHREPORT{JacksonNW97,
AUTHOR = {Daniel Jackson and Yuchung Ng and Jeannette Wing},
TITLE = {A Nitpick Analysis of Mobile IPv6},
INSTITUTION = {Carnegie Mellon University},
YEAR = 1998,
MONTH = {March},
PS = {JacksonNW97.ps}
}
@INPROCEEDINGS{MoLi97,
AUTHOR = { Aloysius K. Mok and Guangtian Liu},
TITLE = { Efficient Run-time Monitoring of Timing Constraints},
BOOKTITLE = {IEEE Real-Time Technology and Applications Symposium },
YEAR = 1997,
MONTH = JUN,
PS = {MoLi97.ps}
}
@ARTICLE{Jah90,
AUTHOR = {F. Jahanian and A. Goyal},
TITLE = {A formalism for monitoring real-time constraints at
run-time},
JOURNAL = {20th Int. Symp. on Fault-Tolerant Computing Systems
(FTCS-20)},
PAGES = {148--55},
PUBLISHER = {IEEE Computer Society Press},
ADDRESS = {Newcastle upon Tyne, UK},
YEAR = {1990},
ABSTRACT = {A formalism is presented for specification and
analysis of real-time constraints of systems at run
time. Real-time logic (RTL) is employed to illustrate
how timing properties can be specified elegantly in the
form of annotation added to a program (or to a design
specification). The algorithms for detecting a
violation of a timing property at runtime, expressed in
RTL, are presented.}
}
@ARTICLE{LiCo92,
TITLE = {A Specificational Approach to High Level Program Monitoring and
Measuring},
AUTHOR = {Yingsha Liao and Donald Cohen},
JOURNAL = {IEEE Transactions on Software Engineering},
PAGES = {969--979},
MONTH = NOV,
YEAR = 1992,
VOLUME = 18,
NUMBER = 11,
SOURCE = {http://theory.lcs.mit.edu/~dmjones/hbp/bibs/ley/tse/ieeetse.bib}
}
@MISC{Somos98,
TITLE = {Monitoring Server},
NOTE = {\url{http://www.compsvcs.com/somos.html}},
YEAR = 1998
}
@MISC{Rover97,
TITLE = {Time Rover Home Page},
YEAR = 1997,
NOTE = {\url{http://www.time-rover.com/}}
}
@BOOK{Holzmann91,
AUTHOR = {Gerard J. Holzmann},
TITLE = {Design and Validation of Computer Protocols},
PUBLISHER = {Prentice Hall},
YEAR = 1991,
ISBN = 0135399254,
NOTE = {\url{http://cm.bell-labs.com/cm/cs/what/spin/Doc/Book91.html}}
}
@INPROCEEDINGS{LiPo99,
AUTHOR = {Ulf Lindqvist and Phillip A. Porras},
TITLE = {Detecting Computer and Network Misuse Through the
Production-Based Expert System Toolset ({P-BEST})},
BOOKTITLE = {Proceedings of the 1999 IEEE Symposium on Security and
Privacy},
YEAR = 1999,
ADDRESS = {Oakland, California},
MONTH = MAY,
PS = {LiPo99.pdf}
}
@INPROCEEDINGS{HBG95,
AUTHOR = {Constance Heitmeyer and Alan Bull and Carolyn Gasarch
and Bruce Labaw},
TITLE = {SCR*: A toolset for Specifying and Analyzing Requirements},
BOOKTITLE = {Proceedings of the 10th Annual {IEEE} Conference on COMPuter
ASSurance (COMPASS)},
YEAR = 1995,
PS = {HBG95.ps}
}
@INPROCEEDINGS{BrockmeyerJHL97,
BOOKTITLE = {Proceedings of the IEEE Real-Time Technology and Applications
Symposium (RTAS)},
AUTHOR = {Monica Brockmeyer and Farnam Jahanian and Constance Heitmeyer and
Bruce Labaw},
TITLE = {A Flexible, Extensible Environment for Testing Real-Time
Specifications},
YEAR = 1997,
ABSTRACT = {This paper describes MTSim, an extensible, customizable simulation
platform for the Modechart Toolset (MT). MTSim provides support for
``plugging in'' of user-defined viewers which display simulation behavior in
different ways including application-specific displays. In addition, MTSim
supports full user participation in the generation of simulations through the
injection of events into the execution trace. Moreover, MTSim supports
monitoring and assertion-checking of execution traces, invoking user-specified
handlers upon assertion violation. This paper also introduces
WebSim, a web-centric suite of simulation tools for MT, on
top of the MTSim platform. It also describes a
application-specific interface built on MTSim which
represents the cockpit of an F-18 aircraft and models its
bomb-release}
}
@INPROCEEDINGS{Lin86,
AUTHOR = {H. Paul Lin},
TITLE = {Modeling a Transport Layer Protocol Using First
Order Logic},
BOOKTITLE = {{SIGCOMM}},
YEAR = 1986,
ORGANIZATION = {{ACM}}
}
@ARTICLE{McCannR99,
AUTHOR = {Petere J. McCann and Gruia-Catalin Roman},
TITLE = {Modeling Mobile IP in Mobile UNITY},
JOURNAL = {{ACM} Transactions on Software Engineering and Methodology (TOSEM)},
YEAR = 1999,
VOLUME = 8,
PAGES = {115-146},
PS = {McCannR99.ps}
}
@INPROCEEDINGS{GrobauerM,
AUTHOR = {Bernd Grobauer and Olaf {M\"{u}ller}},
TITLE = {From {I/O} Automata to Timed {I/O} Automata: A
Solution to the `Generalized Railroad Crossing' in {Isabelle/HOLCF}},
BOOKTITLE = {Procedeedings of the Conference on Theorem Provers
for Higher Order Logic},
YEAR = 1999,
PS = {GrobauerM.ps}
}
@INPROCEEDINGS{HeitmeyerJL98,
TITLE = {Applying the {SCR} Requirements Method to a Weapons
Control Panel: An Experience Report},
AUTHOR = {Constance Heitmeyer and James Kirby and Bruce Labaw},
YEAR = 1998,
BOOKTITLE = {Formal Methods in Software Practice},
ORGANIZATION = {{ACM SIGSOFT}},
MONTH = {March}
}
@BOOK{GordonM93,
EDITOR = {M. J. C. Gordon and T. F. Melham},
TITLE = {Introduction to {HOL}: A theorem proving environment for higher order logic},
PUBLISHER = {Cambridge University Press},
YEAR = 1993
}
@MISC{hol,
KEY = {HOL},
TITLE = {Home Page for the {HOL} Interactive Theorem Proving System},
HOWPUBLISHED = {\url{http://www.cl.cam.ac.uk/Research/HVG/HOL}}
}
@MISC{spin,
KEY = {SPIN},
TITLE = {Home Page for the {SPIN} Model Checker},
HOWPUBLISHED = {\url{http://netlib.bell-labs.com/netlib/spin/whatispin.html}}
}
@TECHREPORT{Rushby94,
AUTHOR = {John Rushby},
TITLE = {Critical System Properties: Survey and Taxonomy},
INSTITUTION = {SRI Internetional},
YEAR = 1993,
TYPE = {Technical Report},
NUMBER = {CSL-93-01},
NOTE = {Revised February 1994},
PS = {Rushby94.ps}
}
@INPROCEEDINGS{GunterE98,
AUTHOR = {Elsa L. Gunter},
TITLE = {Adding external decision procedures to HOL90 securely},
BOOKTITLE = {Theorem Proving in Higher Order Logics, 11th
International Conference TPHOLs '98},
ABSTRACT = {This paper describes a modest conservative extension of HOL90
that allows the results from external decision procedures to
be used within HOL90 without compromising its logical
consistency.},
YEAR = {1998},
MONTH = {September},
PS = {GunterE98.ps},
VOLUME = 1479,
PUBLISHER = {Springer-Verlag LNCS}
}
@MASTERSTHESIS{LarssonH99,
TITLE = {Routing Protocols in Wireless Ad-hoc Networks---A Simulation
Study},
AUTHOR = {Tony Larsson and Nicklas Hedman},
SCHOOL = {Lule\aa University of Technology},
ADDRESS = {Stockholm},
YEAR = 1998,
TYPE = {Master's thesis},
PDF = {LarssonH99.pdf}
}
@TECHREPORT{LabovitzABJ00,
AUTHOR = {C. Labovitz and A. Ahuja and A. Bose and F. Jahanian},
TITLE = {An Experimental Study of Internet Routing Convergence},
INSTITUTION = {Microsoft Research},
YEAR = 2000,
TYPE = {Technical Report},
NUMBER = {MSR-TR-2000-08},
PS = {LabovitzABJ00.ps}
}
@TECHREPORT{VaradhanGE96,
AUTHOR = {K. Varadhan and R. Govindan and D. Estrin},
TITLE = {Persistent Route Oscillations in Inter-Domain Routing},
INSTITUTION = {{USC}/Information Sciences Institute},
YEAR = 1996,
TYPE = {{ISI} Technical Report},
NUMBER = {96-631},
PS = {VaradhanGE96.ps}
}
@INPROCEEDINGS{GriffinW99,
AUTHOR = {Timothy G. Griffin and Gordon Wilfong},
TITLE = {An Analysis of {BGP} Convergence Properties},
EDITOR = {Guru Parulkar and Jonathan S. Turner},
PAGES = {277-288},
BOOKTITLE = {Proceedings of {ACM SIGCOMM} '99 Conference},
YEAR = 1999,
ADDRESS = {Boston},
MONTH = {August},
PS = {GriffinW99.ps}
}
@INPROCEEDINGS{GriffinSW99,
AUTHOR = {Timothy G. Griffin and F. Bruce Shepherd and Gordon Wilfong},
TITLE = {Policy Disputes in Path-Vector Protocols},
BOOKTITLE = {Proceedings of {ICNP} '99 Conference},
YEAR = 1999,
ADDRESS = {Toronto, Canada},
MONTH = {October},
PS = {GriffinSW99.ps}
}
@INPROCEEDINGS{GriffinW00,
AUTHOR = {Timothy G. Griffin and Gordon Wilfong},
TITLE = {A Safe Path Vector Protocol},
BOOKTITLE = {Proceedings of {INFOCOM} 2000 Conference},
YEAR = 2000,
ADDRESS = {Tel Aviv, Israel},
MONTH = {March},
PS = {GriffinW00.ps}
}
@INPROCEEDINGS{PerkinsR99,
AUTHOR = {Charles E. Perkins and Elizabeth M. Royer},
TITLE = {Ad-Hoc On-Demand Distance Vector Routing},
PAGES = {90-100},
BOOKTITLE = {Proceedings of the 2nd {IEEE} Workshop on Mobile
Computer Systems and Applications},
YEAR = 1999,
MONTH = {February},
PS = {PerkinsR99.ps}
}
@INPROCEEDINGS{Broch98,
AUTHOR = {Josh Broch and David A. Maltz and David B. Johnson and
Yih-Chun Hu and Jorjeta Jetcheva},
TITLE = {A Performance Comparison of Multi-Hop Wireless Ad Hoc Network
Routing Protocols},
BOOKTITLE = {Proceedings of the Fourth Annual ACM/IEEE International
Conference on Mobile Computing and Networking},
YEAR = 1998,
MONTH = {October},
PS = {Broch98.ps}
}
@ARTICLE{JohnsonM96,
AUTHOR = {David B. Johnson and David A. Maltz},
TITLE = {Dynamic Source Routing in Ad Hoc Wireless Networks},
JOURNAL = {Mobile Computing},
YEAR = 1996,
PAGES = {153-181},
PS = {JohnsonM96.ps}
}
@INPROCEEDINGS{SmithMG97,
AUTHOR = {Bradley R. Smith and Shree Murthy and {J.J.} {Garcia-Luna-Aceves}},
TITLE = {Securing distance-vector routing protocols},
PAGES = {85-92},
BOOKTITLE = {Proceedings of the 1997 Symposium on Network and Distributed System Security},
YEAR = 1997,
PUBLISHER = {{IEEE Computer Society Press}},
MONTH = {February}
}
@INPROCEEDINGS{XuDG,
AUTHOR = {Zhengyu Xu and Sa Dai and {J.J}. {Garcia-Luna-Aceves}},
TITLE = {A more efficient distance vector routing algorithm.},
PAGES = {993-997},
BOOKTITLE = {Proceedings of Milcomm 97},
YEAR = 1997,
ORGANIZATION = {{IEEE} Communications Society}
}
@ARTICLE{PerkinsB94,
AUTHOR = {Charles E. Perkins and Pravin Bhagwat},
TITLE = {Highly Dynamic Destination-Sequenced Distance-Vector
Routing ({DSDV}) for Mobile Computers},
JOURNAL = {Computer Communications Review},
YEAR = 1994,
PAGES = {234-244},
MONTH = {October},
PS = {PerkinsB94.ps}
}
@ARTICLE{RoyerT99,
AUTHOR = {Elizabeth M. Royer and Chai-Keong Toh},
TITLE = {A Review of Current Routing Protocols for Ad Hoc
Mobile Wireless Networks},
JOURNAL = {{IEEE} Personal Communications},
YEAR = 1999,
PAGES = {46-55},
MONTH = {April}
}
@INPROCEEDINGS{Chiang97,
AUTHOR = {{C.-C.} Chiang},
TITLE = {Routing in Clustered Multihop, Mobile Wireless
Networks with Fading Channel},
PAGES = {197-211},
BOOKTITLE = {Proceedings of {IEEE SICON '97}},
YEAR = 1997,
MONTH = {April}
}
@BOOK{Perlman92,
AUTHOR = {R. Perlman},
TITLE = {Interconnections: Bridges and Routers},
PUBLISHER = {Addison-Wesley},
YEAR = 1992
}
@INPROCEEDINGS{Perlman85,
AUTHOR = {R. Perlman},
TITLE = {An algorithm for distributed computation of spanning trees in an extended {LAN}},
BOOKTITLE = {Proceedings of the Ninth Data Communications Symposium},
PAGES = {44-53},
YEAR = 1985,
MONTH = {September}
}
@BOOK{Huitema95,
AUTHOR = {Christian Huitema},
TITLE = {Routing in the Internet},
PUBLISHER = {Prentice Hall},
YEAR = 1995
}
@INPROCEEDINGS{BellurO99,
AUTHOR = {Bhargav Bellur and Richard G. Ogier},
TITLE = {A Reliable, Efficient Topology Broadcast Protocol
for Dynamic Networks},
BOOKTITLE = {{IEEE} Infocomm},
YEAR = 1999,
PUBLISHER = {{IEEE}}
}
@BOOK{BertsekasG91,
AUTHOR = {Dimitri P. Bertsekas and Robert Gallager },
TITLE = {Data Networks},
PUBLISHER = {Prentice Hall},
YEAR = 1991,
ISBN = 0132009161
}
@MISC{NSPage,
AUTHOR = {The {VINT} {P}roject},
TITLE = {The ns {N}etwork {S}imulator},
HOWPUBLISHED = {Web Page},
NOTE = {Available at \url{http://www-mash.CS.Berkeley.EDU/ns}}
}
@MANUAL{NSManual,
TITLE = {ns {N}otes and {D}ocumentation},
AUTHOR = {Kevin Fall and Kannan Varadhan},
ORGANIZATION = {The {VINT} Project},
MONTH = {February},
YEAR = {2000}
}
@TECHREPORT{Bajaj99,
AUTHOR = {Sandeep Bajaj and Lee Breslau and Deborah Estrin and Kevin Fall,
Sally Floyd and Padma Haldar and Mark Handley and Ahmed Helmy and John
Heidemann and Polly Huang and Satish Kumar and Steven McCanne and Reza
Rejaie and Puneet Sharma and Kannan Varadhan and Ya Xu and
Haobo Yu and Daniel Zappala.},
TITLE = {Improving Simulation For Network Research},
INSTITUTION = {{USC}},
YEAR = 1999,
TYPE = {{USC} Technical Report},
NUMBER = {99-702}
}
@INPROCEEDINGS{PoNe97,
AUTHOR = {Phillip A. Porras and Peter G. Neumann},
TITLE = {EMERALD: Event Monitoring Enabling Responses to Anomalous Live
Disturbances},
BOOKTITLE = {National Information Systems Security Conference},
YEAR = 1997,
PS = {PoNe97.ps}
}
@TECHREPORT{AFV95,
AUTHOR = {Debra Anderson and Thane Frivold and Alfonso Valdes},
TITLE = {Next-generation Intrusion Detection Expert System ({NIDES}) : A
Summary},
NOTE = {SRI-CSL-95-07},
MONTH = MAY,
YEAR = 1995
}
@BOOK{FordF62,
AUTHOR = {L. R. Ford~Jr. and D. R. Fulkerson},
TITLE = {Flows in Networks},
PUBLISHER = {Princeton University Press},
YEAR = 1962
}
@INPROCEEDINGS{Guttman97,
AUTHOR = {Joshua D. Guttman},
TITLE = {Filtering Postures: Local Enforcement for Global Policies},
BOOKTITLE = {Proceedings of IEEE Symposium on Security and Privacy},
OPTCROSSREF = {},
OPTKEY = {},
OPTPAGES = {},
YEAR = {1997},
PS = GUTTMAN97.PS,
OPTEDITOR = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTSERIES = {},
OPTADDRESS = {},
OPTMONTH = {},
OPTORGANIZATION = {},
OPTPUBLISHER = {},
OPTNOTE = {},
OPTANNOTE = {}
}
@TECHREPORT{Guttman97t,
AUTHOR = {Joshua D. Guttman},
TITLE = {Filtering Postures: Local Enforcement for Global Policies},
INSTITUTION = {The MITRE Corporation},
YEAR = {1997},
OPTKEY = {},
OPTTYPE = {},
OPTNUMBER = {},
OPTADDRESS = {},
OPTMONTH = {},
OPTNOTE = {},
OPTANNOTE = {}
}
@ARTICLE{BochmannDZ89,
AUTHOR = {{Bochmann}, {G.v.} and {Dssouli}, {R.} and {Zhao},
{J.R.}},
TITLE = {Trace analysis for conformance and arbitration testing},
JOURNAL = {I{EEE} {T}r. on {S}oft. {E}ng.},
VOLUME = {15},
NUMBER = {11},
PAGES = {1347-1356},
MONTH = NOV,
YEAR = 1989
}
@INPROCEEDINGS{BochmannB89,
AUTHOR = {{Bochmann}, {G.v.} and {Bellal}, {O.}},
TITLE = {Test result analysis with respect to formal
specifications},
BOOKTITLE = {Proc. 2-nd {I}nt. {W}orkshop on {P}rotocol {T}est
{S}ystems, {B}erlin},
PAGES = {272-294},
MONTH = OCT,
ABSTRACT = {There are two aspects to testing: (1) the selection of
appropriate test inputs and (2) the analysis of the
observed interactions of the implementation under test
({IUT}) in order to determine whether they conform to
the {IUT}'s specification. {T}he paper considers the
second aspect with particular attention to the testing
of {OSI} communication protocol implementations. {A}
system is described which analyses an observed test
trace of interactions with respect to a reference
specification which is assumed to be written in
{LOTOS}. {I}n the case that an error is detected, the
system also provides some diagnostic information for
locating the \"error\" in the analyzed trace.
{T}he practical use of such a trace analysis system is
discussed, as well as the possibility of using a
similar approach for the validation of the verdicts
which are included in the standardized {OSI}
conformance test cases.},
KEYWORDS = {Testing, {S}pecification, {P}rotocol},
YEAR = 1989,
PS = {BochmannB89.ps.gz}
}
@INPROCEEDINGS{BochmannDDOS90,
AUTHOR = {{Bochmann}, {G.v.} and {Desbiens}, {D.} and {Dubuc},
{M.} and {Ouimet}, {D.} and {Saba}, {F.}},
TITLE = {Test result analysis and validation of test verdicts},
BOOKTITLE = {Proc. {W}orkshop on {P}rotocol {T}est {S}ystems
({IFIP})},
KEYWORDS = {Testing, {TETRA}, {T}race {A}nalysis},
ABSTRACT = {Formal description techniques ({FDT}'s) are useful in
the protocol development cycle, particulary in the
conformance testing area. {I}n this paper, we present
{TETRA}, a test and trace analysis tool based on the
{LOTOS} {FDT} which can be used to automatically
compare the specified verdicts of a conformance test
case with a protocol specification, or to analyse
results of a test run with the reference specification.
{W}e also describe our experience with this tool for
the validation of a {X}.25 {TTCN} test suite and for
the testing of an {ACSE} implementation.},
PS = {BochmannDDOS90.ps.gz},
YEAR = 1990
}
@ARTICLE{EzustB95,
AUTHOR = {{Ezust}, {S.A.} and {Bochmann}, {G.v.}},
TITLE = {An {A}utomatic {T}race {A}nalysis {T}ool {G}enerator
for {E}stelle {S}pecifications},
JOURNAL = {Computer {C}ommunication {R}eview},
VOLUME = {25},
NUMBER = {4},
PAGES = {175-184},
NOTE = {Proceedings of {ACM} {SIGCOMM} 95 {C}onference},
MONTH = OCT,
YEAR = 1995,
PS = {EzustB95.ps.gz}
}
@INPROCEEDINGS{PetrenkoYB96,
AUTHOR = {{Petrenko}, {A.} and {Yevtushenko}, {N.} and
{Bochmann}, {G.v.}},
TITLE = {Testing deterministic implementations from
nondeterministic {FSM} specifications},
BOOKTITLE = {Proc. of 9th {I}nternational {W}orkshop on {T}esting
of {C}ommunicating {S}ystems ({IWTCS}'96)},
PAGES = {125-140},
KEYWORDS = {Testing, {FSM}, {N}on-deterministic {S}pecification},
YEAR = 1996,
PS = {PetrenkoYB96.ps.gz}
}
@INPROCEEDINGS{Paxson97,
AUTHOR = {{Paxson}, {V.}},
TITLE = {Automated {P}acket {T}race {A}nalysis of {TCP}
{I}mplementations},
BOOKTITLE = {A{CM} {SIGCOMM} '97},
MONTH = SEP,
KEYWORDS = {T{CP}, {P}acket {T}race {A}nalysis},
YEAR = 1997,
PS = {Paxson97.ps.gz}
}
@INPROCEEDINGS{Paxson97E,
AUTHOR = {{Paxson}, {V.}},
TITLE = {End-to-End Internet Packet Dynamics},
BOOKTITLE = {A{CM} {SIGCOMM} '97},
MONTH = SEP,
YEAR = 1997,
PS = {Paxson97E.ps}
}
@INPROCEEDINGS{DillonY94,
AUTHOR = {{Dillon}, {Laura K.} and {Yu}, {Q.}},
TITLE = {Oracles for {C}hecking {T}emporal {P}roperties of
{C}oncurrent {S}ystems},
BOOKTITLE = {Proceedings of the 2nd {ACM} {SIGSOFT} {S}ymposium on
{F}oundations of {S}oftware {E}ngineering
({SIGSOFT}'94)},
VOLUME = {19},
NUMBER = {5},
PAGES = {140-153},
NOTE = {Proceedings published as {S}oftware {E}ngineering
{N}otes},
KEYWORDS = {Testing, {O}racle},
YEAR = 1994,
MONTH = DEC,
PS = {DillonY94.ps.gz},
ABSTRACT = {Verifying that test executions are correct is a
crucial step in the testing process. {U}nfortunately,
it can be a very arduous and error-prone step,
especially when testing a concurrent system. {S}ystem
developers can therefore benefit from oracles
automating the verification of test executions.
{T}his paper examines the use of {G}raphical {I}nterval
{L}ogic ({GIL}) for specifying temporal properties of
concurrent systems and describes a method for
constructing oracles from {GIL} specifications. {T}he
visually intuitive representation of {GIL}
specifications makes them easier to develop and to
understand than specifications written in more
traditional temporal logics. {A}dditionally, when a
test execution violates a {GIL} specification, the
associated oracle provides information about a fault.
{T}his information can be displayed visually, together
with the execution, to help the system developer see
where in the execution a fault was detected and the
nature of the fault.
}
}
@INPROCEEDINGS{JagadeesanPPRV97,
AUTHOR = {L. J. Jagadeesan and A. Porter and C. Puchol and J. C. Ramming and
L.G.Votta},
TITLE = {Specification-based Testing of Reactive Software: Tools and
Experiments},
BOOKTITLE = {Proceedings of the International Conference on Software
Engineering},
MONTH = {May},
YEAR = 1997,
PS = {JagadeesanPPRV97.ps},
ABSTRACT = {Testing commercial software is expensive and time consuming. Automated testing methods promise to save a great deal of
time and money throughout the software industry. One approach that is well-suited for the reactive systems found in
telephone switching systems is specification-based testing.
We have built a set of tools to automatically test software applications for violations of safety properties expressed in
temporal logic. Our testing system automatically constructs finite state machine oracles corresponding to safety properties,
builds test harnesses, and integrates them with an application. The test harness then generates inputs automatically to test
the application.
We describe a study examining the feasibility of this approach for testing industrial applications. To conduct this study we
formally modeled an Automatic Protection Switching system (APS), which is an application common to many telephony
systems. We then asked a number of computer science graduate students to develop several versions of the APS and
use our tools to test them. We found that the tools are very effective, save significant amounts of human effort (at the
expense of machine resources), and are easy to use. We also discuss improvements that are needed before we can use
the tools with professional developers building commercial
products.}
}
@INPROCEEDINGS{JagadeesanPO95,
AUTHOR = {L. Jagadeesan and C. Puchol and J. Von Olnhausen},
TITLE = {Safety Property Verification of ESTEREL Programs and Applications to Telecommunications Software},
BOOKTITLE = {Proceedings of the 7th International Conference on Computer Aided Verification},
OPTCROSSREF = {},
OPTKEY = {},
PAGES = {127--140},
YEAR = {1995},
PS = JAGADEESONPO95.PS,
OPTEDITOR = {},
VOLUME = {939},
OPTNUMBER = {},
SERIES = {Lecture Notes in Computer Science},
OPTADDRESS = {},
MONTH = {July},
OPTORGANIZATION = {},
OPTPUBLISHER = {},
OPTNOTE = {},
OPTANNOTE = {}
}
@INPROCEEDINGS{Richardson94,
AUTHOR = {{Richardson}, {D.J.}},
TITLE = {T{AOS}: {T}esting with {A}nalysis and {O}racle
{S}upport},
BOOKTITLE = {Proceedings of the {I}nternational {S}ymposium on
{S}oftware {T}esting and {A}nalysis},
MONTH = AUG,
KEYWORDS = {Testing, {O}racle},
ABSTRACT = {Few would question that software testing is a
necessary activity for assuring software quality, yet
the typical testing process is a human intensive
activity and as such, it is unproductive, error-prone,
and often inadequately done. {M}oreover, testing is
seldom given a prominent place in software development
or maintenance processes, nor is it an integral part of
them. {M}ajor productivity and quality enhancements can
be achieved by automating the testing process through
tool development and use and effectively incorporating
it with development and maintenance processes.
{T}he {TAOS} toolkit, {T}esting with {A}nalysis and
{O}racle {S}upport, provides support for the testing
process. {I}t includes tools that automate many tasks
in the testing process, including management and
persistence of test artifacts and the relationships
between those artifacts, test development, test
execution, and test measurement. {A} unique aspect of
{TAOS} is its support for test oracles and their use to
verify behavioral correctness of test executions.
{TAOS} also supports structural/dependence coverage by
measuring the adequacy of test criteria coverage and
regression testing by identifying tests associated or
dependent upon modified software artifacts. {T}his is
accomplished by integrating the {P}ro{DAG} toolset,
{P}rogram {D}ependence {A}nalysis {G}raph, with {TAOS}.
{T}he combination of {P}ro{DAG} and {TAOS} supports the
use of program dependence analysis in testing,
debugging, and maintenance.
{T}his paper describes
the {TAOS} toolkit and its capabilities as well as
testing, debugging and maintenance processes based on
program dependence analysis. {W}e also describe our
experience with the toolkit and discuss our future
plans.},
PS = {Richardson94.ps.gz},
YEAR = 1994
}
@INPROCEEDINGS{OMalleyRD96,
AUTHOR = {{O'Malley}, {T.O.} and {Richardson}, {D.J.} and
{Dillon}, {L.K.}},
TITLE = {Efficient {S}pecification-{B}ased {T}est {O}racles},
BOOKTITLE = {Second {C}alifornia {S}oftware {S}ymposium ({CSS}'96)},
MONTH = APR,
ABSTRACT = {Effective testing of critical systems has been
hampered by the lack of a cost-effective method for
deciding the correctness of a program's behavior under
test. {U}sing formal specifications to describe the
critical system properties and then checking test
results against these specifications overcomes these
problems. {I}f these test oracles, which are
mechanisms for determining whether a test passes or
fails, are efficient, they can be combined with
automatic test generation to cost-effectively automate
the testing of large numbers of testcases that more
adequately cover the system requirements and structure.
{T}his paper presents a algorithm for automatically
deriving efficient test oracles from {G}raphical
{I}nterval {L}ogic ({GIL}), which is a graphical
temporal logic that is easier for non-experts to
understand than many formal languages. {T}o develop
efficient test oracles from {GIL}, we convert the
specifications into automata that can be checked in
time linear in the length of the trace. {A}dditionally,
the automata can be checked incrementally to identify
the failure when it occurs, which provides the
opportunity to obtain useful information about the
erroneous state of the system. {W}e have implemented a
tool that converts {GIL} specifications into automata
based on the algorithms presented in this paper.},
PS = {OMalleyRD96.ps.gz},
YEAR = 1996
}
@INPROCEEDINGS{DillonR96,
AUTHOR = {{Dillon}, {Laura K.} and {Ramakrishna}, {Y.S.}},
TITLE = {Generating {O}racles from {Y}our {F}avorite {T}emporal
{L}ogic {S}pecifications},
BOOKTITLE = {Proc. 4th {ACM} {SIGSOFT} {S}ymp. {F}oundations of
{S}oftware {E}ngineering, {S}an {F}rancisco},
PAGES = {106-117},
MONTH = OCT,
ABSTRACT = {This paper describes a generic tableau algorithm,
which is the basis for a general customizable method
for producing oracles from temporal logic
specifications. {A} generic argument gives semantic
rules with which to build the semantic tableau for a
specification. {P}arameterizing the tableau algorithm
by semantic rules permits it to easily accommodate a
variety of temporal operators and provides a clean
mechanism for fine-tuning the algorithm to produce
efficient oracles. {T}he paper develops conditions
to ensure that a set of rules results in a correct
tableau procedure. {I}t gives sample rules for a
variety of linear-time temporal operators and shows how
rules are tailored to reduce the size of an oracle.},
PS = {DillonR96.ps.gz},
YEAR = 1996,
KEYWORDS = {Testing, {GIL}, {T}ableau, {O}racle}
}
@INPROCEEDINGS{RichardsonAOM,
AUTHOR = {{Richardson}, {D.J.} and {Aha}, {S. Leif} and
{O'Malley}, {T.O.}},
TITLE = {Specification-{B}ased {O}racles for {R}eactive
{S}ystems},
BOOKTITLE = {14th {I}nternational {C}onference on {S}oftware
{E}ngineering},
MONTH = MAY,
KEYWORDS = {Testing, {S}pecification, {O}racles, {R}eactive},
ABSTRACT = {The testing process is typically systematic in test
data selection and test execution. {F}or the most part,
however, the effective use of test oracles has been
neglected, even though they are a critical component of
the testing process. {T}est oracles prescribe
acceptable behavior for test execution. {I}n the
absence of judging test results with oracles, testing
does not achieve its goal of revealing failures or
assuring correct behavior in a practical manner; manual
result checking is neither reliable nor cost-effective.
{W}e argue that test oracles should be derived from
specifications and in conjunction with testing
criteria, represented in a common form, and their use
made integral to the testing process. {F}or complex,
reactive systems, oracles must reflect the
multiparadigm nature of the required behavior. {S}uch
systems are often specified using multiple languages,
each selected for its utility in specifying a
particular computational paradigm. {T}hus, we are
developing an approach for deriving and using oracles
based on multiparadigm and multilingual specifications
to enable the verification of test results for reactive
systems as well as less complex systems.},
PS = {RichardsonAOM.ps.gz},
YEAR = 1992
}
@ARTICLE{Paxson99,
AUTHOR = {{Paxson}, {V.}},
TITLE = {Bro: {A} {S}ystem for {D}etecting {N}etwork
{I}ntruders in {R}eal-{T}ime},
JOURNAL = {Computer {N}etworks},
VOLUME = {31},
PAGES = {2435-2463},
NOTE = {This paper is a revision of paper that previously
appeared in {P}roc. 7th {USENIX} {S}ecurity {S}ymposium
, {J}anuary 1998},
MONTH = {14 } # DEC,
KEYWORDS = {Network {I}ntrusion {D}etection, {P}acket {T}race
{A}nalysis},
YEAR = 1999,
PS = {Paxson99.ps.gz}
}
@ARTICLE{ClarkeW96,
AUTHOR = {Edmund M. Clarke and Jeannette M. Wing},
TITLE = {Formal {M}ethods: {S}tate of the {A}rt and {F}uture {D}irections},
JOURNAL = {A{CM} {C}omputing {S}urveys},
YEAR = {1996},
OPTKEY = {},
VOLUME = {28},
NUMBER = {4},
PAGES = {626--643},
MONTH = {December},
NOTE = {report by the {W}orking {G}roup on {F}ormal {M}ethods for the {ACM} {W}orkshop on {S}trategic
{D}irections in {C}omputing {R}esearch},
ABSTRACT = {We survey recent progress in the development of mathematical
techniques for specifying and verifying complex hardware and software
systems. Many of these techniques are capable of handling
industrial-sized examples; in fact, in some cases these techniques are
already being used on a regular basis in industry. Success in formal
specification can be attributed to notations that are accessible to
system designers and to new methodologies for applying these notations
effectively. Success in verification can be attributed to the
development of new tools such as more powerful theorem provers and
model checkers than were previously available. Finally, we suggest
some general research directions that we believe are likely to lead to
technological advances. Although it is difficult to predict where the
future advances will come, optimism about the next generation of
formal methods is justified in view of the progress during the past
decade. Such progress, however, will strongly depend on continued
support for basic research on new specification languages and new
verification techniques.},
PS = {ClarkeW96.ps.gz},
OPTANNOTE = {}
}
@INPROCEEDINGS{Shankar96,
TITLE = {{PVS}: Combining Specification, Proof Checking, and
Model Checking},
AUTHOR = {N. Shankar},
BOOKTITLE = {Formal Methods in Computer-Aided Design (FMCAD '96)},
EDITOR = {Mandayam Srivas and Albert Camilleri},
PAGES = {257--264},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1166,
MONTH = NOV,
YEAR = 1996,
ADDRESS = {Palo Alto, CA},
ABSTRACT = {PVS is an automated tool for specification and verification
that is designed to exploit the synergies between language
and deduction, automation and interaction, and theorem
proving and model
checking. PVS strives for a balance between automation and interaction by using
decision procedures to simplify the tedious and obvious steps
in a proof leaving the user to interactively supply
the high-level steps in a verification. Decision procedures for BDD-based
propositional simplification and model checking, equality,
and linear arithmetic are integrated into PVS. The utility of
the
language and deductive features of PVS have been demonstrated in a number of
examples, including the specification and partial
verification of the Rockwell-Collins AAMP5 processor design,
and the verification of an SRT divider. This tutorial concentrates on the
integration of individual verification techniques available
in PVS. },
PS = {Shankar96.ps.gz}
}
@INPROCEEDINGS{MullerN95,
AUTHOR = {Olaf Muller and Tobias Nipkow},
TITLE = {Combining model checking and deduction for I/O-automata},
BOOKTITLE = {Proceedings of the Workshop on Tools and Algorithms for the Construction and Analysis of Systems},
YEAR = {1995},
MONTH = {May},
ABSTRACT = {We propose a combination of model checking and interactive
theorem proving where the theorem prover is used to represent
finite and infinite state systems, reason about them
compositionally
and reduce them to small finite systems by verified abstractions. As an example
we verify a version of the Alternating Bit Protocol with
unbounded lossy and duplicating channels: the channels
are abstracted by interactive proof and the resulting finite state system is
model checked. },
PS = {MullerN95.ps.gz}
}
@INPROCEEDINGS{McMillanQS00,
AUTHOR = {Kenneth L. McMillan and Shaz Qadeer and James B. Saxe},
TITLE = {Induction in Compositional Model Checking},
BOOKTITLE = {Twelfth {I}nternational {C}onference on
{C}omputer {A}ided {V}erification ({CAV} 2000)},
YEAR = {2000},
NOTE = {To Appear},
PS = {McMillanQS00.ps.gz}
}
@ARTICLE{MokkedemHJG00,
AUTHOR = {Abdel Mokkedem and Ravi Hosabettu and Michael D. Jones and Ganesh Gopalakrishnan},
TITLE = {Formalization and {A}nalysis of a {S}olution to the {PCI}
2.1 {B}us {T}ransaction {O}rdering {P}roblem},
JOURNAL = {Formal Methods in System Design},
YEAR = {2000},
OPTKEY = {},
VOLUME = {16},
NUMBER = {1},
PAGES = {93--119},
MONTH = {January},
PS = {MokkedemHJG00.ps.gz},
OPTNOTE = {},
OPTANNOTE = {}
}
@ARTICLE{SinnottT95,
TITLE = {Applying Formal Methods to Standard Development: {The}
{Open Distributed Processing} Experience},
AUTHOR = {Richard O. Sinnott and Kenneth J. Turner},
MONTH = {October},
YEAR = 1995,
JOURNAL = {Computer Standards and Interfaces},
VOLUME = 17,
PAGES = {615--630},
CVCP = 11,
HEFC = 07,
PS = {SinnottT95.ps.gz}
}
@INPROCEEDINGS{CypherLMPS98,
AUTHOR = {D. Cypher and D. Lee and M. Martin-Villalba and C. Prins and D. Su},
TITLE = {Formal {S}pecification, {V}erification, and {A}utomatic {T}est
{G}eneration of {ATM} {R}outing {P}rotocol: {PNNI} },
BOOKTITLE = {{F}ormal {D}escription {T}echniques & {P}rotocol {S}pecification, {T}esting, and {V}erification ({FORTE/PSTV}) {IFIP}},
OPTCROSSREF = {},
OPTKEY = {},
YEAR = {1998},
OPTEDITOR = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTSERIES = {},
OPTADDRESS = {},
MONTH = {November},
OPTORGANIZATION = {},
OPTPUBLISHER = {},
OPTNOTE = {},
OPTANNOTE = {},
PDF = {CypherLMPS98.pdf}
}
@ARTICLE{MurthyG96,
TITLE = {A {R}outing {P}rotocol for {W}ireless {N}etworks},
AUTHOR = {Shree Murthy and J.J.Garcia-Luna-Aceves},
MONTH = {October},
YEAR = 1996,
JOURNAL = {Mobile {N}etworks and {N}omadic {A}pplications ({NOMAD})},
NOTE = {Special Issue on Routing in Mobile
Communication Network},
ABSTRACT = {We present the Wireless Routing Protocol (WRP). In WRP, routing
nodes communicate the
distance and second-to-last hop for each destination. WRP reduces the
number of cases in
which a temporary routing loop can occur, which accounts for its fast
convergence
properties. A detailed proof of correctness is presented and its
performance is compared by
simulation with the performance of the distributed Bellman-Ford
Algorithm (DBF), DUAL (a
loop-free distance-vector algorithm) and an Ideal Link-state
Algorithm (ILS), which represent
the state of the art of internet routing. The simulation results
indicate that WRP is the most
efficient of the alternatives analyzed.},
PS = {MurthyG96.ps.gz}
}
@INPROCEEDINGS{GarciaM95,
AUTHOR = {J.J. Garcia-Luna-Aceves and Shree Murthy},
TITLE = {A {L}oop-{F}ree {P}ath-{F}inding {A}lgorithm: {S}pecification,
{V}erification and {C}omplexity},
BOOKTITLE = {Proceedings of {IEEE} {INFOCOM} '95},
OPTCROSSREF = {},
OPTKEY = {},
YEAR = {1995},
OPTEDITOR = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTSERIES = {},
OPTADDRESS = {},
MONTH = {April},
OPTORGANIZATION = {},
OPTPUBLISHER = {},
OPTNOTE = {},
OPTANNOTE = {},
PS = {GarciaM95.ps.gz}
}
@INPROCEEDINGS{Smith96,
AUTHOR = {Mark A. Smith},
TITLE = {Formal verification of {C}ommunication {P}rotocols},
BOOKTITLE = {{F}ormal {D}escription {T}echniques & {P}rotocol {S}pecification, {T}esting, and {V}erification ({FORTE/PSTV}) {IFIP}},
OPTCROSSREF = {},
OPTKEY = {},
PAGES = {129--144},
YEAR = {1996},
OPTEDITOR = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTSERIES = {},
OPTADDRESS = {},
MONTH = {October},
OPTORGANIZATION = {},
OPTPUBLISHER = {},
OPTNOTE = {},
OPTANNOTE = {},
PS = {Smith96.ps.gz}
}
@INPROCEEDINGS{CallahanM96,
AUTHOR = {J. R. Callahan and T. L. Montgomery},
TITLE = {An {A}pproach to {V}erification and {V}alidation of a
{R}eliable
{M}ulticasting {P}rotocol},
BOOKTITLE = {International {S}ymposium on {S}oftware {T}esting and {A}nalysis ({ISSTA}'96)},
YEAR = {1996},
MONTH = {January},
ABSTRACT = {This paper describes the process of implementing a
complex communications protocol that provides reliable
delivery of data in multicast-capable, packet-switching
telecommunication networks. The protocol, called the
Reliable Multicasting Protocol (RMP), was developed
incrementally using a combination of formal and informal
techniques in an attempt to ensure the correctness of its
implementation. Our development process involved three
concurrent activities: (1) the initial construction and
incremental enhancement of a formal state model of the
protocol machine; (2) the initial coding and incremental
enhancement of the implementation; and (3) model-based
testing of iterative implementations of the protocol.
These activities were carried out by two separate teams:
a design team and a V&V team. The design team built
the first version of RMP with limited functionality to
handle only nominal requirements of data delivery. This
initial version did not handle off-nominal cases such as
network partitions or site failures. Meanwhile, the
V&V team concurrently developed a formal model of the
requirements using a variant of SCR-based state tables.
Based on these requirements tables, the V&V team
developed test cases to exercise the implementation. In a
series of iterative steps, the design team added new
functionality to the implementation while the V&V
team kept the state model in fidelity with the
implementation. This was done by generating test cases
based on suspected errant or off-nominal behaviors
predicted by the current model. If the execution of a
test in the model and implementation agreed, then the
test either found a potential problem or verified a
required behavior. However, if the execution of a test
was different in the model and implementation, then the
differences helped identify inconsistencies between the
model and implementation. In either case, the dialogue
between both teams drove the co-evolution of the model
and implementation. We have found that this interactive,
iterative approach to development allows software
designers to focus on delivery of nominal functionality
while the V&V team can focus on analysis of
off-nominal cases. Testing serves as the vehicle for
keeping the model and implementation in fidelity with
each other. This paper describes (1) our experiences in
developing our process model; and (2) three example
problems found during the development of RMP. Although
RMP has provided our research effort with a rich set of
test cases, it also has practical applications within
NASA. For example, RMP is being considered for use in the
NASA EOSDIS project due to its significant performance
benefits in applications that need to replicate large
amounts of data to many network sites. The RMP source
code and documentation are currently available on the WWW
via},
PS = {CallahanM96.ps.gz}
}
@INPROCEEDINGS{NagasamyRP95,
AUTHOR = {Vijay Nagasamy and Sreeranga Rajan and Preeti R. Panda},
TITLE = {Fibre channel protocol: {F}ormal specification and verification},
BOOKTITLE = {Sixth Annual Silicon Valley Networking Conference. SysTech Research},
YEAR = {1995},
MONTH = {April},
PS = {NagasamyRP95.ps.gz}
}
@INPROCEEDINGS{MokkedemHG98,
AUTHOR = {Abdel Mokkedem and Ravi Hosabettu and Ganesh Gopalakrishnan},
TITLE = {Formalization and {P}roof of a {S}olution to the {PCI} 2.1 {B}us {T}ransaction {O}rdering {P}roblem},
BOOKTITLE = {Formal methods in computer aided design: second internaitonal conference, FMCAD '98, Palo Alto, CA, USA},
OPTCROSSREF = {},
OPTKEY = {},
OPTPAGES = {},
YEAR = {1998},
EDITOR = {Ganesh Gopalakrishnan and Phillip Windley},
OPTVOLUME = {},
OPTNUMBER = {},
OPTSERIES = {},
OPTADDRESS = {},
MONTH = {November},
OPTORGANIZATION = {},
OPTPUBLISHER = {},
OPTNOTE = {},
OPTANNOTE = {},
PS = {MokkedemHG98.ps.gz}
}
@INPROCEEDINGS{DuMNRS97,
AUTHOR = {X. Du and K.T. McDonnell and E. Nanos and Y.S. Ramakrishna and S.A. Smolka},
TITLE = {Software {D}esign, {S}pecification, and {V}erification: {L}essons Learned from the {R}ether Case Study},
BOOKTITLE = {Proceedings of the {S}ixth {I}nternational {C}onference on {A}lgebraic {M}ethodology and {S}oftware {T}echnology (AMAST'97), {S}ydney, {A}ustralia},
OPTCROSSREF = {},
OPTKEY = {},
OPTPAGES = {},
YEAR = {1997},
OPTEDITOR = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTSERIES = {},
OPTADDRESS = {},
MONTH = {December},
OPTORGANIZATION = {},
OPTPUBLISHER = {},
OPTNOTE = {},
OPTANNOTE = {},
PS = {DuMNRS97.ps.gz}
}
@ARTICLE{DuSC99,
AUTHOR = {X. Du and S.A. Smolka and R. Cleaveland},
TITLE = {Local Model Checking and Protocol Analysis},
JOURNAL = {Software {T}ools for {T}echnology {T}ransfer},
YEAR = {1999},
OPTKEY = {},
VOLUME = {2},
NUMBER = {3},
PAGES = {219--241},
MONTH = {November},
PS = {DuSC99.ps.gz},
OPTANNOTE = {}
}
@INPROCEEDINGS{CallahanS96,
AUTHOR = {J. Callahan and F. Schneide},
TITLE = {Specification-Based Testing using Model Checking},
BOOKTITLE = {1996 SPIN Workshop, Rutgers University},
OPTCROSSREF = {},
OPTKEY = {},
OPTPAGES = {},
YEAR = {1996},
OPTEDITOR = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTSERIES = {},
OPTADDRESS = {},
MONTH = {August},
OPTORGANIZATION = {},
OPTPUBLISHER = {},
ABSTRACT = {White-box testing allows developers to determine
whether or not a program is partially consistent with its
specified behavior and design through the examination of
intermediate values of variables during program
execution. These intermediate values are often recorded
as an execution trace produced by monitoring code
inserted into the program. After program execution, the
values in an execution trace are compared to values
predicted by the specified behavior and design.
Inconsistencies between predicted and actual values can
lead to the discovery of errors in the specification and
its implementation. This paper describes an approach to
(1) verify the execution traces created by monitoring
statements during white-box testing using a model checker
as a semantic tableau; (2) organize multiple execution
traces into distinct equivalence partitions based on
requirements specifications written in linear temporal
logic (LTL); and (3) use the counter-example generation
mechanisms found in most model-checker tools to generate
new test cases for unpopulated equivalence partitions.},
PS = {CallahanS96.ps.gz},
OPTNOTE = {},
OPTANNOTE = {}
}
@MISC{CallahanEM98,
AUTHOR = {John R. Callahan and Stephen M. Easterbrook and Todd
L. Montgomery},
TITLE = {Generating Test Oracles via Model Checking},
YEAR = {1998},
NOTE = {Unpublished, working paper.
Available at
\url{http://research.ivv.nasa.gov/projects/blurbs/FormalTesting.html}},
PDF = {CallahanEM98.pdf.gz}
}
@TECHREPORT{YuEG00,
AUTHOR = {Yan Yu and Deborah Estrin and Sandeep Gupta},
TITLE = {Worst Case Performance Analysis of Wireless Ad-hoc Routing
Protocols: Case Studies},
INSTITUTION = {USC},
YEAR = 2000,
NUMBER = {00-730},
NOTE = {Submitted for Publication},
PS = {YuEG00.ps.gz}
}
@INPROCEEDINGS{HelmyEG98,
AUTHOR = {Ahmed Helmy and Deborah Estrin and Sandep Gupta},
TITLE = {Fault-oriented {T}est {G}eneration for {M}ulticast {R}outing {P}rotocol {D}esign},
BOOKTITLE = {{F}ormal {D}escription {T}echniques & {P}rotocol {S}pecification, {T}esting, and {V}erification ({FORTE/PSTV}) {IFIP}},
OPTCROSSREF = {},
OPTKEY = {},
OPTPAGES = {},
YEAR = {1998},
OPTEDITOR = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTSERIES = {},
OPTADDRESS = {},
MONTH = {November},
OPTORGANIZATION = {},
OPTPUBLISHER = {},
OPTNOTE = {},
OPTANNOTE = {},
PS = {HelmyEG98.ps.gz}
}
@INPROCEEDINGS{HelmyE98,
AUTHOR = {Ahmed Helmy and Deborah Estrin},
TITLE = {Simulation-based `{STRESS}' {T}esting {C}ase {S}tudy},
BOOKTITLE = {Sixth {I}nternational {S}ymposium on {M}odeling, {A}nalysis and {S}imulation of {C}omputer and {T}elecommunication {S}ystems (MASCOTS)},
OPTCROSSREF = {},
OPTKEY = {},
OPTPAGES = {},
YEAR = {1998},
OPTEDITOR = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTSERIES = {},
OPTADDRESS = {},
MONTH = {July},
OPTORGANIZATION = {},
OPTPUBLISHER = {},
OPTNOTE = {},
OPTANNOTE = {},
PS = {HelmyE98.ps.gz}
}
@INPROCEEDINGS{HickeyLR99,
AUTHOR = {Jason Hickey and Nancy Lynch and Robbert van Renesse},
TITLE = {Specifications and Proofs for Ensemble Layers
},
BOOKTITLE = {Proceedings of TACAS'99},
OPTCROSSREF = {},
OPTKEY = {},
OPTPAGES = {},
YEAR = {1999},
PS = HICKEYLR99.PS,
OPTEDITOR = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTSERIES = {},
OPTADDRESS = {},
MONTH = {MAy},
OPTORGANIZATION = {},
PUBLISHER = {Springer},
OPTNOTE = {},
OPTANNOTE = {}
}
@INPROCEEDINGS{LiuRBKC01,
AUTHOR = {Xiaoming Liu and Robbert van Renesse and Mark Bickford and Christoph Kreitz and Robert Constable},
TITLE = {Protocol Switching: Exploiting Meta Properties
},
BOOKTITLE = {Proceedings of International Workshop on Applied Reliable Group Communication},
OPTCROSSREF = {},
OPTKEY = {},
OPTPAGES = {},
YEAR = {2001},
PS = LIURBKC01.PS,
OPTEDITOR = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTSERIES = {},
OPTADDRESS = {},
OPTMONTH = {},
OPTORGANIZATION = {},
OPTPUBLISHER = {},
OPTNOTE = {},
OPTANNOTE = {}
}
@TECHREPORT{Axelsson99,
AUTHOR = {Stefan Axelsson},
TITLE = {Research in Intrusion-Detection Systems: A Survey},
INSTITUTION = {Chalmers University of Technology},
YEAR = {1999},
PDF = AXELSSON99.PDF,
OPTKEY = {},
OPTTYPE = {},
OPTNUMBER = {},
OPTADDRESS = {},
OPTMONTH = {},
OPTNOTE = {},
OPTANNOTE = {}
}
@TECHREPORT{PtacekN98,
AUTHOR = {Thomas H. Ptacek and Timothy N. Newsham},
TITLE = {Insertion, Evasion and Denial of Service: Eluding Network Intrusion Detection},
INSTITUTION = {Secure Networks, Inc.},
YEAR = {1998},
PDF = PTACEKN98.PDF,
OPTKEY = {},
OPTTYPE = {},
OPTNUMBER = {},
OPTADDRESS = {},
OPTMONTH = {},
OPTNOTE = {},
OPTANNOTE = {}
}
@TECHREPORT{Kvarnstrom99,
AUTHOR = {Hakan Kvarnstrom},
TITLE = {A survey of commercial tools for Intrusion Detection},
INSTITUTION = {Chalmers University of Technology},
YEAR = {1999},
PDF = KVARNSTROM99.PDF,
OPTKEY = {},
OPTTYPE = {},
OPTNUMBER = {},
OPTADDRESS = {},
OPTMONTH = {},
OPTNOTE = {},
OPTANNOTE = {}
}