@COMMENT{{{This file has been generated by bib2bib 1.75}}
@COMMENT{{{Command line: bib2bib -oc sens-citations.txt -ob sens-pubs.bib -c 'author : "Cheng" or author : "Dillon" or author : "Kulkarni" or author : "McKinley" or author : "Shapiro" or author : "Stirewalt"' allbib.bib betty-direct.bib kurt-pubs2.bib LthruR.bib rapidware-pubs.bib AthruD.bib EthruK.bib laurie-pubs.bib phil-pubs.bib SthruZ.bib}}
@INPROCEEDINGS{Turner-HPC,
AUTHOR = {Stephen W.~Turner and Lionel M.~Ni and Betty H.C.~Cheng},
TITLE = {A Scheduling Facility for Network of Workstations},
BOOKTITLE = {Proc. of High Performance Computing-Asia},
KEY = {HPC,PP},
EDITOR = {},
YEAR = {1995},
MONTH = {September},
COMMENT = {Don't have final copy from proceedings.}
}
@MISC{FMSDNotes,
AUTHOR = {Betty H.C. Cheng and Others},
TITLE = {Lecture Notes for Formal Methods For Software
Development (CPS814)},
HOWPUBLISHED = {Online classnotes},
YEAR = {1995},
MONTH = {},
NOTE = {Available on web (http://www.cps.msu.edu/~cps814/classnotes.html)}
}
@TECHREPORT{Che87,
AUTHOR = {Betty H.~C. Cheng},
TITLE = {SEED : A Semantic Editor},
INSTITUTION = {University of Illinois at Urbana-Champaign},
NUMBER = {UIUCDCS-R-87-1341},
ADDRESS = {Champaign-Urbana, IL},
MONTH = {May},
YEAR = {1987},
NOTE = {Master's Thesis},
KEY = {WP}
}
@INPROCEEDINGS{Che89a,
AUTHOR = {Betty Cheng and Simon Kaplan},
TITLE = {A Semantically Oriented Program Synthesis System},
BOOKTITLE = {Hawaii International Conference on System Sciences-22},
YEAR = {1989},
PAGES = {85--94},
KEY = {WP}
}
@UNPUBLISHED{Che89c,
AUTHOR = {Betty H. C. Cheng},
TITLE = {Synthesis of Procedural and Data Abstractions},
NOTE = {Preliminary Report of Investigations},
YEAR = {1989},
MONTH = {July},
KEY = {WP}
}
@UNPUBLISHED{Che89b,
AUTHOR = {Betty Cheng and Simon Kaplan},
TITLE = {Update of SEED},
YEAR = {1989},
NOTE = {submitted to Computer},
KEY = {WP}
}
@INPROCEEDINGS{Compsac91,
AUTHOR = {Betty H.~C. Cheng},
TITLE = {Synthesis of {P}rocedural {A}bstractions from {F}ormal
{S}pecifications},
BOOKTITLE = {Proc. of COMPSAC'91},
BOOKTITLELONG = {Proc. of IEEE COMPSAC'91: Computer Software and
Applications Conference},
YEAR = {1991},
PAGES = {149--154},
BHCORGANIZATION = {IEEE Computer Society and Information
Processing Society of Japan},
BHCADDRESS = {Tokyo, Japan},
MONTH = {September},
KEY = {WP,PRG,FORMAL}
}
@INPROCEEDINGS{Cheng91-adt,
AUTHOR = {Betty H.~C. Cheng},
TITLE = {Automated {S}ynthesis of {D}ata {A}bstractions},
BOOKTITLE = {Proc. of Irvine Software Symposium},
YEAR = {1991},
PAGES = {161-176},
BC-ORGANIZATION = {The Irvine Research Unit in Software},
BC-ADDRESS = {University of California, Irvine},
MONTH = {June},
KEY = {FORMAL,WP}
}
@INPROCEEDINGS{FM-Panel,
AUTHOR = {Betty H.~C.~Cheng and David Gries and Mark A. Ardis
and Kwei-Jay Lin and Natarajan~Shankar and Joseph
E.~Urban and Horst F.~Wedde},
TITLE = {Are Formal Methods Useful for Software Development},
BOOKTITLE = {Proc. of the 16th Annual International Computer Software and
Applications Conference},
YEAR = {1992},
MONTH = {September},
PAGES = {2--9},
COMMENT = {FM panel organized by BHC and Wedde.}
}
@INPROCEEDINGS{Transparent-Debugging,
AUTHOR = {David F. Robinson and Betty H.~C. Cheng and Richard J. Enbody},
TITLE = {A Transparent Monitoring Tool for Shared-Memory
Multiprocessors},
BOOKTITLE = {Proc. of COMPSAC'92: Computer Software and
Applications Conference},
YEAR = {1992},
MONTH = {September},
PAGES = {227--232},
COMMENT = {SW-Based non-intrusive debugging}
}
@TECHREPORT{Temporal-Debugging-TR,
AUTHOR = {David F. Robinson and Betty H.~C. Cheng},
TITLE = {A Temporal Model for Transparent Monitoring of
Shared-Memory Multiprocessors},
INSTITUTION = {Department of Computer Science, Michigan
State University},
YEAR = {1992},
TYPE = {Technical Report},
NUMBER = {MSU-CPS-ACS-65},
ADDRESS = {East Lansing, Michigan 48824},
MONTH = {July},
KEY = {DEBUG,FM,SPEC}
}
@INPROCEEDINGS{Temporal-Debugging,
AUTHOR = {David F. Robinson and Betty H.~C. Cheng},
TITLE = {A Temporal Model for Transparent Monitoring of
Shared-Memory Multiprocessors},
BOOKTITLE = {COMPSAC'93},
YEAR = {1993},
ORGANIZATION = {IEEE},
PAGES = {388--394},
ADDRESS = {Phoenix, Arizona},
MONTH = {November},
KEY = {DEBUG,FM,SPEC}
}
@UNPUBLISHED{ILINE,
AUTHOR = {Stephen W. Turner and Betty H.~C. Cheng},
TITLE = {Formal {S}pecification of {W}eapon {T}arget
{A}ssignment {S}oftware},
YEAR = {1992},
MONTH = {January},
KEY = {PP,CRIT,FM,SPEC}
}
@INPROCEEDINGS{NC-Alloc-ICPP,
AUTHOR = {Stephen W.~Turner and Lionel M.~ Ni and Betty H.~C.~Cheng},
TITLE = {Contention {F}ree {2-D} {M}esh {C}luster {A}llocation
in {H}ypercubes},
BOOKTITLE = {Proc. of International Conference on Parallel Processing},
YEAR = {1993},
PAGES = {Vol. {II}, 125--129},
MONTH = {August},
COMMENT = {Extended version submitted to TPDS}
}
@ARTICLE{NC-Alloc-TC,
AUTHOR = {Stephen W.~Turner and Lionel M.~ Ni and Betty H.~C.~Cheng},
TITLE = {Contention {F}ree {2-D} {M}esh {C}luster {A}llocation
in {H}ypercubes},
JOURNAL = {Trans. on Computers},
VOLUME = {44},
NUMBER = {8},
MONTH = {August},
YEAR = {1995},
NOTE = {Extended version of ICPP paper.}
}
@INPROCEEDINGS{TimeSpaceSharing-Super94,
AUTHOR = {S.~W.~Turner and L.~M.~Ni and B.~H.~C.~Cheng},
TITLE = {Time and/or Space Sharing in a Workstation Cluster Environment},
BOOKTITLE = {Proc. of Supercomputing'94},
YEAR = {1994},
MONTH = {November}
}
@INPROCEEDINGS{AllPort,
AUTHOR = {D.~F.~Robinson and D.~Judd and P.~K.~McKinley and
B.~H.~C.~Cheng},
TITLE = {Efficient Collective Data Distribution in All-Port
Wormhole-Routed Hypercubes},
BOOKTITLE = {Supercomputing'93},
YEAR = {1993},
PAGES = {792--803},
MONTH = {November},
COMMENT = {Full version submitted to JPDC, 12/93}
}
@ARTICLE{AllPort-JPDC,
AUTHOR = {D.~F.~Robinson and D.~Judd and P.~K.~McKinley and
B.~H.~C.~Cheng},
TITLE = {Efficient Collective Data Distribution in All-Port
Wormhole-Routed Hypercubes},
JOURNAL = {Journal of Parallel and Distributed Computing},
YEAR = {1995},
VOLUME = {31},
NUMBER = {1},
PAGES = {1029--1042},
MONTH = {November},
COMMENT = {Extended version of Supercomputing'93 paper}
}
@INPROCEEDINGS{Torus-icpp94,
AUTHOR = {D.~F.~Robinson and P.~K.~McKinley and B.~H.~C.~Cheng},
TITLE = {Optimal Multicast Communication in Torus Networks},
BOOKTITLE = {Proc. of International Conference on Parallel Processing},
YEAR = {1994},
PAGES = {Vol.~I, 131--141},
MONTH = {August},
KEY = {MULTICAST}
}
@ARTICLE{Torus-TPDS,
AUTHOR = {D.~F.~Robinson and P.~K.~McKinley and B.~H.~C.~Cheng},
TITLE = {Optimal Multicast Communication in Torus Networks},
JOURNAL = {IEEE Trans. on Parallel and Distributed Systems},
YEAR = {1995},
VOLUME = {6},
NUMBER = {10},
MONTH = {October},
PAGES = {1029--1042},
KEY = {MULTICAST},
COMMENT = {extended version of ICPP paper}
}
@TECHREPORT{Gannod890,
AUTHOR = {Gerald C. Gannod and Betty H.~C. Cheng},
TITLE = {Formal {S}pecification and {D}evelopment of {A}uto{S}pec},
INSTITUTION = {Department of Computer Science,Michigan State University},
YEAR = {1991},
ADDRESS = {East Lansing, MI 48824},
MONTH = {December}
}
@INPROCEEDINGS{Autospec,
AUTHOR = {Betty H.~C. Cheng and Gerald C. Gannod},
TITLE = {Constructing Formal Specifications from Program Code},
BOOKTITLE = {Proc. of IEEE Third International
Conference on Tools in Artificial Intelligence},
YEAR = {1991},
PAGES = {125--128},
BC-ORGANIZATION = {IEEE Computer Society},
BC-ADDRESS = {San Jose, California},
MONTH = {November},
KEY = {PRG,FM}
}
@ARTICLE{Two-Phase,
AUTHOR = {Gerald C. Gannod and Betty H.~C. Cheng},
TITLE = {A Two-Phase Approach to Reverse Engineering using
Formal Methods},
JOURNAL = {Lecture Notes in Computer Science, Proc. of Formal
Methods in Programming and Their
Applications Conference},
YEAR = {1993},
VOLUME = {735},
PAGES = {335--348},
MONTH = {June},
PUBLISHER = {Springer-Verlag},
COMMENT = {Russian conference with Broy and Cliff Jones on prog.
comm.},
COMMENT2 = {The proceedings will appear as part of the series of
Lecture Notes in Computer Science (LNCS) published by
Springer-Verlag.},
KEY = {FM,REV,OO}
}
@TECHREPORT{Prolog-Appl,
AUTHOR = {Betty H.~C. Cheng and Gerald C. Gannod},
TITLE = {Using {P}rolog to {D}evelop {T}ools {S}upporting
{F}ormal {M}ethods in {S}oftware {D}evelopment},
INSTITUTION = {Department of Computer Science, Michigan State University},
COMMENT = {submitted to First International Conference on the
Practical Application of Prolog},
YEAR = {1992},
ADDRESS = {A714 Wells Hall},
NUMBER = {MSU-CPS-92-02},
KEY = {PRG,FM,PROLOG}
}
@ARTICLE{Autospec-SEKE,
AUTHOR = {Gerald C.~Gannod and Betty H.~C.~Cheng},
TITLE = {Facilitating the Maintenance of Safety-Critical Systems},
JOURNAL = {Int.~J.~ of Software Engineering and
Knowledge Engineering},
YEAR = {1994},
VOLUME = {4},
NUMBER = {2},
PAGES = {183--204},
COMMENT = {Summary of autospec, plus new things for procedures
and scope of variables.}
}
@INPROCEEDINGS{StrongPost,
AUTHOR = {Gerald C.~Gannod and Betty H.~C.~Cheng},
TITLE = {Strongest Postcondition as the Basis to Reverse Engineering},
BOOKTITLE = {Proc. of IEEE Working Conference on Reverse Engineering},
YEAR = {1995},
PAGES = {188--197},
ADDRESS = {Toronto, Ontario},
MONTH = {July},
COMMENT = {First paper on using SP for reverse engineering.}
}
@ARTICLE{StrongPost-JASE,
AUTHOR = {Gerald C. Gannod and Betty H.~C.~Cheng},
TITLE = {Strongest Postcondition Semantics for Reverse Engineering},
JOURNAL = {Journal of Automated Software Engineering},
YEAR = {1996},
KEY = {REV},
VOLUME = {3},
NUMBER = {1/2},
MONTH = {June},
PAGES = {139--164},
COMMENT = {WCRE paper in journal form.},
NOTE = {A preliminary version appeared in the {\it Proc. of IEEE
Working Conference on Reverse Engineering}, July
1995, Toronto, Canada.}
}
@INPROCEEDINGS{StrongPost-Appl,
AUTHOR = {Gerald C.~Gannod and Betty H.~C.~Cheng},
TITLE = {Integration of Informal and Formal Methods for
Reverse Engineering of {C} Programs},
BOOKTITLE = {Proc. of IEEE International Conference on Software Maintenance},
YEAR = {1996},
OPTPAGES = {},
ADDRESS = {Monterey Bay, California},
MONTH = {November},
COMMENT = {SP semantics applied to MGSO project.}
}
@INPROCEEDINGS{ASE97-Pointers,
AUTHOR = {Gerald C. Gannod and Betty H.~C.~Cheng},
TITLE = {A Formal Automated Approach for Reverse Engineering
Programs with Pointers},
BOOKTITLE = {Proc. IEEE of Automated Software Engineering Conference},
YEAR = {1997},
ADDRESS = {Lake Tahoe, Nevada},
MONTH = {November},
ANNOTE = {Strong Post for pointers}
}
@INPROCEEDINGS{ASE98-RevReuse,
AUTHOR = {Gerald C. Gannod and Yonghao Chen and Betty H.~C.~Cheng},
TITLE = {An Automated Approach for Supporting Software Reuse
via Reverse Engineering},
BOOKTITLE = {Proc. IEEE of Automated Software Engineering Conference},
YEAR = {1998},
ADDRESS = {Honolulu, Hawaii},
MONTH = {October},
ANNOTE = {Combined reverse engineering technique to support reuse}
}
@INPROCEEDINGS{Packrat,
AUTHOR = {Gerald C.~Gannod Mark Fagnani and Gora Sudindranath
and Betty H.~C.~Cheng},
TITLE = {Packrat: A Software Re-engineering Case Study},
BOOKTITLE = {Proc. of IEEE Working Conference on Reverse Engineering},
YEAR = {1998},
ADDRESS = {Honolulu, Hawaii},
MONTH = {October},
COMMENT = {Capstone project for TI}
}
@TECHREPORT{MSU-CSE-00-30,
AUTHOR = {Gerald C. Gannod and Betty H.C. Cheng},
TITLE = {A Suite of Tools for Facilitating Reverse Engineering Using Formal Methods},
NUMBER = {MSU-CSE-00-30},
INSTITUTION = {Computer Science and Engineering, Michigan State University},
ADDRESS = {East Lansing, Michigan},
ABSTRACT = {As a program evolves, it becomes increasingly difficult to understand and reason about changes in
source code. Eventually, if enough changes are made without a corresponding modification of the software
documentation, reverse engineering and design recovery techniques must be used in order to understand the current
behavior of a system. In our previous investigations, we described a formal technique for reverse engineering. One of the
benefits of formal techniques is that they are amenable to automated processing. In this paper we describe an integrated
suite of tools that we have developed to support reverse engineering and analysis of C programs. },
KEYWORDS = {reverse engineering, formal methods, program analysis},
NOTE = {},
MONTH = {December},
YEAR = {2000},
AUTHOR1_URL = {http://www.public.asu.edu/~gannod},
AUTHOR1_EMAIL = {gannod@asu.edu},
AUTHOR2_URL = {http://www.cse.msu.edu/~chengb},
AUTHOR2_EMAIL = {chengb@cse.msu.edu},
PAGES = {},
FILE = {},
URL = {},
CONTACT = {chengb@cse.msu.edu}
}
@INPROCEEDINGS{Shuttle-SEL,
AUTHOR = {Betty H.~C.~Cheng and Brent Auernheimer},
TITLE = {Applying Formal Methods and Object-Oriented Analysis to
Existing Flight Systems},
BOOKTITLE = {Proc. of 18th Annual Software Engineering Workshop},
YEAR = {1993},
ORGANIZATION = {NASA/Goddard Space Flight Center, Software
Engineering Laboratory},
MONTH = {December},
PAGES = {274--282},
COMMENT = {Summary of summer at JPL}
}
@TECHREPORT{Shuttle-TR,
AUTHOR = {Betty H.~C.~Cheng and Brent Auernheimer},
TITLE = {Applying {F}ormal {M}ethods and {O}bject-{O}riented {A}nalysis
to the {E}xisting {S}pace {S}huttle {S}oftware},
INSTITUTION = {Michigan State University},
YEAR = {1994},
TYPE = {Technical Report},
NUMBER = {CPS-94-9},
ADDRESS = {Department of Computer Science, A714 Wells Hall, East
Lansing, Michigan 48824},
MONTH = {February},
COMMENT = {shorter version submitted to Special Issue of IEEE
Software on Legacy Systems},
NOTE1 = {(submitted to {\it IEEE Software}.)}
}
@TECHREPORT{LB-Browser-Techreport,
AUTHOR = {Michael R. Laux and Robert H. Bourdeau and Betty H.~C. Cheng},
TITLE = {An Integrated Environment Supporting the Reuse of
Formal Specifications},
INSTITUTION = {Michigan State University},
YEAR = {1992},
TYPE = {Technical Report},
NUMBER = {MSU-CPS-ACS-70},
ADDRESS = {Department of Computer Science, East Lansing,
Michigan 48824},
MONTH = {September},
NOTE = {submitted for publication},
NOTE2 = {submitted to International Conference on Software
Engineering},
COMMENT = {Browser for Larch LSL specifications}
}
@INPROCEEDINGS{LB-Browser,
AUTHOR = {Michael R. Laux and Robert H. Bourdeau and Betty H.~C. Cheng},
TITLE = {An Integrated Development Environment for Formal
Specifications},
BOOKTITLE = {Proc. of International Conference on Software
Engineering and Knowledge Engineering},
YEAR = {1993},
PAGES = {681--688},
BHC-ORGANIZATION = {IEEE Computer Society},
ADDRESS = {San Francisco, California},
MONTH = {July},
COMMENT = {First LB Browser paper, rewrite of ICSE paper},
KEY = {FM,SPEC,LARCH}
}
@TECHREPORT{LDE-TR,
AUTHOR = {Michele Morin and Betty H.~C.~Cheng},
TITLE = {Graphical {D}evelopment {E}nvironment for {Larch Shared and
Interface Languages}},
INSTITUTION = {Michigan State University},
YEAR = {1994},
TYPE = {Technical Report},
NUMBER = {CPS-94-18},
ADDRESS = {Department of Computer Science, A714 Wells Hall, East
Lansing, MI 48824-1027},
MONTH = {April},
COMMENT = {will be an extension of LBE paper with discussions
about LCL and LCCL}
}
@MANUAL{LDE-Manual,
TITLE = {User Manual for Larch Development Environment},
AUTHOR = {Michele Morin and Betty H.~C.~Cheng},
ORGANIZATION = {Michigan State University},
YEAR = {1994},
ADDRESS = {Department of Computer Science, A714 Wells Hall, East
Lansing, MI 48824-1027},
MONTH = {April},
KEY = {SPEC,LARCH},
FILE = {LDE-Manual.ps.Z}
}
@MISC{OO-Decomp,
AUTHOR = {Robert H. Bourdeau and Betty H.~C. Cheng},
TITLE = {Decomposition of {F}ormal {S}pecifications for
{O}bject-{O}riented {S}oftware},
NOTE = {in preparation},
YEAR = {1993},
KEY = {FORMAL,WP,SPEC}
}
@INPROCEEDINGS{Spectacle,
AUTHOR = {Robert H. Bourdeau and Betty H.~C. Cheng},
TITLE = {An Object-Oriented Toolkit for Constructing
Specification Editors},
BOOKTITLE = {Proceedings of COMPSAC'92: Computer Software and
Applications Conference},
YEAR = {1992},
MONTH = {September},
PAGES = {239--244},
KEY = {FORMAL,SPEC}
}
@TECHREPORT{OMT-FM-object,
AUTHOR = {Robert H. Bourdeau and Betty H.~C. Cheng},
TITLE = {Formal Software Specifications through Pictures},
INSTITUTION = {Department of Computer Science, Michigan
State University},
YEAR = {1993},
TYPE = {Technical Report},
NUMBER = {MSU-CPS-93-16},
ADDRESS = {A714 Wells Hall, East Lansing, 48824},
MONTH = {June},
COMMENT = {Preliminary Object and DFD formalization. Submitted
to special issue of IEEE Software on Safety Critical
Systems},
KEY = {OO,OMT,SPEC,FM,REQ}
}
@TECHREPORT{LICS-OMT,
AUTHOR = {Robert H. Bourdeau and Betty H.~C. Cheng},
TITLE = {A Formal Semantics for the Integration of Object and
Dynamic Models},
INSTITUTION = {Department of Computer Science, Michigan
State University},
YEAR = {1993},
TYPE = {Technical Report},
NUMBER = {MSU-CPS-93-32},
ADDRESS = {A714 Wells Hall, East Lansing, 48824},
MONTH = {December},
NOTE = {(submitted for publication)},
COMMENT = {Extended abstract of OMT formalization and its
integration into state diagrams. Submitted
to LICS'94},
KEY = {OO,OMT,SPEC,FM,REQ}
}
@TECHREPORT{TSE-OMT-TR,
AUTHOR = {Robert H. Bourdeau and Betty H.~C. Cheng},
TITLE = {A Formal Semantics of Object Models},
INSTITUTION = {Department of Computer Science, Michigan
State University},
YEAR = {1994},
TYPE = {Technical Report},
NUMBER = {MSU-CPS-94-6},
ADDRESS = {A714 Wells Hall, East Lansing, 48824},
MONTH = {January},
NOTE = {(under review for {\it IEEE Trans. on Software Engineering}.)}
}
@ARTICLE{TSE-OMT,
AUTHOR = {Robert H. Bourdeau and Betty H.~C. Cheng},
TITLE = {A Formal Semantics of Object Models},
JOURNAL = {IEEE Trans. on Software Engineering},
YEAR = {1995},
VOLUME = {21},
NUMBER = {10},
PAGES = {799--821},
MONTH = {October},
COMMENT = {First paper on formalization of the object model.
Accepted in July 1995, with minor revisions.}
}
@TECHREPORT{VisSpecs-TR,
AUTHOR = {Betty H.~C.~Cheng and Enoch Y.~Wang and Robert H.~Bourdeau},
TITLE = {A Graphical Environment for Formally Developing
Object-Oriented Software},
INSTITUTION = {Department of Computer Science, Michigan
State University},
YEAR = {1994},
TYPE = {Technical Report},
NUMBER = {MSU-CPS-94-26},
ADDRESS = {A714 Wells Hall, East Lansing, 48824},
MONTH = {April},
COMMENT = {Short version in ICTAI94}
}
@INPROCEEDINGS{DynamicModel-ICSE,
AUTHOR = {Enoch Y. Wang and Heather A. Richter and Betty H.~C. Cheng},
TITLE = {Formalizing and Integrating the Dynamic Model within
{OMT}},
BOOKTITLE = {Proceedings of IEEE International Conference
on Software Engineering (ICSE97)},
YEAR = {1997},
ADDRESS = {Boston, MA},
MONTH = {May},
OPTPAGES = {},
OPTNOTE = {},
OPTANNOTE = {}
}
@ARTICLE{DynamicModel,
AUTHOR = {Betty H.~C. Cheng and Enoch Y. Wang},
TITLE = {Formalizing and Integrating the Dynamic Model for Object-Oriented Modeling},
JOURNAL = {IEEE Transactions on Software Engineering},
YEAR = {2002},
MONTH = {August},
VOLUME = {28},
NUMBER = {8},
PAGES = {747--762},
NOTE = {A shorter, preliminary version appeared in {\it Proc. of IEEE International Conference
on Software Engineering} (ICSE97).},
OPTANNOTE = {}
}
@TECHREPORT{OMT:Fx:TR,
AUTHOR = {Heather Richter and Betty H.~C. Cheng},
TITLE = {Formalizing and Integration the Functional Model within {OMT}},
INSTITUTION = {Department of Computer Science, Michigan
State University},
YEAR = {1995},
TYPE = {Technical Report},
NUMBER = {MSU-CPS-95-30},
ADDRESS = {A714 Wells Hall, East Lansing, 48824},
MONTH = {August},
NOTE = {(submitted for publication)}
}
@INPROCEEDINGS{SERF,
AUTHOR = {Betty H.C.~Cheng and Enoch Y. Wang and Robert
H. Bourdeau and Heather A. Richter},
TITLE = {Bridging the Gap Between the Informal and Formal
Approaches to Software Development},
BOOKTITLE = {Proceedings of Software Engineering Research Forum},
YEAR = {1995},
ADDRESS = {Boca Raton, Florida},
MONTH = {November}
}
@TECHREPORT{UML-VHDL,
AUTHOR = {William E. McUmber and Betty H.C. Cheng},
TITLE = {Integrating UML and VHDL},
INSTITUTION = {Michigan State University},
YEAR = {1998},
OPTKEY = {},
TYPE = {Draft research manuscript},
OPTNUMBER = {},
OPTADDRESS = {},
MONTH = {October},
NOTE = {(in progress)},
ANNOTE = {interested in the combination of model checking and
simulation for determining source of errors through counter-examples }
}
@INPROCEEDINGS{HASE99,
AUTHOR = {William E. McUmber and Betty {H.C.} Cheng},
TITLE = {{UML}-Based Analysis of Embedded Systems Using a
Mapping to {VHDL}},
BOOKTITLE = {Proceedings of IEEE High Assurance Software Engineering (HASE99)},
YEAR = {1999},
OPTORGANIZATION = {IEEE},
ADDRESS = {Washington, DC},
MONTH = {November},
ANNOTE = {First paper on UML to VHDL formalization}
}
@TECHREPORT{DynamicModel-TR,
AUTHOR = {Enoch Y. Wang and
Betty H.C. Cheng},
TITLE = {Formalizing and Integrating the Dynamic Model within OMT},
NUMBER = {MSU-CPS-96-13},
INSTITUTION = {Department of Computer Science, Michigan State University},
ADDRESS = {East Lansing, Michigan},
ABSTRACT = {The Object Modeling Technique (OMT), a commonly used
object-oriented development technique, comprises the object, dynamic,
and functional models to provide three complementary views that
graphically describe different aspects of systems. The lack of a well-defined
semantics for the integration of the three models hinders the
overall development process, particularly during the design phase.
Previously, we formalized the object model in terms of algebraic
specifications. However, the algebraic specifications only capture
the static, structural aspects of a system. It does not explicitly
describe the behavior, which is critical for system development,
especially for the design phase. It is necessary to formalize the
dynamic model in terms of the structural descriptions in order to
specify and verify the system behavior using rigorous techniques.
This paper presents a well-defined formal model for both the object
and dynamic models and their integration. The formal model is
described in terms of a well-known specification language,
LOTOS. Formalization of the graphical notation enables numerous
automated processing and analysis tasks, such as behavior simulation
and consistency checks between levels of specifications.
},
NOTE = {(revised August 1997)},
MONTH = {March},
YEAR = {1996},
AUTHOR1_URL = {},
AUTHOR1_EMAIL = {},
PAGES = {},
FILE = {},
URL = {},
CONTACT = {chengb@cps.msu.edu}
}
@TECHREPORT{FFR-techreport,
AUTHOR = {Enoch Y. Wang and Betty H.~C. Cheng},
TITLE = {Integrating the Functional Model into Object-Oriented Design},
NUMBER = {MSU-CPS-96-20},
INSTITUTION = {Department of Computer Science, Michigan State University},
ADDRESS = {East Lansing, Michigan},
ABSTRACT = {The data flow diagram (DFD) was first introduced in structured design
for representing data and the processes that transform data. A DFD
visually models a system in terms of input/output data flows and
processes, and it provides a means to systematically decompose a
system. Based on concepts such as modularity, abstraction,
encapsulation, and reuse, object-oriented development methods have
advantages over structured methods in modeling, maintenance, and
reuse. In order to capture the functional aspect of systems and
objects, many object-oriented approaches sought to incorporate DFDs
into their respective methods. Thus far, the inclusion of DFDs has
not been based on a well-defined integration. The main hindrance to
the integration is due to the conflicting development philosophies
underlying structured and object-oriented methods, particularly with
respect to their respective system decomposition strategies. The
structured approaches decompose systems according to functionality,
while the object-oriented approaches conduct decomposition according
to static object structure. This paper attempts to integrate DFDs
into object-oriented methods without violating the object-orientation
philosophy. The proposed approach modifies DFDs and introduces formal
semantics to functional models in terms of algebraic specifications.
The object-oriented development model of this research is based upon
the {\it Object Modeling Technique} (OMT). OMT includes
three complementary models: object model, functional model, and
dynamic model. The object models depicts the static structural aspect
of a system; the functional model describe the functionalities of a
system; and the dynamic model captures the dynamic behavior of a
system. The objective of the research is to formalize and integrate
the three models in terms of their underlying formal semantics, where
we have previously formalized the object model in terms of algebraic
specifications and the dynamic model in terms of process algebras.
The formalization of the functional model is defined in the
context of its integration with both the object and the dynamic
models.
},
KEYWORDS = {Object-oriented modeling, data flow diagrams, formal specification,
requirements analysis, design, model integration},
BHCNOTE = {completely revised version of functional model paper with Richter},
MONTH = {June},
YEAR = {1997},
AUTHOR1_URL = {},
AUTHOR1_EMAIL = {},
PAGES = {},
FILE = {},
URL = {}
}
@INPROCEEDINGS{FunctionalModel-Conf,
AUTHOR = {Enoch Y.~Wang and Betty H.~C.~Cheng},
TITLE = {Formalizing and Integrating the Functional Model into
Object-Oriented Design},
BOOKTITLE = {Proceedings of International
Conference on Software Engineering and Knowledge Engineering},
YEAR = {1998},
NOTE = {Selected as Best Paper},
OPTPAGES = {},
MONTH = {June},
COMMENT = {First published paper on functional model formalization},
KEY = {OMT,OO,SPEC}
}
@ARTICLE{FunctionalModel,
AUTHOR = {Enoch Y.~Wang and Betty H.~C.~Cheng},
TITLE = {Formalizing the Functional Model Within
Object-Oriented Design},
JOURNAL = {International Journal of Software Engineering and Knowledge Engineering},
VOLUME = {10},
NUMBER = {1},
PAGES = {5--30},
YEAR = {2000},
COMMENT = {synopsis of phd thesis},
KEY = {FORMAL,WP}
}
@TECHREPORT{ProcessModel-TR,
AUTHOR = {Enoch Y. Wang and Betty H.C. Cheng},
TITLE = {A Rigorous Object-Oriented Design Process},
NUMBER = {MSU-CPS-97-46},
INSTITUTION = {Department of Computer Science, Michigan State University},
ADDRESS = {East Lansing, Michigan},
ABSTRACT = {
Within the software development process, software design plays an
important role in realizing software requirements. A considerable
amount of effort has been expended in the area of software design
and design methods in the past three decades. However, unlike other
disciplines of engineering, such as mechanical engineering and
electronic engineering, the proposed software design methods rarely
incorporate mathematical rigor in order to facilitate precise
specification of requirements and design. This phenomenon can be
partly attributed to the fact that formal methods research has largely
focused on the development of formal notation and inference rules, and
the notation and the grammar of formal specification languages require
familiarity with discrete mathematics and symbolic logic that most
practicing software engineers, designers, and implementors do not
have.
The Object Modeling Technique (OMT), a commonly used object-oriented
development technique, comprises the object, dynamic, and functional
models that provide three complementary views of systems. However, the
lack of a well-defined semantics for the
individual models and their integration
hinders the overall development process, particularly during
the design phase. Previously, we have formalized the three models and
integrated their corresponding formal specifications in terms of the
underlying formal semantics.
In an attempt to formalize the OMT models,
including their integration, we found it necessary to identify a
concrete process for developing the graphical models. The
design process has also been developed in order to achieve mathematical rigor in
design specifications. By using the results of our OMT formalization
investigations, the proposed design process promotes
an iterative
approach that systematically applies formal methods during design.
The formal specifications enable designers to detect and eliminate
design flaws by using automated formal analysis during earlier
stages of software development. In addition, this
paper discusses the results of applying the
process to a distributed multimedia information and decision support
system.
},
KEYWORDS = {},
NOTE = {},
MONTH = {November},
YEAR = {97},
AUTHOR1_URL = {http://www.cps.msu.edu/~wangyi},
AUTHOR1_EMAIL = {wangyi@cps.msu.edu},
AUTHOR2_URL = {http://www.cps.msu.edu/~chengb},
AUTHOR2_EMAIL = {chengb@cps.msu.edu},
PAGES = {},
FILE = {},
URL = {},
BHC-NOTE = {submitted to ICSP5, process conference},
CONTACT = {chengb@cps.msu.edu}
}
@INPROCEEDINGS{ProcessModel,
AUTHOR = {Enoch Y.~Wang and Betty H.~C.~Cheng},
TITLE = {A Rigorous Object-Oriented Design Process},
BOOKTITLE = {Proceedings of International
Conference on Software Process},
YEAR = {1998},
OPTPAGES = {},
MONTH = {June},
ADDRESS = {Naperville, Illinois},
COMMENT = {First published paper on process model},
KEY = {OMT,OO,SPEC,PROCESS}
}
@TECHREPORT{AppProcessModel,
AUTHOR = {Enoch Y. Wang and Betty H.C. Cheng},
TITLE = {An Application of a Rigorous Design Process },
NUMBER = {MSU-CPS-98-6},
INSTITUTION = {Department of Computer Science, Michigan State University},
ADDRESS = {East Lansing, Michigan},
ABSTRACT = {},
KEYWORDS = {object-oriented analysis and design,software process, formal specifications},
NOTE = {},
MONTH = {February},
YEAR = {98},
AUTHOR1_URL = {http://www.cps.msu.edu/~wangyi},
AUTHOR1_EMAIL = {wangyi@cps.msu.edu},
AUTHOR2_URL = {http://www.cps.msu.edu/~chengb},
AUTHOR2_EMAIL = {chengb@cps.msu.edu},
PAGES = {41},
FILE = {},
URL = {},
CONTACT = {chengb@cps.msu.edu}
}
@TECHREPORT{casestudy,
AUTHOR = {Enoch Y. Wang and Betty H.C. Cheng},
TITLE = {An Application of a Rigorous Design Process },
NUMBER = {MSU-CPS-98-6},
INSTITUTION = {Department of Computer Science, Michigan State University},
ADDRESS = {East Lansing, Michigan},
ABSTRACT = {},
KEYWORDS = {object-oriented analysis and design,software process, formal
specifications},
NOTE = {},
MONTH = {February},
YEAR = {98},
AUTHOR1_URL = {www.cps.msu.edu/~wangyi},
AUTHOR1_EMAIL = {wangyi@cps.msu.edu},
AUTHOR2_URL = {www.cps.msu.edu/~chengb},
AUTHOR2_EMAIL = {chengb@cps.msu.edu},
PAGES = {41},
FILE = {},
URL = {},
CONTACT = {chengb@cps.msu.edu}
}
@INPROCEEDINGS{ICTAI94,
AUTHOR = {Betty H.~C.~Cheng and Enoch Y.~Wang and Robert H.~Bourdeau},
TITLE = {A Graphical Environment for Formally Developing
Object-Oriented Software},
BOOKTITLE = {Proceedings of IEEE 6th International
Conference on Tools with Artificial Intelligence},
YEAR = {1994},
OPTPAGES = {},
MONTH = {November},
COMMENT = {First published paper on VizSpecs -- cover object
models only.},
KEY = {OMT,OO,SPEC}
}
@TECHREPORT{IntegratedVisSpecs-TR,
AUTHOR = {Robert H.~Bourdeau and Enoch Y.~Wang and Betty H.~C.~Cheng},
TITLE = {An Integrated Approach to Developing Diagrams as
Formal Specifications},
INSTITUTION = {Michigan State University},
YEAR = {1994},
TYPE = {Technical Report},
NUMBER = {MSU-CPS-94-42},
ADDRESS = {Department of Computer Science, A714 Wells Hall, East
Lansing, Michigan 48824},
MONTH = {September},
NOTE = {(submitted for publication)}
}
@INCOLLECTION{CSDA99,
AUTHOR = {Betty H.C. Cheng},
TITLE = {Multiple Dimensions of Integrating Development Technology},
BOOKTITLE = {Computer Security, Dependability, and Assurance:
From Needs to Solutions},
EDITOR = {P. Ammann and B. Barnes and S. Jajodia and E. Sibley},
PUBLISHER = {IEEE Computer Society},
OPTPAGES = {71-82},
YEAR = {1999},
KEY = {OMT, Integration}
}
@INPROCEEDINGS{WIFT98-Panel,
AUTHOR = {Betty H.~C.~Cheng and Robert France},
TITLE = {A Discussion about Integrated Techniques},
BOOKTITLE = {Post-Proceedings. of IEEE International Workshop on
Industrial Strength Formal Specification Techniques (WIFT98)},
YEAR = {1999},
OPTPAGES = {},
MONTH = {April},
COMMENT = {First published paper on VizSpecs -- cover object
models only.},
KEY = {OMT,OO,SPEC,Integration}
}
@TECHREPORT{OMT-VHDL-TR,
AUTHOR = {Gretel V.L.~Coombs and Betty H.~C.~Cheng},
TITLE = {Translation of Object-Oriented Designs into VHDL},
INSTITUTION = {Michigan State University},
YEAR = {1998},
TYPE = {Technical Report},
NUMBER = {MSU-CPS-98-8},
ADDRESS = {Department of Computer Science, 3115 Engineering Bldg., East
Lansing, Michigan 48824},
MONTH = {February},
NOTE = {(submitted for publication)}
}
@TECHREPORT{Spectacle-tr,
AUTHOR = {Robert H. Bourdeau and Betty H.~C. Cheng},
TITLE = {An Object-Oriented Toolkit for Constructing
Specification Editors},
INSTITUTION = {Michigan State University, Department of Computer Science},
YEAR = {1992},
KEY = {FORMAL,SPEC}
}
@TECHREPORT{Mapping-TR,
AUTHOR = {William E. McUmber and Betty H.C. Cheng},
TITLE = {{UML}-Based Analysis of Embedded Systems Using a Mapping to {VHDL}},
NUMBER = {MSU-CPS-99-11},
INSTITUTION = {Department of Computer Science and Engineering, Michigan State University},
ADDRESS = {East Lansing, Michigan},
ABSTRACT = {Embedded systems are typically 10 to 100 times more common than their desktop
counterparts, residing in everything from engine
systems, to toasters, to autopilots. The software for embedded systems
is, in general, more difficult to write and debug because embedded
systems software usually involves time-dependent sections in difficult
to instrument situations.
Embedded systems usually must achieve
a higher level of robustness and reliability because they control
real-world physical processes or devices upon which we depend,
frequently, in a critical way. Consequently, methods for developing
and modeling embedded systems and rigorously verifying behavior before
committing to code, are increasingly important. Currently, much of the
embedded
systems industry use ad hoc approaches for developing embedded
systems, where many proceed directly from requirements in prose to
%Frequently, there are few, if any, intermediate
%steps between high-level, prose descriptions of requirements
%and code written in
the target implementation language, such as C.
A number of object-oriented techniques and notations have been
introduced, but recently, it appears that the
Unified Modeling Language (UML)
could be a notation broad enough in scope to represent a variety of
domains and gain widespread use.
Currently, however, UML is only a
notation, with no formal semantics attached to the individual
diagrams or is there a formally defined semantics for
the integration of the diagrams. Therefore, it
is not possible to apply rigorous automated analysis
to execute a UML model in order to test its behavior, short of writing
code and performing exhaustive testing.
In order to address this problem, we have developed a framework for
deriving VHDL specifications from the class and state diagrams
in order to capture the structure and the behavior of embedded systems. The
VHDL specifications enable us to perform behavior simulation of the
UML models.
},
KEYWORDS = {metamodel, homomorphism, formal specifications, object-oriented modeling
notations},
NOTE = {},
MONTH = {February},
YEAR = {99},
AUTHOR1_URL = {},
AUTHOR1_EMAIL = {bill@objectsr.com},
AUTHOR2_URL = {www.cse.msu.edu/~chengb},
AUTHOR2_EMAIL = {chengb@cse.msu.edu},
PAGES = {32},
FILE = {},
URL = {},
CONTACT = {chengb@cse.msu.edu}
}
@TECHREPORT{Analysis-TR,
AUTHOR = {Laura Campbell and Betty H.C. Cheng and Enoch Y. Wang},
TITLE = {Enabling Automated Analysis Through the Formalization of Object-Oriented Modeling
Diagrams},
NUMBER = {MSU-CPS-99-13},
INSTITUTION = {Department of Computer Science and Engineering, Michigan State University},
ADDRESS = {East Lansing, Michigan},
ABSTRACT = {As the impact of and demand for software increases, there
is more demand for
rigorous software development techniques that can be used by a typical
software engineer. Formal development techniques, such as model checking, have
received recognition recently mostly in the hardware community for
its ability to detect flaws in requirements and designs that have been
formally specified. In contrast,
there is a much larger community of software developers who are
either using or learning to use the numerous object-oriented modeling
techniques to facilitate software development.
Unfortunately, there is a perception that these two
types of development techniques have mutually exclusive user communities.
We have been developing integration techniques that enable developers
to graphically construct object-oriented models of system requirements
and designs then automatically generate formal specifications for
the diagrams. The formal specifications can then be analyzed using automated tec
hniques to check for numerous properties of the diagrams, including
inter- and intramodel consistency. In addition, the formal
specifications enable the developer to validate the behavior of
the system depicted by the object-oriented models without implementing
the system by using various simulation tools. This paper presents
a case study that illustrates how our formalization rules have been
applied to the object-oriented models of a distributed multimedia
decision support system designed to access and manipulate enviromental
science information. In addition, we describe how a number of tools
have been used to analyze the specifications in order to detect and
correct flaws in the diagrams and the original requirements.
},
KEYWORDS = {object-oriented modeling, formal specifications. automated analysis},
NOTE = {},
MONTH = {March},
YEAR = {99},
AUTHOR1_URL = {www.cse.msu.edu/~campb222},
AUTHOR1_EMAIL = {campb222@cse.msu.edu},
AUTHOR2_URL = {www.cse.msu.edu/~chengb},
AUTHOR2_EMAIL = {chengb@cse.msu.edu},
PAGES = {},
FILE = {},
URL = {},
CONTACT = {chengb@cse.msu.edu}
}
@INPROCEEDINGS{Homomorphism-ICSE01,
AUTHOR = {William E. McUmber and Betty H.~C. Cheng},
TITLE = {A Generic Framework for Formalizing {UML} with Formal
Languages},
BOOKTITLE = {Proceedings of IEEE International Conference
on Software Engineering (ICSE01)},
YEAR = {2001},
ADDRESS = {Toronto, Canada},
MONTH = {May},
OPTPAGES = {},
OPTANNOTE = {}
}
@INPROCEEDINGS{ICSE01,
AUTHOR = {William E. McUmber and Betty H.~C. Cheng},
TITLE = {A General Framework for Formalizing {UML} with Formal
Languages},
BOOKTITLE = {Proceedings of IEEE International Conference
on Software Engineering (ICSE01)},
YEAR = {2001},
ADDRESS = {Toronto, Canada},
MONTH = {May},
ANNOTE = {Formalization based on homomorphic mappings between
metamodels of UML and target specification languages.
Paper focuses on the Promela formal specification language
for SPIN model checker.}
}
@TECHREPORT{ICSE01-TR,
AUTHOR = {William E. McUmber and Betty H.C. Cheng},
TITLE = {A Generic Framework for Formalizing {UML} with Formal
Languages},
NUMBER = {MSU-CPS-99-10},
INSTITUTION = {Department of Computer Science, Michigan State
University},
ADDRESS = {East Lansing, Michigan},
ABSTRACT = {},
KEYWORDS = {metamodel, homomorphism, formal specifications,
object-oriented modeling notations},
NOTE = {(Revised August 2000, submitted for publication)},
MONTH = {February},
YEAR = {1999},
AUTHOR1_URL = {},
AUTHOR1_EMAIL = {bill@objectsr.com},
AUTHOR2_URL = {www.cse.msu.edu/~chengb},
AUTHOR2_EMAIL = {chengb@cse.msu.edu},
PAGES = {},
FILE = {},
URL = {},
CONTACT = {chengb@cse.msu.edu}
}
@INPROCEEDINGS{Enforms-Analysis,
AUTHOR = {Laura Campbell and Betty H.~C. Cheng and Enoch Y. Wang},
TITLE = {Enabling Automated Analysis Through the Formalization of Object-Oriented Modeling
Diagrams},
BOOKTITLE = {Proceedings of {IEEE} Dependable Systems and Networks ({FTCS-30} and {DCCA-8})},
YEAR = {2000},
ADDRESS = {New York, NY},
MONTH = {June},
KEY = {OMT, analysis}
}
@TECHREPORT{OO-Browser,
AUTHOR = {Douglas K. Pierce and Betty H.~C. Cheng},
TITLE = {Intelligent {B}rowser for {F}ormal {S}pecifications of
{S}oftware {C}omponents},
INSTITUTION = {Department of Computer Science, Michigan State University},
NUMBER = {MSU-CPS-91-14},
YEAR = {1991},
KEY = {FORMAL,WP,OO}
}
@TECHREPORT{Design-tool,
AUTHOR = {Tom Danieli and Betty H.~C. Cheng},
TITLE = {Construction of {F}ormal {S}pecifications from an
{O}bject-{O}riented {D}ecomposition of {I}nformal
{P}roblem {D}escriptions},
INSTITUTION = {Department of Computer Science, Michigan State
University},
NUMBER = {MSU-CPS-92-08},
YEAR = {1992},
KEY = {FORMAL,WP,DESIGN}
}
@ARTICLE{Cheng-CSE,
AUTHOR = {Betty H.~C. Cheng},
TITLE = {Applying Formal Methods in Automated Software Development},
JOURNAL = {Journal of Computer and Software Engineering},
VOLUME = {2},
NUMBER = {2},
PAGES = {137--164},
YEAR = {1994},
COMMENT = {synopsis of phd thesis},
KEY = {FORMAL,WP}
}
@TECHREPORT{Stride-Interval-TR,
AUTHOR = {Jianchang Mao and Betty H.~C. Cheng and Lionel M. Ni},
TITLE = {The Stride Interval Tests for Data Dependence Analysis},
INSTITUTION = {Department of Computer Science, Michigan State University},
NOTE = {submitted for publication},
NUMBER = {MSU-CPS-ACS-59},
YEAR = {1992},
COMMENT = {submitted to Int. Conf. Parallel and Distributed
Computing, Taiwan, July 1992}
}
@INPROCEEDINGS{Stride-Interval,
AUTHOR = {J. Mao and B.~H.~C. Cheng and L.~M. Ni},
TITLE = {The stride interval tests for data dependence analysis},
BOOKTITLE = {Proceedings of 1992
International Conference on Parallel and Distributed
Systems},
YEAR = {1992},
ADDRESS = {Taiwan},
MONTH = {December},
PAGE = {409--416},
NOTE = {Extended version in Department of Computer Science,
Michigan State University Technical
Report,MSU-CPS-ACS-59},
COMMENT = {parallel processing, compiler}
}
@TECHREPORT{DataPartitioning,
AUTHOR = {Joseph L.~Sharnowski and Betty H.~C. Cheng},
TITLE = {Using Visualizations to Guide Data Partitioning},
INSTITUTION = {Department of Computer Science, Michigan State University },
YEAR = {1993},
TYPE = {Technical Report},
NUMBER = {CPS-93-19},
ADDRESS = {A714 Wells Hall, East Lansing, Michigan 48824},
MONTH = {May},
COMMENT = {Predecessor to JPDC paper}
}
@ARTICLE{GOLD,
AUTHOR = {Joseph Sharnowski and Betty H.~C.~Cheng},
TITLE = {{GOLD}: A Graphical, On-Line Debugger for Parallel Programs},
JOURNAL = {submitted to IEEE Parallel and Distributed Technology},
YEAR = {1995},
OPTVOLUME = {},
OPTNUMBER = {},
OPTPAGES = {},
OPTMONTH = {},
NOTE = {Available as Department of Computer Science,
Technical Report, MSU-CPS-95-16, April 1995.}
}
@INPROCEEDINGS{TopDownViz,
AUTHOR = {Joseph L.~Sharnowski and Betty H.~C.~Cheng},
TITLE = {A Visualization-Based Environment for Top-down
Debugging of Parallel Programs},
BOOKTITLE = {Proceedings of 9th International Parallel Processing Symposium},
YEAR = {1995},
PAGES = {640--645},
ADDRESS = {Santa Barbara, CA},
MONTH = {April},
KEY = {VIZ,DEBUG}
}
@TECHREPORT{FM-ExpectedBehaviorTR,
AUTHOR = {Joseph L.~Sharnowski and Betty H.~C. Cheng},
TITLE = {A Formal Approach to Modeling Expected Behavior
in Parallel Program Visualizations},
INSTITUTION = {Department of Computer Science, Michigan State University },
YEAR = {1993},
TYPE = {Technical Report},
NUMBER = {CPS-93-30},
ADDRESS = {A714 Wells Hall, East Lansing, Michigan 48824},
MONTH = {November},
NOTE = {(submitted for publication)},
COMMENT = {submitted to PARLE'94}
}
@ARTICLE{FM-ExpectedBehavior,
AUTHOR = {Joseph L.~Sharnowski and Betty H.~C. Cheng},
TITLE = {A Formal Approach to Modeling Expected Behavior
in Parallel Program Visualizations},
JOURNAL = {Lecture Notes in Computer Science},
YEAR = {1994},
VOLUME = {817},
MONTH = {July},
PAGES = {202--213},
PUBLISHER = {Springer-Verlag},
NOTE = {PARLE'94}
}
@ARTICLE{JPDC-Visual,
AUTHOR = {M.~V. LaPolla and J.~L. Sharnowski and B.~H.~C. Cheng and K.~Anderson},
TITLE = {Data Parallel Program Visualizations from Formal
Specifications },
JOURNAL = {Journal of Parallel and Distributed
Computing},
YEAR = {1993},
VOLUME = {18},
NUMBER = {2},
PAGES = {252--257},
MONTH = {June},
NOTEBHCA = {Special issue on tools and methods for visualization},
NOTEBHC = {Special issue on tools and methods for visualization
of parallel systems and computations. Extended
version available as Michigan State University,
Department of Computer Science Technical Report
MSU-CPS-92-05},
COMMENT = {Tom Cassavant, guest editor of special issue of JPDC
on visualization tools and techniques.}
}
@INPROCEEDINGS{Minnowbrook-Visual,
AUTHOR = {Joseph Sharnowski and Betty H.~C. Cheng and Mark V. LaPolla},
TITLE = {Mapping Formal Specifications to Parallel Program
Visualizations},
BOOKTITLE = {Proceedings of Minnowbrook Workshop on Software
Engineering for Parallel Computing},
YEAR = {1992},
MONTH = {August},
PAGES = {29--34},
COMMENT = {Extended abstract of JPDC paper, introduced ports and
classified the complexity and dimension concepts.}
}
@TECHREPORT{Viz-Data,
AUTHOR = {J.~Sharnowski and B.~H.~C.~Cheng},
TITLE = {Using Visualizations to Guide Data Partitioning},
INSTITUTION = {Department of Computer Science, Michigan State University },
YEAR = {1993},
TYPE = {Technical Report},
NUMBER = {CPS-93-19},
ADDRESS = {A714 Wells Hall, East Lansing, Michigan 48824},
MONTH = {May},
COMMENT = {Scheme for data partitioning using visualizations}
}
@TECHREPORT{FM-Viz,
AUTHOR = {M.~V.~LaPolla and J.~Sharnowski and B.~H.~C.~Cheng
and K.~Anderson},
TITLE = {Using Formal Specifications to Generate
Visualizations of Data Parallelism},
INSTITUTION = {Department of Computer Science, Michigan State University },
YEAR = {1992},
TYPE = {Technical Report},
NUMBER = {CPS-92-05},
ADDRESS = {A714 Wells Hall, East Lansing, Michigan 48824},
MONTH = {July},
COMMENT = {Predecessor to JPDC paper}
}
@TECHREPORT{Guideplus,
AUTHOR = {J.L.~Sharnowski and K. Gidewall and Betty H.~C. Cheng},
TITLE = {Guideplus: An Interface-Building Tool for the Sun
OpenWindows},
INSTITUTION = {Michigan State University},
YEAR = {1992},
TYPE = {Technical Report},
NUMBER = {MSU-CPS-92-04},
ADDRESS = {Department of Computer Science, A714 Wells Hall, East
Lansing, MI 48824},
MONTH = {July},
COMMENT = {Independent study for adding graphical connections
between components for DevGuide 1.0. The 3.0 release
supersedes the capabilities provided by Guideplus.
This project also gave Kenton Gidewall an opportunity
to apply object-oriented programming techniques to a
project.},
KEY = {OO,GUI}
}
@TECHREPORT{Dist-Larch,
AUTHOR = {William McUmber and Betty H.~C. Cheng},
TITLE = {Formally Specifying Distributed Systems},
INSTITUTION = {Department of Computer Science, Michigan
State University},
YEAR = {1993},
TYPE = {Technical Report},
NUMBER = {MSU-CPS-93-25},
ADDRESS = {East Lansing, Michigan 48824},
MONTH = {October},
KEY = {DIST,FM,SPEC,LARCH}
}
@TECHREPORT{FM-Parallel-Tech,
AUTHOR = {D. R. Chesney and B. H.~C. Cheng},
TITLE = {Formal {S}pecification of {A}utomatic {S}ource {C}ode {T}ranslator for {P}arallel {C}omputer},
INSTITUTION = {Department of Computer Science,Michigan State University},
YEAR = {1992},
ADDRESS = {East Lansing, MI 48824},
MONTH = {October},
NOTE = {in preparation}
}
@TECHREPORT{FusionFission,
AUTHOR = {David R.~Chesney and Betty H.~C.Cheng},
TITLE = {Application of the Unimodular Approach to Loop Fission and Loop Fusion},
INSTITUTION = {Michigan State University},
YEAR = {1993},
TYPE = {Technical Report},
NUMBER = {CPS-93-13},
ADDRESS = {Department of Computer Science, A714 Wells Hall, East
Lansing, Michigan 48824},
MONTH = {March},
COMMENT = {Use formal specs to specify transformations}
}
@TECHREPORT{BlockCoalesce,
AUTHOR = {David R.~Chesney and Betty H.~C.Cheng},
TITLE = { Extending the Unimodular Approach to Other Transformation Techniques},
INSTITUTION = {Michigan State University},
YEAR = {1993},
TYPE = {Technical Report},
NUMBER = {CPS-93-24},
ADDRESS = {Department of Computer Science, A714 Wells Hall, East
Lansing, Michigan 48824},
MONTH = {September},
COMMENT = {Use formal specs to specify transformations}
}
@INPROCEEDINGS{FM-Parallel-Paper,
AUTHOR = {D.R. Chesney and B. H.~C. Cheng},
TITLE = {A Formal {A}pproach to {A}utomatic {S}ource {C}ode {T}ranslation for {P}arallel {A}rchitectures},
BOOKTITLE = {Proceedings of Minnowbrook Workshop on Software for
Parallel Computing},
MONTH = {August},
YEAR = {1992},
PAGES = {29--34},
KEY = {FM,PP,SPEC},
COMMENT = {beef up references, clarify related work, Kuck et al}
}
@INPROCEEDINGS{Minnowbrook91,
AUTHOR = {Betty H.~C. Cheng},
TITLE = {Constructing Formal Specifications from Informal
Descriptions },
BOOKTITLE = {Proceedings of Fourteenth Minnowbrook Software
Engineering Workshop},
YEAR = {1991},
PAGES = {22--23},
BHCORGANIZATION = {Syracuse University and Software Engineering
Research Center, Purdue University},
BYCADDRESS = {Minnowbrook Conference Center, New York},
MONTH = {July},
KEY = {FM,INFORMAL}
}
@TECHREPORT{FM-Reuse-techreport,
AUTHOR = {{Jun-Jang} Jeng and Betty H.~C. Cheng},
TITLE = {Using {A}utomated {R}easoning to {D}etermine
{S}oftware {R}euse},
INSTITUTION = {Department of Computer Science, Michigan
State University},
NOTE = {accepted for publication in IJSEKE},
YEAR = {1992},
NUMBER = {MSU-CPS-ACS-64},
ADDRESS = {East Lansing, Michigan},
MONTH = {June},
KEY = {FORMAL,WP,SPEC,REUSE}
}
@INPROCEEDINGS{WISR92,
AUTHOR = {Betty H.~C. Cheng and {Jun-Jang} Jeng},
TITLE = {Formal Methods Applied to Reuse},
BOOKTITLE = {Proceedings of the Fifth Workshop in Software Reuse},
YEAR = {1992},
COMMENT = {Short position paper of IJSEKE}
}
@ARTICLE{FM-Reuse,
AUTHOR = {Jun-Jang Jeng and Betty H.~C. Cheng},
TITLE = {Using {A}utomated {R}easoning to {D}etermine
{S}oftware {R}euse},
JOURNAL = {International Journal of Software Engineering and
Knowledge Engineering},
VOLUME = {2},
NUMBER = {4},
MONTH = {December},
YEAR = {1992},
PAGES = {523--546},
COMMENT = {Identification scheme for reuse},
KEY = {REUSE}
}
@TECHREPORT{FM-SW-Comp-tech,
AUTHOR = {Jun-Jang Jeng and Betty H.~C. Cheng},
TITLE = {Using {F}ormal {M}ethods to {C}onstruct a {S}oftware
{C}omponent {L}ibrary},
INSTITUTION = {Michigan State University, Department of Computer
Science},
NUMBER = {MSU-CPS-92-11},
NOTE = {submitted for publication},
YEAR = {1992},
KEY = {FORMAL,WP,SPEC,REUSE}
}
@ARTICLE{FM-SW-Comp,
AUTHOR = {Jun-Jang Jeng and Betty H.~C. Cheng},
TITLE = {Using {F}ormal {M}ethods to {C}onstruct a {S}oftware
{C}omponent {L}ibrary},
JOURNAL = {Lecture Notes in Computer Science},
VOLUME = {717},
PUBLISHER = {Springer-Verlag},
PAGES = {397--417},
YEAR = {1993},
MONTH = {September},
NOTE = {(Proceedings of Fourth European Software Engineering Conference)}
}
@INPROCEEDINGS{ReuseAnalogy,
AUTHOR = {Jun-Jang Jeng and Betty H.~C. Cheng},
TITLE = {Using Analogy to Determine Program Modifications
Based on Specification Changes},
BOOKTITLE = {Proceedings of IEEE 5th Int'l Conf. on Tools with Artificial
Intelligence},
YEAR = {1993},
ADDRESS = {Boston, MA},
PAGES = {113--116},
MONTH = {November},
COMMENT = {Preliminary results about the use of analogy to
determine program modifications based on
specification changes.},
KEY = {REUSE,FM,SPEC}
}
@INPROCEEDINGS{SSR95-REUSE,
AUTHOR = {Jun-Jang Jeng and Betty H.~C. Cheng},
TITLE = {{S}pecification {M}atching for {S}oftware {R}euse:
{A} {F}oundation},
BOOKTITLE = {ACM Symposium on Software Reuse},
PAGES = {97--105},
MONTH = {April},
YEAR = {1995},
ADDRESS = {Seattle, Washington},
KEY = {REUSE,FORMAL},
FILE = {ssr95.ps.Z}
}
@TECHREPORT{OSPL-TR,
AUTHOR = {Betty H.~C.~Cheng and Jun-Jang Jeng},
TITLE = {Reusing Analogous Components},
INSTITUTION = {Michigan State University},
YEAR = {1994},
TYPE = {Technical Report},
NUMBER = {MSU-CPS-94-28},
ADDRESS = {Department of Computer Science, A714 Wells Hall, East
Lansing, MI 48824-1027},
MONTH = {April},
NOTE = {Revised June 1995},
COMMENT = {Techreport version of OSPL paper (submitted to TKDE),
large version of paper published in ICTAI93.}
}
@ARTICLE{ReuseAnalogy-TKDE,
AUTHOR = {Betty H.C.~Cheng and Jun-Jang Jeng},
TITLE = {Reusing Analogous Components},
JOURNAL = {IEEE Trans. on Knowledge and Data Engineering},
YEAR = {1997},
VOLUME = {9},
NUMBER = {2},
MONTH = {March},
PAGES = {341--349},
COMMENT = {Short paper, after major revisions. Longer version
of ICTAI paper.}
}
@INPROCEEDINGS{Reuse-General-KBSE,
AUTHOR = {Jun-Jang Jeng and Betty H.~C.~Cheng},
TITLE = {A Formal Approach to Reusing More General Components},
BOOKTITLE = {IEEE 9th Knowledge-Based Software Engineering Conference},
YEAR = {1994},
PAGES = {90--97},
ADDRESS = {Monterey, California},
MONTH = {September},
COMMENT = {Using OSPL to describe the logic for software reuse}
}
@INPROCEEDINGS{Graz-EIS,
AUTHOR = {Robert H. Bourdeau and Bryan Pijanowski and Betty
H.~C. Cheng},
TITLE = {A Decision Support System for Regional Environmental
Analysis},
BOOKTITLE = {Proceedings of 25th International Symposium on Remote
Sensing and Global Environmental Change: Tools for
Sustainable Development (Vol.~II)},
YEAR = {1993},
PAGES = {223--233},
ADDRESS = {Graz, Austria},
KEY = {EIS}
}
@ARTICLE{PERS-EIS,
AUTHOR = {Robert H.~Bourdeau and Betty H.~C.~Cheng and Bryan Pijanowski},
TITLE = {A Regional Information System for Environmental Data Analysis},
JOURNAL = {Photogrammetric Engineering \& Remote Sensing},
NUMBER = {7},
VOLUME = {62},
MONTH = {July},
YEAR = {1994},
PAGES = {855--861},
KEY = {EIS}
}
@INPROCEEDINGS{ENFORMS-ICMCS,
AUTHOR = {Joseph L. Sharnowski and Gerald C. Gannod and Betty
H.C. Cheng},
TITLE = {A Distributed Multimedia Environmental Information System},
BOOKTITLE = {Proceedings of IEEE Int. Conference on Multimedia and
Computing Systems},
YEAR = {1995},
PAGES = {142--194},
ADDRESS = {Washington, DC},
MONTH = {May},
COMMENT = {Submitted to IEEE Multimedia},
KEY = {ENFORMS,MULTIMEDIA}
}
@INCOLLECTION{ENFORMS-Book,
AUTHOR = {Gerald C.~Gannod and Betty H.~C.~Cheng},
BOOKTITLE = {Multimedia and Storage Management},
TITLE = {Development of Multimedia Information Systems},
PUBLISHER = {Kluwer Academic Publishers},
YEAR = {1996},
KEY = {OO,ENFORMS},
EDITOR = {S.M.~Chung},
COMMENT = {Overview of building multimedia systems, with
specific emphasis on OO approaches.}
}
@TECHREPORT{US-Mexico94,
AUTHOR = {Betty H.~C.~Cheng and Steve R. Schafer},
TITLE = {Design {D}ocument for 1993 {K}nowledge {T}ransfer {P}rototype
{R}egional {I}nformation {S}ystem for {US}/{M}exico {B}order},
INSTITUTION = {Department of Computer Science, Michigan State University},
YEAR = {1994},
TYPE = {Technical Report},
NUMBER = {MSU-CPS-94-37},
ADDRESS = {A714 Wells Hall, East Lansing, Michigan, USA},
MONTH = {July},
COMMENT = {CIESIN/USDA Project report}
}
@TECHREPORT{SaginawBay-USDA,
AUTHOR = {Betty H.C. Cheng and Robert H. Bourdeau},
TITLE = {Design Document for {T}ask \#6 of {CIESIN/USDA} {G}lobal
{C}hange {D}ata {A}ssessment and {I}ntegration {P}roject},
INSTITUTION = {Department of Computer Science, Michigan
State University},
YEAR = {1992},
TYPE = {Technical Report},
NUMBER = {MSU-CPS-92-21},
ADDRESS = {A714 Wells Hall, East Lansing, Michigan, USA},
MONTH = {November},
COMMENT = {Created techreport for USDA deliverable of 1992.}
}
@TECHREPORT{Enforms-Multimedia-Journal,
AUTHOR = {Joseph L.~Sharnowski and Gerald C.~Gannod and Betty H.~C.~Cheng},
TITLE = {ENFORMS: A Distributed Multimedia Environmental Information System},
INSTITUTION = {Michigan State University},
YEAR = {1994},
TYPE = {Technical Report},
NUMBER = {MSU-CPS-94-57},
ADDRESS = {Department of Computer Science, East Lansing, MI 48824},
MONTH = {November},
NOTE = {(submitted for publication)}
}
@INPROCEEDINGS{Enforms-Multimedia-Conf,
AUTHOR = {Joseph L.~Sharnowski and Gerald C.~Gannod and Betty H.~C.~Cheng},
TITLE = {A Distributed Multimedia Environmental Information System},
BOOKTITLE = {Proceedings of IEEE International Conference on Multimedia
and Computing Systems},
YEAR = {1995},
PAGES = {142--149},
ADDRESS = {Washington, D.C.},
MONTH = {May},
COMMENT = {Longer version sent to IEEE Multimedia, May 1995.},
KEY = {MULT,ENFORMS}
}
@INPROCEEDINGS{OO-CIESIN,
AUTHOR = {Betty H.~C.~Cheng and Robert H. Bourdeau and Gerald C. Gannod},
TITLE = {The Object-Oriented Development of a Distributed
Multimedia Environmental Information System},
BOOKTITLE = {Proceedings of 6th International Conference on Software
Engineering and Knowledge Engineering},
YEAR = {1994},
MONTH = {June},
PAGES = {70--77},
KEY = {CIESIN,OOP}
}
@TECHREPORT{OO-CIESIN2,
AUTHOR = {Robert H. Bourdeau and Gerald C. Gannod and Betty
H.~C. Cheng},
TITLE = {The Object-Oriented Development of a Contextual
Information System},
INSTITUTION = {Michigan State University},
YEAR = {1993},
TYPE = {Technical Report},
NUMBER = {CPS-93-5},
ADDRESS = {Department of Computer Science, A714 Wells Hall, East
Lansing, Michigan 48824},
MONTH = {February},
KEY = {CIESIN,OOP}
}
@INPROCEEDINGS{ACM-GIS,
AUTHOR = {N.~Bourbakis and W.~Campbell and B.~Cheng and
M.~Gennert and K.~Makki},
TITLE = {The Role of Multimedia and {AI} in {GIS}},
BOOKTITLE = {Proceedings of the Second ACM Workshop on Advances in
Geographic Information Systems},
YEAR = {1994},
EDITOR = {Niki Pissinou and Kia Makki},
PAGES = {84--88},
ADDRESS = {Gaithersburg, Maryland},
MONTH = {December},
COMMENT = {Panelists for AI in GIS, organized by Bourbakis},
KEY = {ENFORMS,MULT}
}
@TECHREPORT{Enforms-DigitalLibrary,
AUTHOR = {Betty H.~C.Cheng and Gerald C.~Gannod and Dan Judd
and Philip K.~McKinley},
TITLE = {Object-Oriented Environmental Information System for Multimedia
Information Using Traditional and High-Speed Networks},
INSTITUTION = {Michigan State University},
YEAR = {1995},
TYPE = {Technical Report},
NUMBER = {MSU-CPS-95-30},
ADDRESS = {Department of Computer Science},
MONTH = {July},
COMMENT = {Paper about EPA project. Focus on OO,
spatial/temporal referencing, and across high-speed
networks. Submitted to special issue of IEEE Computer
on Large-Scale Digital Libraries. Due September 1, 1995.}
}
@INPROCEEDINGS{ASE97-Reuse,
AUTHOR = {Yonghao Chen and Betty H.~C.~Cheng},
TITLE = {Facilitating an Automated Approach to
Architecture-based Software Reuse},
BOOKTITLE = {Proceedings IEEE of Automated Software Engineering Conference},
YEAR = {1997},
ADDRESS = {Lake Tahoe, Nevada},
MONTH = {November},
ANNOTE = {Presented at ASE by Jerry}
}
@INPROCEEDINGS{ICTAI97-Reuse,
AUTHOR = {Yonghao Chen and Betty H.~C.~Cheng},
TITLE = {Formalizing and Automating Component Reuse},
BOOKTITLE = {Proceedings IEEE of International Conference on Tools with
Artificial Intelligence},
YEAR = {1997},
ADDRESS = {Newport Beach, California},
MONTH = {November},
KEY = {reuse, architecture}
}
@INPROCEEDINGS{WISR8-Reuse,
AUTHOR = {Yonghao Chen and Betty H.~C.~Cheng},
TITLE = {Formally Specifying and Analyzing Architectural and
Functional Properties of Components for Reuse},
BOOKTITLE = {Proceedings Eighth Annual Workshop on Software Reuse (WISR8)},
YEAR = {1997},
ADDRESS = {Columbus, Ohio},
MONTH = {March},
KEY = {reuse, architecture}
}
@TECHREPORT{SSR99,
AUTHOR = {Yonghao Chen and Betty H.C. Cheng},
TITLE = {A Theory of Specification Matching},
NUMBER = {MSU-CPS-98-30},
INSTITUTION = {Department of Computer Science, Michigan StateUniversity},
ADDRESS = {East Lansing, Michigan},
ABSTRACT = {Determining the behavioral relationship between software components is a
central task for many software engineering activities, such as reuse,
maintenance, and object-oriented subtyping.
With the ever increasing
adoption of formal methods, specification matching has
been proposed as a means to evaluate component relations at an
abstract level. A number of specification
matches have
been proposed to capture the notion of behavioral
subsumption, or reusability in the context of software reuse.
However, lacking rigorousness in establishing
connection between a specification match
and reusability may call into question the usefulness of the
specification match.
In this paper, we establish a semantic foundation for reasoning
the connections between a specification match and its usefulness for
determining reusability, and provide a framework to evaluate various
specification matches. In particular, we discuss a
special type of specification matching, reuse-ensuring match.
We prove that the set of all
non-logically equivalent reuse-ensuring matches together with the
logical implication (=>) operator constitute a
complete lattice. Moreover, we give the lattice's greatest and least
elements, which are also the most general and most
specific reuse ensuring matches, respectively.},
KEYWORDS = {reuse, specification matching},
NOTE = {(submitted for publication)},
MONTH = {October},
YEAR = {98},
AUTHOR1_URL = {www.cse.msu.edu/~chenyong},
AUTHOR1_EMAIL = {chenyong@cse.msu.edu},
AUTHOR2_URL = {www.cse.msu.edu/~chengb},
AUTHOR2_EMAIL = {chengb@cse.msu.edu},
PAGES = {},
FILE = {},
URL = {},
CONTACT = {chengb@cse.msu.edu}
}
@INPROCEEDINGS{FTCS30,
AUTHOR = {Betty H~.C. Cheng and Laura A. Campbell and Enoch Y. Wang},
TITLE = {Enabling Automated Analysis Through the Formalization of Object-Oriented Diagrams},
BOOKTITLE = {Proceedings of the IEEE Int. Conf. on Dependable Systems and Networks (FTCS-30 and DCCA-8)},
OPTCROSSREF = {},
OPTKEY = {},
PAGES = {305--314},
YEAR = {2000},
OPTEDITOR = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTSERIES = {},
ADDRESS = {New York, NY},
MONTH = {June},
OPTORGANIZATION = {IEEE Computer Society},
OPTPUBLISHER = {},
OPTANNOTE = {}
}
@INPROCEEDINGS{Telemedicine-OMT,
AUTHOR = {Laura A. Campbell and Betty H.~C. Cheng},
TITLE = {Object-Oriented Modeling and Automated Analysis of a Telemedicine Application},
BOOKTITLE = {Proceedings of the IEEE International Workshop on Software
Specification and Design (IWSSD-10).},
OPTCROSSREF = {},
OPTKEY = {},
OPTPAGES = {},
YEAR = {2000},
OPTEDITOR = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTSERIES = {},
ADDRESS = {Shelter Island, San Diego, California},
MONTH = {November},
OPTORGANIZATION = {IEEE Computer Society},
OPTPUBLISHER = {},
OPTANNOTE = {}
}
@TECHREPORT{SmartCruiseCaseStudy-TR,
AUTHOR = {Laura A. Campbell and William E. McUmber and Betty H.~C. Cheng},
TITLE = {Enabling Automated Analysis of Embedded Systems Designs via Formalization of UML},
NUMBER = {MSU-CSE-00-22},
INSTITUTION = {Computer Science and Engineering, Michigan State University},
ADDRESS = {East Lansing, Michigan},
ABSTRACT = {A number of object-oriented techniques and notations have been introduced, but recently, it appears that the {\it Unified Modeling
Language} (UML) could be a notation broad enough in scope to represent a variety of domains and gain widespread use. Currently, UML comprises several
different notations with no formal semantics attached to the individual diagrams. Therefore, it is not possible to apply rigorous automated analysis or to execute
a UML model in order to test its behavior, short of writing code and performing exhaustive testing. We have developed a generic framework for formalizing a
subset of UML diagrams in terms of various formal languages. This framework enables different modelers to target various formal languages since one formal
language may be more suitable for representing the semantics of a particular domain or class of applications. Currently, we have focused on the formalization
of UML for modeling embedded systems. This paper presents a case study of the design of an industrial embedded system. In this case study we map UML
to Promela, the language for the model checker SPIN, thus enabling us to perform automated analysis of the UML diagrams, including model checking and
behavior simulation. We also describe a number of visualizations that we have developed to assist in the interpretation of the analysis results.},
KEYWORDS = {object-oriented modeling, formal specifcations, model checking, simulation, visualization},
NOTE = {submitted to IEEE Transactions on Computers},
MONTH = {October},
YEAR = {2000},
AUTHOR1_URL = {},
AUTHOR1_EMAIL = {mcumber@cse.msu.edu},
AUTHOR2_URL = {},
AUTHOR2_EMAIL = {campb222@cse.msu.edu},
PAGES = {40},
FILE = {},
URL = {},
CONTACT = {chengb@cse.msu.edu}
}
@TECHREPORT{MSU-CSE-02-16,
AUTHOR = {R.E.K. Stirewalt and Betty H.C. Cheng and William E. McUmber},
TITLE = {An OO-Framework Approach to a Generic UML Formalization Tool},
NUMBER = {MSU-CSE-02-16},
INSTITUTION = {Computer Science and Engineering, Michigan State University},
ADDRESS = {East Lansing, Michigan},
ABSTRACT = {Growing interest in defining formal semantics for UML diagrams motivates the need for systematic approaches to developing tools
that support the generation of formal specifications from UML. The formal specifications can then be used as the medium for detecting inconsistency
and incompleteness errors in the diagrams. It is becoming increasingly clear that different domains demand different semantic interpretations for UML
diagrams, thus further motivating the need for general formalization utilities. This paper presents an object-oriented (OO) framework approach to
constructing UML formalization tools, where there is a clear separation between the part of the framework that is reusable across all target formal
specifications and that which is target-language specific. The OO framework implementation rests atop formalization rules that are specified using
inference rules.},
KEYWORDS = {OO framework, UML formalization, inference rules},
NOTE = {Submitted for Publication},
MONTH = {June},
YEAR = {2002},
AUTHOR1_URL = {www.cse.msu.edu/~stire},
AUTHOR1_EMAIL = {stire@cse.msu.edu},
AUTHOR2_URL = {www.cse.msu.edu/~chengb},
AUTHOR2_EMAIL = {chengb@cse.msu.edu},
PAGES = {},
FILE = {},
URL = {},
CONTACT = {stire@cse.msu.edu},
CONF = { submitted to PASTE02, June 15, 2002}
}
@ARTICLE{Meridian-article,
AUTHOR = {Betty H.C.~Cheng and Philip K. McKinley and R.~E.~K. Stirewalt and Laura K. Dillon},
TITLE = {Meridian: Automating the Development of Interactive Distributed Applications},
JOURNAL = {IEEE Computer},
YEAR = {},
NOTE = {under revision},
OPTVOLUME = {9},
OPTNUMBER = {2},
OPTMONTH = {March},
OPTPAGES = {341--349},
OPTCOMMENT = {Need to revise to add "glue text"}
}
@INCOLLECTION{SafeAdaptation-ADS-LNCS05,
AUTHOR = {Ji Zhang and Betty H~C. Cheng and Zhenxiao Yang and
Philip K. McKinley},
TITLE = {Enabling Safe Dynamic Component-Based Software Adaptation},
BOOKTITLE = {Architecting Dependable Systems {III}, Springer Lecture Notes for Computer Science},
EDITOR = {Rogerio de Lemos, Cristina Gacek, Alexander Romanovsky},
PUBLISHER = {Springer-Verlag},
YEAR = {2005},
NOTE = {(in press)}
}
@ARTICLE{ObjectAnalysisPatterns-TSE,
AUTHOR = {Sascha Konrad and Betty H.C. Cheng and Laura Campbell},
TITLE = {Object Analysis Patterns for Embedded Systems},
OPTABSTRACT = {},
JOURNAL = {IEEE Transactions on Software Engineering},
YEAR = {2004},
PAGES = {970--992},
MONTH = {December},
VOLUME = {30},
NUMBER = {12}
}
@INPROCEEDINGS{RE-Levels-REFSQ05,
AUTHOR = {Daniel M. Berry and Betty H.C. Cheng and Ji Zhang},
TITLE = {The Four Levels of Requirements Engineering for and
in Dynamic Adaptive Systems},
BOOKTITLE = {11th International Workshop on Requirements
Engineering Foundation for Software Quality (REFSQ)},
YEAR = 2005,
ADDRESS = {Porto, Portugal},
MONTH = {June}
}
@INPROCEEDINGS{NL-SpecPatterns-RE05,
AUTHOR = {Sascha Konrad and Betty H~.C. Cheng},
TITLE = {Facilitating the Construction of Specification
Patterns-based Properties},
BOOKTITLE = {13th IEEE International Requirements Engineering
Conference (RE05)},
YEAR = 2005,
ORGANIZATION = {IEEE},
ADDRESS = {Paris, France},
MONTH = {August},
NOTE = {(accepted to appear)}
}
@INPROCEEDINGS{TransparentShaping-DEAS05,
AUTHOR = {S.~Masoud Sadjadi, Philip K.~McKinley and Betty H.~C.~Cheng},
TITLE = {Transparent Shaping of Existing Software to Support
Pervasive and Autonomic Computing},
BOOKTITLE = {IEEE ICSE Workshop on Design and Evolution of
Autonomic Computing Systems (DEAS)},
YEAR = 2005,
ORGANIZATION = {IEEE},
ADDRESS = {St. Louis, Missouri},
MONTH = {May},
NOTE = {(also accepted for presentation)}
}
@INPROCEEDINGS{TRAP-CPP-DEAS05,
AUTHOR = {Scott D.~Fleming and Betty H.C. Cheng and Kurt
Stirewalt and Philip K. McKinley},
TITLE = {An Approach to Implementing Dynamic Adaptation in C++},
BOOKTITLE = {IEEE ICSE Workshop on Design and Evolution of
Autonomic Computing Systems (DEAS)},
YEAR = 2005,
ORGANIZATION = {IEEE},
ADDRESS = {St. Louis, Missouri},
MONTH = {May}
}
@INPROCEEDINGS{AdaptationSemantics-WADS05,
AUTHOR = {Ji Zhang and Betty H.~C. Cheng},
TITLE = {Specifying Adaptation Semantics},
BOOKTITLE = {IEEE ICSE Workshop on Architecting Dependable
Systems (WADS)},
YEAR = 2005,
ORGANIZATION = {IEEE},
ADDRESS = {St. Louis, Missouri},
MONTH = {May}
}
@INPROCEEDINGS{RealTimeSpecPatterns-ICSE05,
AUTHOR = {Sascha Konrad and Betty H.~C. Cheng},
TITLE = {Real-time Specification Patterns},
BOOKTITLE = {IEEE International Conference on Software
Engineering (ICSE05)},
YEAR = 2005,
ORGANIZATION = {IEEE},
ADDRESS = {St. Louis, Missouri},
MONTH = {May},
NOTE = {(acceptance rate 14\%)}
}
@INPROCEEDINGS{ResourceFeatureInteraction-WOSS04,
AUTHOR = {Jesus Bisbal and Betty H.C. Cheng},
TITLE = {Resource-based Approach to Feature Interaction in
Adaptive Software},
BOOKTITLE = {ACM SIGSOFT Workshop on Self-Managing Systems (WOSS04)},
YEAR = {2004},
MONTH = {November}
}
@INPROCEEDINGS{SecurityPatterns-RHAS03,
AUTHOR = {Sascha Konrad and Laura Campbell and Betty H.~C. Cheng},
TITLE = {Automated Analysis of Timing Information in UML Diagrams},
BOOKTITLE = {Proc. of IEEE International Conference on Automated Software Engineering},
YEAR = 2004,
NOTE = {Short paper},
ADDRESS = {Linz, Austria},
MONTH = {September}
}
@INPROCEEDINGS{TimingExtensions-ASE04,
AUTHOR = {Sascha Konrad and Laura Campbell and Betty H.~C. Cheng
Ronald Wassermann},
TITLE = {Using Security Patterns to Model and Analyze
Security Requirements},
BOOKTITLE = {IEEE Workshop on Requirements for High Assurance
Systems (RHAS03)},
YEAR = 2003,
ADDRESS = {Monterey, California},
MONTH = {September}
}
@INPROCEEDINGS{spin03,
AUTHOR = {Sascha Konrad and Laura A. Campbell and Betty H.~C. Cheng and Min Deng},
TITLE = {A Requirements Patterns-Driven Approach to Check Systems and Specify Properties},
BOOKTITLE = {Model Checking Software (SPIN 2003)},
YEAR = {2003},
EDITOR = {Thomas Ball and Sirom K. Rajamani},
VOLUME = {},
NUMBER = {2648},
SERIES = {Lecture Notes in Computer Science},
PAGES = {18-33},
ADDRESS = {},
MONTH = {May},
ORGANIZATION = {},
PUBLISHER = {Springer Verlag},
NOTE = {},
ABSTRACT = {},
KEYWORDS = {},
FILE = F
}
@ARTICLE{REJ-AnalysisViz,
AUTHOR = {Laura A. Campbell and Betty H.~C.~Cheng and William E. McUmber and
R.E.K. Stirewalt},
TITLE = {Automatically Detecting and Visualizing Errors in {UML}
Diagrams},
JOURNAL = {Requirements Engineering Journal},
YEAR = {2002},
OPTKEY = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTPAGES = {},
MONTH = {December},
OPTNOTE = {},
OPTANNOTE = {}
}
@ARTICLE{DesignAdvisor05,
AUTHOR = {Ryan Stephenson and Betty H.C. Cheng and Brian Berenbach},
TITLE = {Lessons Learned from Metrics-Based Automated Analysis of Industrial UML Models},
BOOKTITLE = { Proc. of the ACM/IEEE $8^{th}$ International
Conference on Model Driven Engineering
Languages and Systems (MoDELS/UML 2005) },
YEAR = 2005,
NOTE = {(to appear)}
}
@INCOLLECTION{Sowell:ads05,
AUTHOR = { J. H. Sowell and R. E. K. Stirewalt },
TITLE = { A feature-oriented alternative to implementing
reliability connector wrappers },
BOOKTITLE = { Architecting Dependable Systems III },
EDITOR = { R. {de Lemos} and C. Gacek and A. Romanovsky },
PUBLISHER = { Springer },
YEAR = 2005
}
@ARTICLE{Deng:ijseke05,
AUTHOR = { M. Deng and R. E. K. Stirewalt and B. H. C. Cheng },
TITLE = { Retrieval by Construction: A Traceability Technique to
Support Verification and Validation of UML Formalizations },
JOURNAL = { International Journal of Software Engineering
and Knowledge Engineering },
NOTE = { To appear },
MONTH = OCT,
YEAR = 2005
}
@ARTICLE{Rugaber:software04,
AUTHOR = { S. Rugaber and R. E. K. Stirewalt },
TITLE = { Model-driven reverse engineering },
JOURNAL = { IEEE Software },
VOLUME = 21,
NUMBER = 4,
PAGES = { 45--53 },
MONTH = {July},
YEAR = 2004
}
@INPROCEEDINGS{Stirewalt:NasaSEW05,
AUTHOR = { R. E. K. Stirewalt and R. Behrends and L. K. Dillon },
TITLE = { Safe and Reliable use of Concurrency in Multi-Threaded
Shared Memory Sytems },
BOOKTITLE = { Proc. of the $29^{th}$ Annual IEEE/NASA
Software Engineering Workshop },
YEAR = 2005
}
@TECHREPORT{Stirewalt:TR04,
AUTHOR = {R. E. K. Stirewalt and Reimer Behrends and Laura K. Dillon},
TITLE = {A model-based semantics for synchronization contracts
in object-oriented languages },
NUMBER = {MSU-CSE-04-38},
INSTITUTION = {Computer Science and Engineering,
Michigan State University},
ADDRESS = {East Lansing, Michigan},
MONTH = AUG,
YEAR = 2004
}
@TECHREPORT{Stirewalt:TR03a,
AUTHOR = {R. E. K. Stirewalt and Reimer Behrends and Laura K. Dillon},
TITLE = {Formal specification of the universe model},
NUMBER = {MSU-CSE-03-7},
INSTITUTION = {Computer Science and Engineering, Michigan State University},
ADDRESS = {East Lansing, Michigan},
MONTH = {March},
YEAR = {2003}
}
@INPROCEEDINGS{mcgu97:qw,
AUTHOR = {Hugh McGuire and Laura K. Dillon and Y. S. Ramakrishna},
TITLE = {Generating Trace Checkers for Test Oracles},
BOOKTITLE = {Proc.~International Quality Week},
YEAR = 1997,
PAGES = {3-T-2},
ADDRESS = {San Francisco},
MONTH = MAY,
PUBLISHER = {Software Research Institute},
KEYWORDS = {}
}
@INPROCEEDINGS{mell92:rtwksp,
AUTHOR = {P. Michael {Melliar-Smith} and Louise E. Moser and
Laura K. Dillon},
TITLE = {Real-Time Graphical Interval Logic: Position Paper},
BOOKTITLE = {Proc. Ninth IEEE Workshop on Real-Time Operating Systems
and Software},
YEAR = 1992,
ADDRESS = {Pittsburg, PA},
PAGES = {100--103},
MONTH = MAY,
NOTE = {},
KEYWORDS = {}
}
@INPROCEEDINGS{mell90:icsi-workshop,
AUTHOR = {P. Michael {Melliar-Smith} and Louise E. Moser and Laura K.
Dillon and Y. S. Ramakrishna},
TITLE = {The Development of Graphical Interval Logic},
CROSSREF = {berkeley-workshop-temporal-and-realtime-specs},
PAGES = {105--116},
KEYWORDS = {}
}
@INPROCEEDINGS{mell94:automated-deduction,
AUTHOR = {P.~Michael Melliar-Smith and Louise E. Moser and
George Kutty and Y. S. Ramakrishna and Laura K. Dillon},
TITLE = {A System for Automated Deduction in {Graphical Interval
Logic}: A System Description Paper},
BOOKTITLE = {Proc.\ 1st Inter.\ Conf.\ Temporal Logic},
EDITOR = {Dov M.\ Gabbay and Hans J{\"u}rgen Ohlbach},
YEAR = 1994,
MONTH = JUL,
PAGES = {540--542},
PUBLISHER = {Springer-Verlag},
ADDRESS = {Bonn, Germany},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = 827,
NOTE = {}
}
@INPROCEEDINGS{mose92:stc,
AUTHOR = {Loiuse E. Moser and
P. Michael {Melliar-Smith} and Laura K. Dillon},
TITLE = {Graphical Tools for Development of Concurrent Systems:
Research Summary},
BOOKTITLE = {Proc. DARPA Software Technology Conference},
YEAR = 1992,
PAGES = {508--511},
ADDRESS = {Los Angeles, CA},
MONTH = APR,
NOTE = {},
KEYWORDS = {}
}
@UNPUBLISHED{mose:tse-submission,
AUTHOR = {Louise E. Moser and Y. S. Ramakrishna and George Kutty
and P. Michael {Melliar-Smith} and Laura K. Dillon},
TITLE = {A Graphical Environment for Design of Concurrent and
Realtime Systems},
NOTE = {Submitted}
}
@ARTICLE{mose96:tosem,
AUTHOR = {Louise E. Moser and Y. S. Ramakrishna and George Kutty
and P. Michael {Melliar-Smith} and Laura K. Dillon},
TITLE = {A Graphical Environment for Design of Concurrent and
Realtime Systems},
YEAR = 1996,
JOURNAL = {TOSEM},
VOLUME = 6,
NUMBER = 1,
MONTH = JAN,
PAGES = {31--79}
}
@INPROCEEDINGS{mose93:temporal-deduction,
AUTHOR = {George Kutty and Louise E. Moser and P.~Michael
Melliar-Smith and Laura K. Dillon and Y. S. Ramakrishna},
TITLE = {Temporal Deduction in a Graphical Logic},
BOOKTITLE = {Proc.\ AAAI Symp.\ Automated Deduction in Nonstandard Logics},
YEAR = 1993,
PAGES = {89--96},
ADDRESS = {Raliegh, NC},
MONTH = OCT,
NOTE = {},
KEYWORDS = {}
}
@INPROCEEDINGS{mose96:cav96-system-description,
AUTHOR = {Louise E.~Moser and P.~Michael
Melliar-Smith and Y. S. Ramakrishna
and George Kutty and Laura K.~Dillon},
TITLE = {The Real-Time Graphical Interval Logic Toolset},
BOOKTITLE = {Proc.\ 8th Inter.\ Conf.\ Computer-Aided Verification},
YEAR = 1996,
PAGES = {446--449},
MONTH = AUG,
NOTE = {System description paper},
KEYWORDS = {}
}
@ARTICLE{mose96:jancl,
AUTHOR = {Louise E.~Moser and P.~Michael
Melliar-Smith and Y. S. Ramakrishna
and George Kutty and Laura K.~Dillon},
TITLE = {Automated Deduction in a Graphical Temporal Logic},
JOURNAL = {Journal of Applied Non-Classical Logics},
YEAR = 1996,
VOLUME = 6,
NUMBER = 1,
PAGES = {29--47},
KEYWORDS = {}
}
@INPROCEEDINGS{omal96:css,
AUTHOR = { T. Owen O'Malley and Deborah J. Richardson and Laura K. Dillon},
TITLE = {Efficient Specification-based Oracles for Critical Systems},
BOOKTITLE = {Proc.\ 1996 California Systems Symposium},
MONTH = APR,
YEAR = 1996,
EDITOR = {Walter Scacchi and Richard Taylor},
PAGES = {50--59},
ADDRESS = {Los Angeles, CA},
KEYWORDS = {}
}
@ARTICLE{rama92:sutl,
AUTHOR = {Y. S. Ramakrishna and Louise E. Moser and Laura K. Dillon and
P. Michael {Melliar-Smith} and George Kutty},
TITLE = {An Automata-Theoretic Decision Procedure for Propositional
Temporal Logic with Since and Until},
JOURNAL = {Fundamenta Informaticae},
MONTH = NOV,
YEAR = 1992,
VOLUME = 17,
NUMBER = 3,
PAGES = {271--282},
KEYWORDS = {}
}
@INPROCEEDINGS{rama92:fil,
AUTHOR = {Y. S. Ramakrishna and Laura K. Dillon and Louise E. Moser and
P. Michael {Melliar-Smith} and George Kutty},
TITLE = {An Automata-Theoretic Decision Procedure for Future
Interval Logic},
BOOKTITLE = {Proc. 12th Conf.\ Foundations of
Software Technology and Theoretical Computer Science},
MONTH = DEC,
PAGES = {51--67},
YEAR = 1992,
ADDRESS = {New Delhi},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 652,
PUBLISHER = {Springer-Verlag}
}
@ARTICLE{rama:rtfil-dp,
AUTHOR = {Y. S. Ramakrishna and Laura K. Dillon and Louise E. Moser
and P. Michael {Melliar-Smith} and George Kutty},
TITLE = {A Real-Time Interval Logic and its Decision Procedure},
JOURNAL = {Sadhana, Engineering Sciences Journal},
PUBLISHER = {Indian Academy of Sciences},
YEAR = 1996,
MONTH = APR,
VOLUME = 21,
NUMBER = 2,
PAGES = {147--184},
KEYWORDS = {}
}
@INPROCEEDINGS{rama:rtfil-decision-procedure,
AUTHOR = {Y. S. Ramakrishna and Laura K. Dillon and Louise E. Moser
and P. Michael {Melliar-Smith} and George Kutty},
TITLE = {A Real-Time Interval Logic and its Decision Procedure},
BOOKTITLE = {Proc.\ 13th Conf.\ Foundations of Software
Technology and Theoretical Computer Science},
MONTH = DEC,
YEAR = 1993,
PUBLISHER = {Springer-Verlag},
VOLUME = 761,
SERIES = {Lecture Notes in Computer Science},
ADDRESS = {Bombay, India},
PAGES = {173--192},
KEYWORDS = {}
}
@INPROCEEDINGS{rama93:really-visual-temporal-reasoning,
AUTHOR = {Y. S. Ramakrishna and P. Michael {Melliar-Smith}
and Louise E. Moser and Laura K. Dillon and George Kutty},
TITLE = {Really Visual Temporal Reasoning},
BOOKTITLE = {Proc. 14th RTSS},
MONTH = DEC,
YEAR = 1993,
ADDRESS = {Raleigh-Durham, NC},
PAGES = {262--273},
KEYWORDS = {}
}
@ARTICLE{rama96:tcs1,
AUTHOR = {Y. S. Ramakrishna and P. Michael {Melliar-Smith} and Louise E. Moser
and Laura K. Dillon and George Kutty},
TITLE = {Interval Logics and Their Decision Procedures, Part {I}: An
Interval Logic},
JOURNAL = {Theoretical Computer Science},
YEAR = 1996,
MONTH = OCT,
VOLUME = 166,
NUMBER = {1--2},
PAGES = {1--47},
NOTE = {},
KEYWORDS = {}
}
@ARTICLE{rama96:tcs2,
AUTHOR = {Y. S. Ramakrishna and P. Michael {Melliar-Smith} and Louise E. Moser
and Laura K. Dillon and George Kutty},
TITLE = {Interval Logics and Their Decision Procedures, Part {II}: A Real-Time
Interval Logic},
JOURNAL = {Theoretical Computer Science},
YEAR = 1996,
MONTH = DEC,
VOLUME = 170,
NUMBER = {1--2},
PAGES = {1--46},
NOTE = {},
KEYWORDS = {}
}
@ARTICLE{lites04,
AUTHOR = {A. Arora and P. Dutta and S. Bapat and V. Kulathumani
and H. Zhang
and V. Naik and V. Mittal and H. Cao and M. Demirbas and M. Gouda
and Y-R. Choi and T. Herman and S. S. Kulkarni and U. Arumugam
and M.
Nesterenko and A. Vora and M. Miyashita},
TITLE = {A Line in the sand: A wireless sensor network for target
detection,
classification, and tracking},
JOURNAL = {Computer Networks (Elsevier)},
YEAR = {2004},
URL = {http://www.cse.msu.edu/~sandeep/publications/lites04}
}
@ARTICLE{ck04,
AUTHOR = {G. Chakrabarti and S. Kulkarni},
TITLE = {Load Balancing and Resource Reservation in
Ad-hoc Networks},
JOURNAL = {Ad-Hoc Networks},
YEAR = {2004},
FIXURL = {http://www.cse.msu.edu/~sandeep/publications/ck04}
}
@ARTICLE{Stirewalt:scp04,
AUTHOR = {R. E. K. Stirewalt and Reimer Behrends and
Laura K. Dillon},
TITLE = {A model-based semantics for synchronization
contracts
in object-oriented languages },
JOURNAL = { Science of Computer Programming },
URL = { http://www.cse.msu.edu/~stire/Papers/scp04.pdf },
NOTE = { Accepted, pending revisions },
YEAR = 2004
}
@INPROCEEDINGS{lopstr04,
AUTHOR = {Sandeep S. Kulkarni and Borzoo Bonakdarpour
and Ali Ebnenasir},
TITLE = {Mechanical Verification of Automatic Synthesis
of
Fault-Tolerance},
BOOKTITLE = {Proceedings of the International Symposium on
Logic-based Program Synthesis and Transformation},
YEAR = {2004}
}
@INPROCEEDINGS{TimingPatterns-ASE04,
AUTHOR = {Sascha Konrad and Laura Campbell and Betty H.C. Cheng},
TITLE = {Automated Analysis of Timing Information in UML Diagrams},
BOOKTITLE = {Proc. of IEEE International Conference on Automated Software Engineering},
YEAR = {2004},
MONTH = {September},
ADDRESS = {Linz, Austria},
COMMENT = {short paper on timing extensions to requirements patterns and UML formalization framework}
}
@INPROCEEDINGS{multitolke04,
AUTHOR = {S. S. ~Kulkarni and A. ~Ebnenasir},
TITLE = {Automated Synthesis of Multitolerance},
BOOKTITLE = {Proceedings of the International Conference on Dependable Systems
and Networks, Palazzo dei Congressi, Florence, Italy, June 28 - July 1},
YEAR = {2004},
FIXURL = {http://www.cse.msu.edu/~sandeep/publications/ke04a}
}
@ARTICLE{sat04,
AUTHOR = {Ali Ebnenasir and Sandeep S. Kulkarni},
TITLE = {{SAT}-Based Synthesis of Fault-Tolerance},
JOURNAL = {Fast Abstracts of the International Conference
on Dependable
Systems and Networks, Palazzo dei Congressi, Florence, Italy, June 28 - July 1},
YEAR = 2004,
FIXURL = {http://www.cse.msu.edu/~sandeep/publications/ek04a}
}
@INPROCEEDINGS{ka04b,
AUTHOR = {S. S. Kulkarni and M(U). Arumugam},
TITLE = {Approximate Causal Observer},
BOOKTITLE = {Proceedings of the International Workshop on
Networked Sensing Systems (INSS)},
PAGES = {123-128},
MONTH = {June},
YEAR = {2004},
URL = {http://www.cse.msu.edu/~sandeep/publications/ka04b}
}
@INPROCEEDINGS{Stirewalt:asee04,
AUTHOR = { R. E. K. Stirewalt },
TITLE = { Teaching software engineering ``bottom up'' },
BOOKTITLE = { Proc. of the ASEE Annual Conference and
Exposition },
URL = { http://www.cse.msu.edu/~stire/Papers/asee04.doc
},
MONTH = {June},
YEAR = 2004
}
@INPROCEEDINGS{cbse7-04,
AUTHOR = {Sandeep Kulkarni and Karun Biyani},
TITLE = {Correctness of Component-based Adaptation},
BOOKTITLE = {Proceedings of the International Symposium on Component-based
Software Engineering},
YEAR = 2004,
MONTH = {May},
URL = {http://www.cse.msu.edu/~sandeep/publications/kb04a}
}
@INPROCEEDINGS{Sowell:wads04,
AUTHOR = { J. H. Sowell and R. E. K. Stirewalt },
TITLE = { Middleware reliability implementations
and connector wrappers },
BOOKTITLE = { Proc. of the ICSE Workshop on Architecting
Dependable Systems (WADS'04) },
URL = {http://www.cse.msu.edu/~stire/Papers/wads04.pdf },
MONTH = {May},
YEAR = 2004
}
@INPROCEEDINGS{ka04a,
AUTHOR = {S. S. Kulkarni and M(U). Arumugam},
TITLE = {{TDMA} Service for Sensor Networks},
BOOKTITLE = {Proceedings of the Third International Workshop on
Assurance in
Distributed Systems and Networks},
MONTH = {March},
YEAR = {2004},
URL = {http://www.cse.msu.edu/~sandeep/publications/ka04a}
}
@INPROCEEDINGS{ka03b,
AUTHOR = {S. S. Kulkarni and M(U). Arumugam},
TITLE = {Transformations for Write-All-With-Collision Model},
BOOKTITLE = {Proceedings of the International Conference on
Principles of
Distributed Systems (OPODIS)},
VOLUME = {LNCS:3144},
PAGES = {184-197},
MONTH = {December},
YEAR = {2003},
URL = {http://www.cse.msu.edu/~sandeep/publications/ka03b}
}
@ARTICLE{ComposableProxies,
AUTHOR = {P. K. McKinley and U. I. Padmanabhan and N. Ancha and S. M. Sadjadi},
TITLE = {Composable Proxy Services to Support Collaboration on the Mobile Internet},
JOURNAL = {IEEE Transactions on Computers (Special Issue on Wireless Internet)},
ABSTRACT = {This paper describes the design and operation of a composable
proxy infrastructure that enables mobile Internet users to
collaborate via heterogeneous devices and network connections.
The approach is based on detachable Java I/O streams, which
enable proxy filters and transcoders to be dynamically inserted,
removed, and reordered on a given data stream. Unlike conventional
Java I/O streams, detachable streams can be stopped, disconnected,
reconnected, and restarted. As such, they provide a convenient
method by which to support the dynamic composition of proxy services.
Moreover, use of the I/O stream abstraction enables network
distribution and stream adaptability to be implemented transparently
with respect to application components. The operation and implementation
of detachable streams are described. To evaluate the composable proxy
infrastructure, it is used to enhance interactive audio communication
among users of a Web-based collaborative computing framework.
Two forward error correction (FEC) proxylets are developed, one using
block erasure codes and the other using the GSM 06.10 encoding algorithm.
Separately, each type of FEC improves the ability of the audio stream
to tolerate errors in a wireless LAN environment. When composed in a
single proxy, however, they cooperate to correct additional types of burst
errors. Results are presented from a performance study conducted on a
mobile computing testbed.},
YEAR = {2003},
PAGES = {713-726},
MONTH = {June},
URL = {ftp://ftp.cse.msu.edu/pub/crg/PAPERS/mckinley-toc-si-revision.pdf}
}
@INPROCEEDINGS{kba03,
AUTHOR = {S. S. Kulkarni and K. N. Biyani and U. Arumugam},
TITLE = {Composing Distributed Fault-Tolerance Components},
BOOKTITLE = {Proceedings of the International Conference on
Dependable Systems
and Networks (DSN), Supplemental Volume, Workshop on Principle
s of Dependable Systems (PoDSy)},
PAGES = {W127-W136},
MONTH = {June},
YEAR = {2003},
URL = {http://www.cse.msu.edu/~sandeep/publications/kba03}
}
@INPROCEEDINGS{enhance03,
AUTHOR = {Sandeep S. Kulkarni and Ali Ebnenasir},
TITLE = {Enhancing The Fault-Tolerance of Nonmasking
Programs},
BOOKTITLE = {Proceedings of the 23rd IEEE International Conference on Distributed
Computing
Systems, Providence, Rhode Island USA, May 19-22},
YEAR = 2003,
URL = {http://www.cse.msu.edu/~sandeep/publications/ke03a}
}
@INPROCEEDINGS{ka03a,
AUTHOR = {S. S. Kulkarni and U. Arumugam},
TITLE = {Collision-Free Communication in Sensor Networks},
BOOKTITLE = {Proceedings of the Sixth Symposium on
Self-stabilizing Systems
(SSS), Springer},
VOLUME = {LNCS:2704},
PAGES = {17-31},
MONTH = {June},
YEAR = {2003},
URL = {http://www.cse.msu.edu/~sandeep/publications/ka03a}
}
@INPROCEEDINGS{gk02,
AUTHOR = {G. Chakrabarti and S. S. Kulkarni},
TITLE = {A Modified Approach to Dynamic Source Routing in Mobile
Ad-Hoc Networks},
BOOKTITLE = {Proceedings of AD-HOC NetwOrks and Wireless {(ADHOC-NOW)}},
YEAR = {2002},
ADDRESS = {Toronto, Canada},
MONTH = {September},
OPTKEY = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTPAGES = {},
OPTMONTH = {},
OPTNOTE = {},
OPTANNOTE = {},
URL = {http://www.cse.msu.edu/~sandeep/publications/adhocnow02/main.ps},
ABSTRACT = {To ensure uninterrupted communication in a mobile ad-hoc network,
efficient route discovery is crucial when nodes move and/or fail.
Hence, protocols such as Dynamic Source Routing (DSR) precompute
alternate routes before a node moves and/or fails. In this paper, we
modify the way these alternate routes are maintained and used in DSR,
and show that these modifications permit more efficient route
discovery when nodes move and/or fail. Our simulation results show
that maintenance of these alternate routes (without affecting the
route cache size at each router) increases the packet delivery ratio
without incurring any extra traffic overhead. We also show that our
approach enables us to provide QoS guarantees by ensuring that
appropriate bandwidth will be available for a flow even when nodes
move. Towards this end, we show how reservations can be made on the
alternate routes while maximizing the bandwidth usage in situations
where nodes do not move.
}
}
@ARTICLE{ChCM02.UML,
AUTHOR = {Laura A.~Campbell and Betty H.~C.~Cheng and William E.~McUmber and R.~E.~K.~Stirewalt},
TITLE = {Automatically Detecting and Visualizing Errors in UML Diagrams},
JOURNAL = {Requirements Engineering Journal},
OPTVOLUME = {37},
OPTNUMBER = {10},
OPTMONTH = {October},
YEAR = {2002},
NOTE = {(in press)},
KEY = {FM},
URL = {ftp://ftp.cse.msu.edu/pub/crg/PAPERS/rej02.pdf},
ABSTRACT = {UML has become the de facto standard for object-oriented modeling. Currently, UML comprises several different notations with no formal semantics attached to the individual diagrams or their integration, thus preventing rigorous analysis of the diagrams. Previously, we have developed a formalization framework that attaches formal semantics to a subset of UML diagrams used to model embedded systems. This paper describes automated structural and behavioral analyses applicable to UML diagrams using our formalization framework. In addition to intra- and inter-diagram consistency checks, we discuss how simulation and model checking can be used in tandem for behavioral analysis of the UML diagrams. Our tools also visually interpret the analysis results in terms of the original UML diagrams, thereby facilitating their correction and refinement. We illustrate these capabilities through the modeling and analysis of UML diagrams for an automotive industrial case study.
}
}
@INPROCEEDINGS{RE02-Reqts-Patterns,
AUTHOR = {Sascha Konrad and Betty H.~C. Cheng},
TITLE = {Requirements Patterns for Embedded Systems},
BOOKTITLE = {Proceedings of the IEEE Joint International Conference on Requirements Engineering (RE02)},
OPTCROSSREF = {},
OPTKEY = {},
OPTPAGES = {},
YEAR = {2002},
OPTEDITOR = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTSERIES = {},
ADDRESS = {Essen, Germany},
MONTH = {September},
OPTORGANIZATION = {IEEE Computer Society},
OPTPUBLISHER = {},
URL = {ftp://ftp.cse.msu.edu/pub/crg/PAPERS/re02.pdf},
ABSTRACT = {}
}
@INPROCEEDINGS{RHAS02-Reqts-Patterns-Constraints,
AUTHOR = {Sascha Konrad and Laura A.~Campbell and Betty H.~C. Cheng},
TITLE = {Adding Formal Specifications to Requirements Patterns},
BOOKTITLE = {Proceedings of the IEEE Requirements for High Assurance Systems (RHAS02)},
OPTCROSSREF = {},
OPTKEY = {},
OPTPAGES = {},
YEAR = {2002},
EDITOR = {C.~Heitmeyer and N.~Mead},
OPTVOLUME = {},
OPTNUMBER = {},
OPTSERIES = {},
ADDRESS = {Essen, Germany},
MONTH = {September},
OPTORGANIZATION = {IEEE Computer Society},
OPTPUBLISHER = {},
URL = {ftp://ftp.cse.msu.edu/pub/crg/PAPERS/rhas02.pdf},
ABSTRACT = {Embedded systems usually must achieve
a higher level of robustness and reliability because they control
real-world physical processes or devices upon which we depend,
frequently, in a critical way. Consequently, methods for modeling
and developing embedded systems and rigorously verifying behavior before
committing to code are increasingly important.
In order to use object-oriented development techniques and UML for
embedded systems,
we previously developed a framework for adding
formal semantics to a collection of UML diagrams that enable
the automated derivation of formal
language specifications for those diagrams.
Recently, we also identified a number of requirements patterns
for use in the development of
requirements and high-level design for embedded systems, and constructed
a requirements pattern template.
This paper describes how we have augmented the template to include
requirements constraints that might be applicable when using a given
pattern. With the ability to generate formal specifications from the UML
diagrams, these constraints can be analyzed using existing model checkers.
We also include a description of how the requirements patterns have been used
to model and formally analyze an automotive embedded system.
}
}
@ARTICLE{ChWa02.TSE,
AUTHOR = {Betty H.C. Cheng and
Enoch Y. Wang},
TITLE = {Formalizing and Integrating the Dynamic Model for
Object-Oriented Modeling},
JOURNAL = {IEEE Transactions on Software Engineering},
MONTH = {August},
YEAR = {2002},
OPTKEY = {},
VOLUME = {28},
NUMBER = {28},
PAGES = {747--762},
OPTANNOTE = {},
URL = {ftp://ftp.cse.msu.edu/pub/crg/PAPERS/tse02.pdf},
ABSTRACT = {}
}
@INPROCEEDINGS{ka02,
AUTHOR = {S. S. Kulkarni and A. Ebnenasir},
TITLE = {Complexity of Adding Failsafe Fault-tolerance},
BOOKTITLE = {Proceedings of the 22nd IEEE International
Conference on Distributed Computing
Systems},
YEAR = {2002},
OPTKEY = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTPAGES = {},
ADDRESS = {Vienna, Austria},
MONTH = {July},
NOTE = {},
OPTANNOTE = {},
URL = {http://www.cse.msu.edu/~sandeep/publications/icdcs02/main.ps},
ABSTRACT = {
In this paper, we focus our attention on the problem of automating the
addition of failsafe fault-tolerance where fault-tolerance is added to
an existing (fault-intolerant) program. A failsafe fault-tolerant
program satisfies its specification (including safety and liveness) in
the absence of faults. However, in the presence of faults, it
satisfies its safety specification. We present a somewhat unexpected
result that, in general, the problem of adding failsafe
fault-tolerance in distributed programs is NP-hard. Towards this end,
we reduce the 3-SAT problem to the problem of adding failsafe
fault-tolerance. We also identify a class of specifications, {\em
monotonic specifications} and a class of programs, {\em monotonic
programs}. Given a monotonic specification and a monotonic program,
we show that failsafe fault-tolerance can be added in polynomial time.
As an illustration, we show that the monotonicity restrictions are met
for commonly encountered problems such as Byzantine agreement,
distributed consensus, and atomic commitment. Finally, we argue that
the restrictions on the specifications and programs are necessary to
add failsafe fault-tolerance in polynomial time; we prove that if only
one of these conditions is satisfied, the addition of failsafe
fault-tolerance is still NP-hard.
}
}
@INPROCEEDINGS{kb02,
AUTHOR = {S. S. Kulkarni and B. Bruhadeshwar},
TITLE = {Critical Path in Secure Multicast
for Dynamic Groups},
BOOKTITLE = {Proceedings of the International Workshop on
Assurance in Distributed
Systems and Networks},
YEAR = {2002},
OPTKEY = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTPAGES = {},
ADDRESS = {Vienna, Austria},
MONTH = {July},
OPTANNOTE = {},
URL = {http://www.cse.msu.edu/~sandeep/publications/adsn02/main.ps},
ABSTRACT = {
In this paper, we focus on the problem of secure multicast in dynamic
groups. In this problem, a group of users communicate using a shared
key. Due to the dynamic nature of these groups, to preserve secrecy,
it is necessary to change the group key whenever the group membership
changes.
While the group key is being changed, the group communication needs to
be interrupted until the rekeying is complete. This interruption is
especially necessary if the rekeying is done because a user has left
(or is removed).
We split the rekeying cost into two parts: the cost of the critical path
--where each current user receives the new group key, and the cost of the
non-critical path --where each user receives any other keys that it
needs to obtain.
Then, we present two algorithms that show the trade off between the
cost of the critical path and the cost of the non-critical path.
We also compare our algorithms to previous algorithms and show that our
algorithms reduce the cost of the critical path while keeping the
total cost manageable.
}
}
@INPROCEEDINGS{RuSt:ase01,
AUTHOR = { S. Rugaber and R. E. K. Stirewalt },
TITLE = { Adequate reverse engineering },
BOOKTITLE = { Proceedings of the IEEE International Conference
on Automated Software Engineering },
MONTH = NOV,
YEAR = 2001
}
@INPROCEEDINGS{kac01,
AUTHOR = {S. S. Kulkarni and A. Arora and A. Chippada},
TITLE = {Polynomial time synthesis of Byzantine Agreement},
BOOKTITLE = {Proceedings of the Twentieth Symposium on Reliable
Distributed Systems},
YEAR = {2001},
OPTKEY = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTPAGES = {},
ADDRESS = {New Orleans, LA},
MONTH = {October},
OPTNOTE = {},
OPTANNOTE = {},
URL = {http://www.cse.msu.edu/~sandeep/publications/srds01/main.ps},
ABSTRACT = {
We present a polynomial time algorithm for automatic synthesis of
fault-tolerant distributed programs starting from fault-intolerant
versions of those programs. Since this synthesis problem is known to
be NP-hard, our algorithm relies on heuristics to reduce the
complexity. We demonstrate that our algorithm suffices to synthesize
an agreement program that tolerates a byzantine fault. We also show
that our algorithm suffices for the case where both byzantine and
failstop faults may occur. Finally, we describe an object-oriented
implementation of our algorithm.
}
}
@INPROCEEDINGS{kr01,
AUTHOR = {S. S. Kulkarni and Ravikant},
TITLE = {Stabilizing causal deterministic merge},
BOOKTITLE = {Proceedings of the Fifth Workshop on Self-Stabilization},
YEAR = {2001},
OPTKEY = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTPAGES = {},
MONTH = {October},
OPTNOTE = {},
OPTANNOTE = {},
URL = {http://www.cse.msu.edu/~sandeep/publications/wss01/main.ps},
ABSTRACT = {
In this paper, we present a causal deterministic merge program for
publish-subscribe systems. Our program ensures that if two subscribers
receive two messages then they receive them in the same order. Also,
it guarantees that the order in which a subscriber receives messages
is a linearization of the causal order among those messages. To
develop our program, we expect two guarantees from the underlying
system: the first guarantee deals with the difference between physical
clocks and the second guarantee deals with message delays. While
$O(n2)$ space is required for causal deterministic merge in
asynchronous systems, our program only uses $O(log \ n)$ space. We
also show how our program can be made stabilizing while using only a
bounded space. And, the recovery time for our program is proportional
to the guarantees made by the underlying system.
}
}
@INPROCEEDINGS{Compsac01-Panel,
AUTHOR = {Betty H.~C. Cheng},
TITLE = {A Metamodel-Based Approach to Formalizing {UML}},
BOOKTITLE = {Proceedings of the IEEE International Computer
Software and Applications Conference (COMPSAC01)},
OPTCROSSREF = {},
OPTKEY = {},
OPTPAGES = {},
YEAR = {2001},
OPTEDITOR = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTSERIES = {},
ADDRESS = {Naperville, Illinois},
MONTH = {October},
OPTORGANIZATION = {IEEE Computer Society},
OPTPUBLISHER = {},
OPTANNOTE = {},
ABSTRACT = {}
}
@INPROCEEDINGS{RE01-Poster,
AUTHOR = {Laura A. Campbell and Betty H.~C. Cheng},
TITLE = {Integrating Informal and Formal Approaches to
Requirements Modeling and Analysis},
BOOKTITLE = {Proceedings of the IEEE International Symposium on
Requirements Engineering (RE01)},
OPTCROSSREF = {},
OPTKEY = {},
OPTPAGES = {},
YEAR = {2001},
OPTEDITOR = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTSERIES = {},
ADDRESS = {Toronto, Canada},
MONTH = {August},
OPTORGANIZATION = {IEEE Computer Society},
OPTPUBLISHER = {},
OPTANNOTE = {},
ABSTRACT = {}
}
@ARTICLE{avru:design-methods,
AUTHOR = {George S. Avrunin and Laura K. Dillon and Jack C. Wileden
and William E. Riddle},
TITLE = {Constrained Expressions: {A}dding Analysis Capabilities
to Design Methods for Concurrent Software Systems},
JOURNAL = {IEEE Transactions on Software Engineering},
MONTH = FEB,
YEAR = {1986},
PAGES = {278--292},
VOLUME = {SE-12},
NUMBER = 12,
MYNOTE = {tse paper}
}
@TECHREPORT{avru:tr:ces-realtime,
AUTHOR = {George S. Avrunin and Laura K. Dillon and
Jack C. Wileden},
TITLE = {Constrained Expression Analysis of Real-Time Systems},
INSTITUTION = {Computer and Information Science Department},
YEAR = 1989,
NUMBER = {TR89-50},
ADDRESS = {University of Massachusetts},
MONTH = APR,
NOTE = {},
KEYWORDS = {real-time systems, constrained expressions, concurrent systems,
automated analysis},
ABSTRACT = {The constrained expression formalism and its associated
analysis techniques were originally developed for describing
and analyzing logical properties of concurrent system behavior.
We have recently begun exploring their application to analyzing
timing properties. In this paper we describe our initial approach
to constrained expression analysis of real-time systems.
We then discuss the prospects for extending both the
constrained expression formalism and our existing prototype
toolset to support analysis of real-time concurrent software systems.}
}
@INPROCEEDINGS{avru:experiments-automated-analysis,
AUTHOR = {George S. Avrunin and Laura K. Dillon and
Jack C. Wileden},
TITLE = {Experiments with Automated Constrained
Expression Analysis of Concurrent Software
Systems},
PAGES = {124--130},
KEYWORDS = {constrained expressions, concurrent systems, automated analysis,
experiments},
ABSTRACT = {It is unlikely that any single approach to analysis of concurrent
software systems will meet all the needs of software developers
throughout the development process. Thus, experimental evaluation
of different concurrent analysis techniques is needed to determine
their relative strengths and practical limitations. Such
evaluation requires automated tools implementing the analysis
techniques.
This paper describes a prototype toolset automating the constrained
expression approach to the analysis of concurrent software systems.
The results of preliminary experiments with the toolset are
reported and the implications of these experiments are discussed.}
}
@INPROCEEDINGS{avru:experiments-improved-ce-toolset,
AUTHOR = {George S. Avrunin and Ugo Buy and James C. Corbett
and Laura K. Dillon and
Jack C. Wileden},
TITLE = {Experiments with an Improved Constrained Expression
Toolset},
CROSSREF = {tav4},
PAGES = {178--187},
NOTE = {},
KEYWORDS = {}
}
@ARTICLE{avru:toolset-paper,
AUTHOR = {George S. Avrunin and Ugo A. Buy and James C. Corbett
and Laura K. Dillon and Jack C. Wileden},
TITLE = {Automated Analysis of Concurrent Systems with the Constrained
Expression Toolset},
JOURNAL = {IEEE Transactions on Software Engineering},
MONTH = NOV,
YEAR = 1991,
VOLUME = 17,
NUMBER = 11,
PAGES = {1204--1222},
KEYWORDS = {}
}
@ARTICLE{avru:realtime-paper,
AUTHOR = {George S. Avrunin and James C. Corbett
and Laura K. Dillon and Jack C. Wileden},
TITLE = {Automated Derivation of Time Bounds in Uniprocessor
Concurrent Systems},
JOURNAL = {IEEE Transactions on Software Engineering},
MONTH = SEP,
YEAR = 1994,
VOLUME = 20,
NUMBER = 9,
PAGES = {708--719},
KEYWORDS = {}
}
@INPROCEEDINGS{avru97:pirts,
AUTHOR = {George S. Avrunin and James C. Corbett
and Laura K. Dillon},
TITLE = {Analyzing Partially-Implemented Real-Time Systems},
BOOKTITLE = {Proc.\ 19th IEEE Inter.\ Conf.\ Software Engineering},
YEAR = 1997,
MONTH = MAY,
PAGES = {228--238},
ADDRESS = {Boston, MA},
NOTE = {},
KEYWORDS = {}
}
@ARTICLE{avru98:pirts,
AUTHOR = {George S. Avrunin and James C. Corbett
and Laura K. Dillon},
TITLE = {Analyzing Partially-Implemented Real-Time Systems},
JOURNAL = {IEEE Transactions on Software Engineering},
YEAR = 1998,
MONTH = AUG,
PAGES = {602--614},
VOLUME = 24,
NUMBER = 8,
KEYWORDS = {}
}
@INPROCEEDINGS{Behrends:cbse05,
AUTHOR = {R. Behrends and R. E. K. Stirewalt and L. K. Dillon},
TITLE = {A Component-Oriented Model for the Design of Safe
Multi-threaded Applications},
BOOKTITLE = {Proc.~8$th$ Inter. SIGSOFT Symp. on
Component-based Software Engineering (CBSE 2005):
Software Components at Work},
OPTCROSSREF = {},
OPTKEY = {},
OPTPAGES = {},
YEAR = {2005},
OPTEDITOR = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTSERIES = {},
OPTADDRESS = {},
MONTH = {May},
OPTORGANIZATION = {},
OPTPUBLISHER = {},
OPTANNOTE = {}
}
@INPROCEEDINGS{Behrends:saps04,
AUTHOR = { R. Behrends and R. E. K. Stirewalt and L. K. Dillon },
TITLE = { Avoiding serialization vulnerabilities through the
use of synchronization contracts },
BOOKTITLE = { Proc. of the Workshop on Specification and
Automated Processing of Security
Requirements },
PAGES = { 207--219 },
PUBLISHER = { Austrian Computer Society },
MONTH = SEP,
YEAR = 2004
}
@INPROCEEDINGS{chen:nco01,
AUTHOR = {Betty H. Cheng and Laura K. Dillon and
R. E. Kurt Stirewalt and Phillip McKinley and Sandeep Kulkarni
and Jaejin Lee},
TITLE = {Automated Development and Run-Time Adaptation of Interactive
Distributed Applications},
BOOKTITLE = {NCO Workshop on New Visions for Software Design},
YEAR = 2001,
MONTH = DEC,
NOTE = {http://www.isis.vanderbilt.edu/sdp/Papers/Papers.htm}
}
@UNPUBLISHED{dill:tse02-subm,
AUTHOR = {Laura K. Dillon and R. E. K. Stirewalt},
TITLE = {Inference Graphs: A Computational Structure Supporting
Generation of Customizable and Correct Analysis
Components },
NOTE = {Under review},
OPTKEY = {},
OPTMONTH = {},
OPTYEAR = {},
OPTANNOTE = {}
}
@ARTICLE{dillon04:ICSESpecialIssue,
AUTHOR = {Laura K. Dillon and Walter Tichy},
TITLE = {Guest Editors' Introduction: 2003 International Conference
on Software Engineering},
JOURNAL = {IEEE Transactions on Software Engineering},
YEAR = {2004},
OPTKEY = {},
VOLUME = {30},
NUMBER = {6},
PAGES = {353-354},
OPTMONTH = {},
OPTNOTE = {},
OPTANNOTE = {}
}
@ARTICLE{dill:tse03,
AUTHOR = {Laura K. Dillon and R. E. K. Stirewalt},
TITLE = {Inference Graphs: A Computational Structure Supporting
Generation of Customizable and Correct Analysis},
JOURNAL = {IEEE Transactions on Software Engineering},
YEAR = {2003},
VOLUME = {29},
NUMBER = {2},
PAGES = {133--150},
MONTH = FEB,
OPTNOTE = {},
OPTANNOTE = {}
}
@UNPUBLISHED{dill:icse02-subm,
AUTHOR = {Laura K. Dillon and R. E. Kurt Stirewalt},
TITLE = {Proof of Correctness of a Transparent Design Abstraction},
NOTE = {Submitted to ICSE'02}
}
@INPROCEEDINGS{dill:icse01b,
AUTHOR = { L. K. Dillon and R. E. K. Stirewalt },
TITLE = { Lightweight Analysis of Operational Specifications
Using Inference Graphs },
BOOKTITLE = { Proc. 2001 IEEE Inter.\ Conf.\ Software Engineering},
YEAR = 2001,
PAGES = { 57--67},
ADDRESS = {Toronto},
MONTH = MAY
}
@TECHREPORT{dill:tr:filToLtl,
AUTHOR = {Laura K. Dillon},
TITLE = {Translation of Future Interval Logic into Linear-Time Temporal Logic},
NUMBER = {MSU-CSE-99-32},
INSTITUTION = {Computer Science and Engineering, Michigan State University},
ADDRESS = {East Lansing, Michigan},
ABSTRACT = {This report documents a procedure for translating formulas from
a subset of Future Interval Logic (FIL) into Linear-time Temporal
Logic (LTL). FIL is the textual representation used for
defining the semantics of Graphical Interval Logic
(GIL), a temporal logic with an intuitive
graphical representation similar to the timelines frequently used by
system designers,
but with a formal semantics.
It will provide a cannonical form for a specification wizard currently
under development and is the internal form used by the GIL
toolset. The specification wizard will apply the translation
procedure described in the report to generate property specifications
in LTL. The resulting
specifications are intended for use with finite-state verification tools
such as SPIN.},
KEYWORDS = {temporal logic, Graphical Interval Logic, property specification},
NOTE = {},
MONTH = {September},
YEAR = {99},
AUTHOR1_EMAIL = {ldillon@cse.msu.edu},
PAGES = {28},
FILE = {/user/web/htdocs/publications/tech/TR/MSU-CSE-99-32.ps}
}
@INPROCEEDINGS{dill:fse96,
AUTHOR = {Laura K. Dillon and Y. S. Ramakrishna},
TITLE = {Generating Oracles From Your Favorite Temporal
Specifications},
BOOKTITLE = {Proc.\ 1996 ACM SIGSOFT ACM SIGSOFT Symp.\ Foundations of Software Engineering},
YEAR = 1996,
MONTH = OCT,
PAGES = {106--117},
ADDRESS = {San Francisco},
KEYWORDS = {}
}
@UNPUBLISHED{dill:fse96-subm,
AUTHOR = {Laura K. Dillon and Y. S. Ramakrishna},
TITLE = {Generating Oracles From Your Favorite Temporal
Specifications},
NOTE = {Submitted}
}
@UNPUBLISHED{dill:fse94-subm,
AUTHOR = {Laura K. Dillon and Qing Yu},
TITLE = {Oracles for Checking Temporal Properties of Concurrent
Systems},
NOTE = {Submitted}
}
@INPROCEEDINGS{dill:gil-oracle-paper,
AUTHOR = {Laura K. Dillon and Qing Yu},
TITLE = {Oracles for Checking Temporal Properties of Concurrent
Systems},
CROSSREF = {fse94},
PAGES = {140--153},
NOTE = {}
}
@INPROCEEDINGS{dill:qw95,
AUTHOR = {Laura K. Dillon},
TITLE = {Temporal oracles for Testing and Debugging Concurrent Software
Systems},
BOOKTITLE = {Proc.\ 8th Inter.\ Software Quality Week},
ADDRESS = {San Francisco},
MONTH = MAY,
YEAR = 1995,
NOTE = {Paper 3-T-4}
}
@ARTICLE{dill:task-dependence-and-termination,
AUTHOR = {Laura K. Dillon},
TITLE = {Task Dependence and Termination in {A}da},
JOURNAL = {ACM Trans.\ Software Engineering and Methodology},
MONTH = JAN,
YEAR = 1997,
PAGES = {80--110},
NOTE = {},
KEYWORDS = {}
}
@ARTICLE{dill:jvlc93,
AUTHOR = {Laura K. Dillon and George Kutty and
Melliar-Smith, P. Michael and Louise E. Moser
and Y. S. Ramakrishna},
TITLE = {Visual Specifications for Temporal Reasoning},
JOURNAL = {Journal of Visual Languages and Computing},
YEAR = 1994,
NUMBER = 1,
VOLUME = 5,
MONTH = MAR,
PAGES = {61--81},
KEYWORDS = {}
}
@INPROCEEDINGS{dill:graphical-specifications-for-concurrent-software-systems,
AUTHOR = {Laura K. Dillon and George Kutty and
Louise E. Moser and Melliar-Smith, P. Michael
and Y. S. Ramakrishna},
TITLE = {Graphical Specifications for Concurrent Software Systems},
BOOKTITLE = {Proc.\ 14th IEEE Inter.\ Conf.\ Software Engineering},
YEAR = 1992,
PAGES = {213--224},
ADDRESS = {Melbourne},
MONTH = MAY,
NOTE = {},
KEYWORDS = {}
}
@ARTICLE{dill:gil-tosem-paper,
AUTHOR = {Laura K. Dillon and George Kutty and
Louise E. Moser and Melliar-Smith, P. Michael
and Y. S. Ramakrishna},
TITLE = {A Graphical Interval Logic for Specifying Concurrent
Systems},
JOURNAL = {ACM Trans.\ Software Engineering and Methodology},
MONTH = APR,
YEAR = 1994,
VOLUME = 3,
NUMBER = 2,
PAGES = {131--165},
NOTE = {}
}
@ARTICLE{dill:issta96-best-papers,
AUTHOR = {Laura K.\ Dillon and Steven Zeil},
TITLE = {Introduction to the Special Section
},
JOURNAL = {IEEE Transactions on Software Engineering},
MONTH = JUL,
YEAR = 1996,
VOLUME = 22,
NUMBER = 7,
PAGES = 441,
NOTE = {}
}
@UNPUBLISHED{dill:gil-tosem-paper-subm,
AUTHOR = {Laura K. Dillon and George Kutty and
Louise E. Moser and Melliar-Smith, P. Michael
and Y. S. Ramakrishna},
TITLE = {A Graphical Interval Logic for Specifying Concurrent Systems},
NOTE = {Submitted. Available in directory /pub/gil
at ftp.cs.ucsb.edu by anonymous ftp}
}
@TECHREPORT{dill:gil-tosem-paper-tr,
AUTHOR = {Laura K. Dillon and George Kutty and
Louise E. Moser and Melliar-Smith, P. Michael
and Y. S. Ramakrishna},
TITLE = {A Graphical Interval Logic for Specifying Concurrent Systems},
INSTITUTION = {Computer Science Department},
YEAR = 1993,
NUMBER = {TRCS 93-16},
ADDRESS = {University of California, Santa Barbara},
MONTH = JUL,
NOTE = {},
KEYWORDS = {}
}
@ARTICLE{dill:visual-execution-model-ada-tasking,
AUTHOR = {Laura K. Dillon},
TITLE = {A Visual Execution Model for {A}da Tasking},
JOURNAL = {ACM Trans.\ Software Engineering and Methodology},
MONTH = OCT,
YEAR = 1993,
VOLUME = 2,
NUMBER = 4,
PAGES = {311--345},
KEYWORDS = {}
}
@UNPUBLISHED{dill:task-dependence-termination,
AUTHOR = {Laura K. Dillon},
TITLE = {Task Dependence and Termination in {A}da},
NOTE = {Under revision}
}
@UNPUBLISHED{dill:constraint-eliminator,
AUTHOR = {Laura K. Dillon and George Walden},
TITLE = {A Prototype Constraint Eliminator for Constrained Expression
Representations},
NOTE = {In preparation.}
}
@ARTICLE{dill:broad-appl,
AUTHOR = {Laura K. Dillon and George S. Avrunin and
Jack C. Wileden},
TITLE = {Constrained Expressions: {T}oward Broad Applicability
of Analysis Methods for Distributed Software Systems},
JOURNAL = {ACM Transactions on Programming Languages and
Systems},
MONTH = JUL,
YEAR = 1988,
VOLUME = 10,
NUMBER = 3,
PAGES = {374--402},
KEYWORDS = {}
}
@TECHREPORT{dill:cedl-ces,
AUTHOR = {Laura K. Dillon},
TITLE = {A Constrained Expression Formulation of {CEDL}},
INSTITUTION = {Computer Science Department},
ADDRESS = {University of California, Santa Barbara 93106},
NUMBER = {TRCS86-22},
MONTH = NOV,
YEAR = {1986},
MYNOTE = {gives the translation rules and constraint templates
for deriving constrained expressions from CEDL designs}
}
@PHDTHESIS{dill:disser,
AUTHOR = {Laura K. Dillon},
TITLE = {Analysis of Distributed Systems using Constrained Expressions},
SCHOOL = {University of Massachusetts},
ADDRESS = {Amherst, MA 01003},
MONTH = SEP,
YEAR = {1984},
MYNOTE = {my dissertation}
}
@ARTICLE{dill:gen-saf,
AUTHOR = {Laura K. Dillon},
TITLE = {Verifying General Safety Properties of {A}da Tasking Programs},
JOURNAL = {IEEE Transactions on Software Engineering},
MONTH = JAN,
YEAR = 1990,
VOLUME = 16,
NUMBER = 1,
PAGES = {51--63},
KEYWORDS = {concurrency, symbolic execution, formal specification and
verification, isolation approach, safety properties, Ada tasking}
}
@ARTICLE{dill:iso-app,
AUTHOR = {Laura K. Dillon},
TITLE = {An Isolation Approach to Symbolic Execution-Based
Verification of {A}da Tasking Programs},
JOURNAL = {Journal of Systems and Software},
MONTH = MAR,
YEAR = 1991,
VOLUME = 14,
NUMBER = 3,
PAGES = {183--198},
KEYWORDS = {concurrency, symbolic execution, formal specification and
verification, isolation approach, Ada tasking}
}
@TECHREPORT{dill:over-cedl,
AUTHOR = {Laura K. Dillon},
TITLE = {Overview of the Constrained Expression Design Language},
INSTITUTION = {Computer Science Department},
ADDRESS = {University of California, Santa Barbara 93106},
NUMBER = {TRCS86-21},
MONTH = OCT,
YEAR = {1986},
MYNOTE = {overview of CEDL}
}
@INPROCEEDINGS{dill:se-comp,
AUTHOR = {Laura K. Dillon and Richard A. Kemmerer and
Linda J. Harrison},
TITLE = {An Experience with Two Symbolic Execution-based Approaches
to Formal Verification of {A}da Tasking Programs},
BOOKTITLE = {Proc. 2nd Workshop Software Testing, Verification
and Analysis},
YEAR = 1988,
PAGES = {114--122},
PUBLISHER = {IEEE Computer Society Press},
MONTH = JUL,
NOTE = {},
KEYWORDS = {symbolic execution, Ada tasking programs, testing
and verification workshop, verification, concurrency, parallel programs
interleaving approach, isolation approach, symbolic testing}
}
@INPROCEEDINGS{dill:se-for-ada,
AUTHOR = {Laura K. Dillon},
TITLE = {Symbolic Execution-Based Verification of {A}da Tasking Programs},
BOOKTITLE = {Proc.\ 3rd Intl.\ IEEE Conf.\ Ada
Applications and Environments},
YEAR = 1988,
PAGES = {3--13},
PUBLISHER = {IEEE Computer Society Press},
ADDRESS = {Manchester, NH},
MONTH = MAY,
NOTE = {},
KEYWORDS = {symbolic execution, Ada tasking programs,
verification, concurrent systems, safety properties}
}
@TECHREPORT{dill:simp-red,
AUTHOR = {Laura K. Dillon},
TITLE = {Simplification and Reduction of {CEDL} Constrained Expressions},
INSTITUTION = {Computer Science Department},
ADDRESS = {University of California, Santa Barbara 93106},
NUMBER = {TRCS86-29},
MONTH = NOV,
YEAR = {1986},
MYNOTE = {simplification and reduction procedure}
}
@TECHREPORT{dill:tr:broad-appl,
AUTHOR = {Laura K. Dillon and George S. Avrunin and
Jack C. Wileden},
TITLE = {Constrained Expressions: {T}oward Broad Applicability
of Analysis Methods for Distributed Software Systems},
INSTITUTION = {Computer Science Department},
ADDRESS = {University of California, Santa Barbara 93106},
NUMBER = {TRCS 86-12},
MONTH = MAY,
YEAR = {1986},
NOTE = {{\em ACM Transactions on Programming Languages
and Systems, 1988}},
MYNOTE = {broad applicability paper. submitted to toplas.
shows how to get constrained expressions from
SDYMOL designs, CSP programs and
annotated Petri nets}
}
@TECHREPORT{dill:tr:se-comp,
AUTHOR = {Laura K. Dillon and Richard A. Kemmerrer and
Linda J. Harrison},
TITLE = {An Experience with Two Symbolic Execution-based Approaches
to Formal Verification of {A}da Tasking Programs},
INSTITUTION = {Computer Science Department},
YEAR = 1988,
NUMBER = {TRCS 88-6},
ADDRESS = {University of California, Santa Barbara 93106},
MONTH = MAR,
NOTE = {{\it Proc. of Second Workshop on Software Testing,
Verification and Analysis}, July 1988},
KEYWORDS = {symbolic execution, Ada tasking programs, testing
and verification workshop, verification, concurrency, parallel programs
interleaving approach, isolation approach, symbolic testing}
}
@TECHREPORT{dill:tr:se-for-ada,
AUTHOR = {Laura K. Dillon},
TITLE = {Symbolic Execution-Based Verification of {A}da Tasking Programs},
INSTITUTION = {Computer Science Department},
YEAR = 1988,
ADDRESS = {University of California, Santa Barbara 93106},
MONTH = MAR,
NUMBER = {TRCS 88-11},
NOTE = {{\it Proc. of Third International
IEEE Conference on Ada Applications and Environments}, May 1988},
KEYWORDS = {symbolic execution, Ada tasking programs,
verification, concurrent systems, safety properties}
}
@TECHREPORT{dill:tr:se1,
AUTHOR = {Laura K. Dillon},
TITLE = {Verification of Ada Tasking Programs Using Symbolic Execution,
Part {I}: Partial Correctness},
INSTITUTION = {Computer Science Department},
YEAR = 1987,
NUMBER = {TRCS 87-20},
ADDRESS = {University of California, Santa Barbara 93106},
MONTH = OCT,
KEYWORDS = {symbolic execution, Ada tasking programs,
verification, concurrent systems, partial correctness},
MYNOTE = {early draft of dill:iso-app}
}
@TECHREPORT{dill:tr:se2,
AUTHOR = {Laura K. Dillon},
TITLE = {Verification of Ada Tasking Programs Using Symbolic Execution,
Part {II}: General Safety Properties},
INSTITUTION = {Computer Science Department},
YEAR = 1987,
NUMBER = {TRCS 87-21},
ADDRESS = {University of California, Santa Barbara 93106},
MONTH = OCT,
KEYWORDS = {symbolic execution, Ada tasking programs,
verification, concurrent systems, safety properties},
MYNOTE = {early draft of dill:gen-saf}
}
@ARTICLE{dill:using-se-verification-ada-tasking,
AUTHOR = {Laura K. Dillon},
TITLE = {Using Symbolic Execution for Verification of {A}da Tasking
Programs},
JOURNAL = {ACM Transactions on Programming Languages and
Systems},
MONTH = OCT,
YEAR = 1990,
VOLUME = 12,
NUMBER = 4,
PAGES = {643--669},
KEYWORDS = {}
}
@UNPUBLISHED{dill:critical-gaps,
AUTHOR = {Laura K. Dillon},
TITLE = {Critical Gaps in Software Validation},
NOTE = {Invited paper for {\em SDS Testing and Evaluation Technology
Workshop}, Institute for Denfese Analysis, Washington D.C.},
MONTH = SEP,
YEAR = 1988
}
@UNPUBLISHED{dill:validation-concurrent-realtime-software-systems,
AUTHOR = {Laura K. Dillon},
TITLE = {Research on Validation of Concurrent and Real-Time Software
Systems},
NOTE = {Invited paper for {\em ONR Workshop on Directions
in Software Analysis and Testing}},
MONTH = AUG,
YEAR = 1989
}
@INPROCEEDINGS{dill:il-actions-and-events,
AUTHOR = {Laura K. Dillon and P. Michael {Melliar-Smith} and
Louise E. Moser and Y. S. Ramakrishna},
TITLE = {An Interval Logic Based on Actions and Events},
PAGES = {33--46},
CROSSREF = {berkeley-workshop-temporal-and-realtime-specs},
KEYWORDS = {}
}
@ARTICLE{dillon:editorial-icse2003-si,
AUTHOR = {Laura K. Dillon and Walter F. Tichy},
TITLE = {Guest Editors' Introduction: 2003 International
Conference on Software Engineering},
JOURNAL = {IEEE Transactions on Software Engineering},
YEAR = {2004},
OPTKEY = {},
VOLUME = {30},
NUMBER = {6},
PAGES = {353--354},
OPTMONTH = {},
OPTNOTE = {},
OPTANNOTE = {}
}
@UNPUBLISHED{gree89,
AUTHOR = {Jack Greenbaum and Russel Revlin and Laura Dillon},
TITLE = {Explorations in Parallel Semantic Systems: Test of
Psychological Properties of Data-Flow Semantic Networks},
YEAR = 1989,
KEYWORDS = {semantic networks, concurrent logic programming,
data-flow network, psychological theories of conceptual knowledge},
ABSTRACT = {This paper examines a data structure borrowed from Artificial
Intelligence research for representing parallel search through a
semantic network. The data structure, called a "dataflow semantic
network", is specified using predicate logic and can be realized
by a network of communicating processors. This data structure
offers a concrete instantiation of the implicit assumptions
made by many psychological models of semantic structure.
We present here a true parallel processing model that seeks to
simulate retrieval from semantic memory using the data-flow
network. The findings from this exploration are compared
against acknowledge benchmark values for human retrieval
from conceptual knowledge. While the data structure has
a number of properties that make it attractive in the development
of psychological theories of conceptual knowledge, it exhibits
serious limitations in its ability to account for fundamental
benchmarks of human semantic retrieval.}
}
@INPROCEEDINGS{keye99:spin-case-study,
AUTHOR = {David S. Keyes and Laura K. Dillon and Moon Jung Chung},
TITLE = {Analysis of a Scheduler for a {CAD} Framework},
BOOKTITLE = {Proc. 21$^{\rm st}$ IEEE Inter.\ Conf.\ Software Engineering},
YEAR = 1999,
PAGES = {152--162},
MONTH = MAY,
ADDRESS = {Los Angeles, CA},
ABSTRACT = {}
}
@INPROCEEDINGS{kutt94:fo-fil,
AUTHOR = {George Kutty and Louise E. Moser and P.~Michael
Melliar-Smith and Laura K. Dillon and Y. S. Ramakrishna},
TITLE = {First-Order Future Interval Logic},
BOOKTITLE = {Proc.\ 1st Inter.\ Conf.\ Temporal Logic},
EDITOR = {Dov M.\ Gabbay and Hans J{\"u}rgen Ohlbach},
YEAR = 1994,
MONTH = JUL,
PAGES = {195--209},
PUBLISHER = {Springer-Verlag},
ADDRESS = {Bonn, Germany},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = 827,
NOTE = {}
}
@ARTICLE{kutt:axiomatization-of-ils,
AUTHOR = {George Kutty and Louise E. Moser and P.~Michael
Melliar-Smith and Y. S. Ramakrishna and Laura K. Dillon},
TITLE = {Axiomatizations of Interval Logics},
JOURNAL = {Fundamenta Informaticae},
MONTH = DEC,
YEAR = 1995,
VOLUME = 24,
NUMBER = 4,
PAGES = {313--331},
KEYWORDS = {}
}
@INPROCEEDINGS{kutt93:cav-paper,
AUTHOR = {George Kutty and Y. S. Ramakrishna and Louise E. Moser and
Laura K. Dillon and P.~Michael Melliar-Smith},
TITLE = {A Graphical Interval Logic Toolset for Verifying Concurrent
Systems},
BOOKTITLE = {Proc.\ 4th Conf.\ Computer Aided Verification},
YEAR = 1993,
PAGES = {138--153},
ADDRESS = {Elounda, Greece},
MONTH = JUL,
SERIES = {Lecture Notes in Computer Science},
VOLUME = 697,
PUBLISHER = {Springer-Verlag},
KEYWORDS = {}
}
@INPROCEEDINGS{kutt:svl93,
AUTHOR = {George Kutty and Laura K. Dillon and Louise E. Moser and
P.~Michael Melliar-Smith and Y. S. Ramakrishna},
TITLE = {Visual Tools for Temporal Reasoning},
CROSSREF = {svl93},
PAGES = {152--159},
NOTE = {},
KEYWORDS = {}
}
@INPROCEEDINGS{kutt91,
AUTHOR = {George Kutty and Y. S. Ramakrishna and Laura K. Dillon and
Louise E. Moser and P. Michael {Melliar-Smith}},
TITLE = {Specification of a Communication Protocol in Graphical
Interval Logic},
BOOKTITLE = {Proc.\ IEE Inter.\ Conf.\ Information Engineering},
YEAR = 1991,
PAGES = {432--441},
ADDRESS = {Singapore},
MONTH = DEC,
MYNOTE = {GIL specification for the sliding window protocol;
it uses an old version of the graphical syntax},
KEYWORDS = {}
}
@ARTICLE{MultimediaInstructionLab,
AUTHOR = {Philip K. McKinley and Betty H.C. Cheng and Juyang Weng},
TITLE = {Integrating Multimedia Technology into the Undergraduate Curriculum},
JOURNAL = {International Journal of Engineering Education},
NOTE = {(in press)},
YEAR = {2005},
COMMENT = { report of experiences with using SGI machines and
multimedia software for teaching software
engineering, networking, and graphics undergraduate
courses.}
}
@MISC{TM05.TON,
AUTHOR = {C. Tang and P. K. McKinley},
TITLE = {Topology-Aware Overlay Path Probing},
NOTE = {submitted to {\it IEEE/ACM Transactions on Networking}},
YEAR = {2005}
}
@MISC{TM05.DMPROBE.TPDS,
AUTHOR = {C. Tang and P. K. McKinley},
TITLE = {A Distributed Approach to Path Monitoring in Topology-Aware Overlay Networks},
NOTE = {submitted to {\it IEEE Transactions on Parallel and Distributed Systems}},
YEAR = {2005}
}
@MISC{TM05.iMOBIF.TPDS,
AUTHOR = {C. Tang and P. K. McKinley},
TITLE = {Energy Optimization under Informed Mobility},
NOTE = {submitted to {\it IEEE Transactions on Parallel and Distributed Systems}},
YEAR = {2005}
}
@ARTICLE{McKinley.Computer.2004,
AUTHOR = {P. K. McKinley and S. M. Sadjadi and E. P. Kasten and B. H. C. Cheng},
TITLE = {Composing Adaptive Software},
JOURNAL = {IEEE Computer},
VOLUME = {37},
NUMBER = {7},
OPTMONTH = {July},
YEAR = {2004},
PAGES = {56-64},
URL = {http://www.cse.msu.edu/rapidware/survey}
}
@ARTICLE{MPAS03.TC,
AUTHOR = {P. K. McKinley and U. I. Padmanabhan and N. Ancha and S. M. Sadjadi},
TITLE = {Composable Proxy Services to Support Collaboration on the Mobile Internet},
JOURNAL = {IEEE Transactions on Computers (Special Issue on Wireless Internet)},
ABSTRACT = {This paper describes the design and operation of a composable
proxy infrastructure that enables mobile Internet users to
collaborate via heterogeneous devices and network connections.
The approach is based on detachable Java I/O streams, which
enable proxy filters and transcoders to be dynamically inserted,
removed, and reordered on a given data stream. Unlike conventional
Java I/O streams, detachable streams can be stopped, disconnected,
reconnected, and restarted. As such, they provide a convenient
method by which to support the dynamic composition of proxy services.
Moreover, use of the I/O stream abstraction enables network
distribution and stream adaptability to be implemented transparently
with respect to application components. The operation and implementation
of detachable streams are described. To evaluate the composable proxy
infrastructure, it is used to enhance interactive audio communication
among users of a Web-based collaborative computing framework.
Two forward error correction (FEC) proxylets are developed, one using
block erasure codes and the other using the GSM 06.10 encoding algorithm.
Separately, each type of FEC improves the ability of the audio stream
to tolerate errors in a wireless LAN environment. When composed in a
single proxy, however, they cooperate to correct additional types of burst
errors. Results are presented from a performance study conducted on a
mobile computing testbed.},
YEAR = {2003},
PAGES = {713-726},
MONTH = {June},
URL = {ftp://ftp.cse.msu.edu/pub/crg/PAPERS/mckinley-toc-si-revision.pdf}
}
@ARTICLE{McTM01.TPDS,
AUTHOR = {Philip K. McKinley and Chiping Tang and Arun P. Mani},
TITLE = {A Study of Adaptive Forward Error Correction for for Wireless Collaborative Computing},
JOURNAL = {IEEE Transactions on Parallel and Distributed Systems},
MONTH = {September},
YEAR = {2002},
OPTKEY = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTPAGES = {},
OPTANNOTE = {},
URL = {ftp://ftp.cse.msu.edu/pub/crg/PAPERS/mckinley-tpds-02.ps.gz},
ABSTRACT = {
This paper addresses the problem of reliably multicasting web
resources across wireless local area networks (WLANs) in support
of collaborative computing applications. An adaptive forward
error correction (FEC) protocol is described, which adjusts the
level of redundancy in the data stream in response to packet loss
conditions. The proposed protocol is intended for use on a proxy
server that supports mobile users on a WLAN. The software
architecture of the proxy service and the operation of the
adaptive FEC protocol are described. The performance of the
protocol is evaluated using both experimentation on a mobile
computing testbed as well as simulation. The results of the
performance study show that the protocol can quickly accommodate
worsening channel characteristics in order to reduce delay and
increase throughput for reliable multicast channels.
}
}
@ARTICLE{DSONLINE-2002,
AUTHOR = {Philip K. McKinley and Kurt Stirewalt and Betty H.C. Cheng and Laura K. Dillon and Sandeep S. Kulkarni},
TITLE = {Interactive Distributed Applications and the Computer Science Curriculum},
JOURNAL = {IEEE Distributed Systems Online},
MONTH = {October},
YEAR = {2002},
URL = {}
}
@INPROCEEDINGS{SM05.TAI.ICAC,
AUTHOR = {S. M. Sadjadi and P. K. McKinley},
TITLE = {Using Transparent Shaping and Web Services to Support
Self-Management of Composite Systems},
BOOKTITLE = {Proceedings of the Second IEEE International Conference on Autonomic Computing (ICAC)},
YEAR = {2005},
ADDRESS = {Seattle, Washington},
MONTH = {June}
}
@INPROCEEDINGS{FCSM05.TRAP.DEAS,
AUTHOR = {S. Fleming and B. H. C. Cheng and R. E. K. Stirewalt and P. K. McKinley},
TITLE = {An Approach to Implementing Dynamic Adaptation in C++},
BOOKTITLE = {Proceedings of the ICSE Workshop on Design and Evolution of Autonomic Application Software (DEAS)},
YEAR = {2005},
ADDRESS = {St. Louis, Missouri},
MONTH = {May}
}
@INPROCEEDINGS{SMC05.TS.DEAS,
AUTHOR = {S. M. Sadjadi and P. K. McKinley and B. H. C. Cheng},
TITLE = {Transparent Shaping of Existing Software to Support Pervasive and Autonomic Computing},
BOOKTITLE = {Proceedings of the ICSE Workshop on Design and Evolution of Autonomic Application Software (DEAS)},
YEAR = {2005},
ADDRESS = {St. Louis, Missouri},
MONTH = {May}
}
@INPROCEEDINGS{TM05.TAROM.ADSN,
AUTHOR = {C. Tang and P. K. McKinley},
TITLE = {Improving Mutipath Reliability in Topology-Aware Overlay Networks},
BOOKTITLE = {Proceedings of the Fourth International Workshop on Assurance
in Distributed Systems and Networks (ADSN), held in conjunction
with the 25th IEEE International Conference on Distributed Computing Systems},
YEAR = {2005},
ADDRESS = {Columbus, Ohio},
MONTH = {June}
}
@INPROCEEDINGS{TM05.iMOBIF.WWAN,
AUTHOR = {C. Tang and P. K. McKinley},
TITLE = {{iMobif}: An Informed Mobility Framework for Energy Optimization in Wireless Ad Hoc Networks},
BOOKTITLE = {Proceedings of the Second International Workshop on Wireless Ad Hoc
Networking (WWAN), in conjunction with the 25th IEEE International
Conference on Distributed Computing Systems},
YEAR = {2005},
ADDRESS = {Columbus, Ohio},
MONTH = {June}
}
@INPROCEEDINGS{KaMc.MESO.ICDL04,
AUTHOR = {E. P. Kasten and P. K. McKinley},
TITLE = {MESO: Perceptual memory to support online learning in adaptive software},
BOOKTITLE = {Proceedings of the 3rd International Conference on Development and Learning (ICDL'04)},
PAGES = {},
YEAR = {2004},
OPTEDITOR = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTSERIES = {},
ADDRESS = {La Jolla, California},
MONTH = {October},
OPTORGANIZATION = {},
OPTPUBLISHER = {},
OPTANNOTE = {},
FIXURL = {},
ABSTRACT = {}
}
@INPROCEEDINGS{M2.RM2004,
AUTHOR = {Z. Yang and Z. Zhou and B. H. C. Cheng and P. K. McKinley},
TITLE = {Enabling Collaborative Adaptation across Legacy Components},
BOOKTITLE = {Proceedings of the Third Workshop on Reflective and Adaptive Middleware, in conjunction with Middleware'04},
PAGES = {},
YEAR = {2004},
OPTEDITOR = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTSERIES = {},
ADDRESS = {Toronto, Ontario, Canada},
MONTH = {October},
OPTORGANIZATION = {},
OPTPUBLISHER = {},
OPTANNOTE = {},
FIXURL = {ftp://ftp.cse.msu.edu/pub/crg/PAPERS/m2-rm2004.pdf},
ABSTRACT = {}
}
@INPROCEEDINGS{TRAP.DOA.04,
AUTHOR = {S. M. Sadjadi and P. K. McKinley and B. H. C. Cheng and R. E. K. Stirewalt},
TITLE = {{TRAP/J}: Transparent Generation of Adaptable {Java} Programs},
BOOKTITLE = {Proceedings of the 2004 International Symposium on Distributed Objects and Applications},
PAGES = {},
YEAR = {2004},
OPTEDITOR = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTSERIES = {},
ADDRESS = {Agia Napa, Cyprus},
MONTH = {October},
OPTORGANIZATION = {},
OPTPUBLISHER = {},
OPTANNOTE = {},
FIXURL = {ftp://ftp.cse.msu.edu/pub/crg/PAPERS/trap-doa04.pdf},
ABSTRACT = {}
}
@INPROCEEDINGS{KMX.MPAC.04,
AUTHOR = {F. Samimi and P. K. McKinley and S. M. Sadjadi and P. Ge},
TITLE = {Kernel-Middleware Interaction to Support Adaptation in
Pervasive Computing Environments},
BOOKTITLE = {Proceedings of the Second
Int'l Workshop on Middleware for Pervasive and Ad-Hoc Computing, in conjunction with Middleware'04},
PAGES = {},
YEAR = {2004},
OPTEDITOR = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTSERIES = {},
ADDRESS = {Toronto, Ontario, Canada},
MONTH = {October},
OPTORGANIZATION = {},
OPTPUBLISHER = {},
OPTANNOTE = {},
FIXURL = {ftp://ftp.cse.msu.edu/pub/crg/PAPERS/kmx-mpac04.pdf},
ABSTRACT = {}
}
@INPROCEEDINGS{Zhou.IWQOS.2004,
AUTHOR = {Z. Zhou and P. K. McKinley and S. M. Sadjadi},
TITLE = {On Quality-of-Service and Energy Consumption Tradeoffs in
FEC-Enabled Audio Streaming},
BOOKTITLE = {Proceedings of the 12th IEEE International Workshop on Quality of Service (IWQoS 2004)},
YEAR = {2004},
ADDRESS = {Montreal, Canada},
MONTH = {June},
ABSTRACT = {
This paper addresses the energy consumption of forward error
correction (FEC) protocols as used to improve quality-of-service
(QoS) for wireless computing devices. The paper also characterizes the effect on energy
consumption and QoS of the power saving mode in 802.11
wireless local area networks (WLANs). Experiments are described in
which FEC-encoded audio streams are multicast to mobile
computers across a WLAN. Results of these experiments
quantify the tradeoffs between improved QoS, due to FEC, and
additional energy consumption caused by receiving and decoding
redundant packets. Two different approaches to FEC are
compared relative to these metrics. The results of this study enable the development of
adaptive software mechanisms that attempt to manage these
tradeoffs in the presence of highly dynamic wireless environments.
},
NOTE = {(selected as Best Student Paper)},
URL = {ftp://ftp.cse.msu.edu/pub/crg/PAPERS/iwqos-04.pdf}
}
@INPROCEEDINGS{Cheng-SafeAdaptation,
AUTHOR = {Ji Zhang and Zhenxiao Yang and Betty H.~C. Cheng and Philip K. McKinley},
TITLE = {Adding Safeness to Dynamic Adaptation Techniques},
BOOKTITLE = {Proceedings of the ICSE 2004 Workshop on Architecting Dependable Systems, in
conjunction with ICSE 2004},
YEAR = {2004},
ADDRESS = {Edinburgh, Scotland},
MONTH = {May},
URL = {ftp://ftp.cse.msu.edu/pub/crg/PAPERS/WADS-04.pdf}
}
@INPROCEEDINGS{ACT-ICAC,
AUTHOR = {S. M. Sadjadi and P. K. McKinley},
TITLE = {Transparent Self-Optimization in Existing {CORBA} Applications},
BOOKTITLE = {Proceedings of the International Conference on Autonomic Computing (ICAC-04)},
YEAR = {2004},
ADDRESS = {New York, NY},
MONTH = {May},
ABSTRACT = {
This paper addresses the design of adaptive middleware
to support autonomic computing in pervasive computing
environments.
The particular problem we address here is how to support
self-optimization to changing network connection capabilities
as a mobile user interacts with heterogeneous elements
in a wireless network infrastructure.
The goal is to enable self-optimization to such changes
transparently with respect to the core application code.
We propose a solution based on the use of the {\em generic
proxy}, which is a specific CORBA object that can intercept
and process any CORBA request using rules and actions that
can be introduced to the knowledge base of the proxy during
execution.
To explore its design and operation, we have incorporated
the generic proxy into ACT [1], an adaptive
middleware framework we designed previously to support
adaptation in CORBA applications.
Details of the generic proxy are presented, followed by
results of a case study enabling self-optimization for an
existing surveillance application in a heterogeneous
wireless environment.
},
URL = {ftp://ftp.cse.msu.edu/pub/crg/PAPERS/ACT-ICAC.pdf}
}
@INPROCEEDINGS{TRAP-ICAC,
AUTHOR = {S. M. Sadjadi and P. K. McKinley and R. E. K. Stirewalt and B. H.C. Cheng},
TITLE = {Generation of Self-Optimizing Wireless Network Applications (poster summary)},
BOOKTITLE = {Proceedings of the International Conference on Autonomic Computing (ICAC-04)},
YEAR = {2004},
ADDRESS = {New York, NY},
MONTH = {May},
ABSTRACT = {
This paper introduces {\em TRAP/J}, a software tool that
enables autonomic computing in existing Java programs by
generating {\em adapt-ready} versions of the original programs
at compile time.
The generation process is transparent to the original
program source code, in which there is no need to modify
the source code manually.
At run time, new behavior can be introduced to the adapt-ready
programs.
To reduce overhead, TRAP/J enables the developer to select,
at compile time, a subset of classes, constituting an
existing program, to be adaptive at run time.
To support dynamic adaptation in existing Java programs,
TRAP/J benefits from aspect-oriented programming and
behavioral reflection.
TRAP/J generate specific aspects and reflective classes associated
with the selected classes.
A case study is presented in which TRAP/J was used to
enable an existing audio-streaming application to perform
self-optimization in a wireless network environment by
adapting to changing conditions automatically.
},
URL = {ftp://ftp.cse.msu.edu/pub/crg/PAPERS/TRAP-ICAC.pdf}
}
@INPROCEEDINGS{ACT-ICDCS,
AUTHOR = {S. M. Sadjadi and P. K. McKinley},
TITLE = {{ACT}: An Adaptive {CORBA} Template to Support Unanticipated
Adaptation},
BOOKTITLE = {Proceedings of the 24th IEEE International Conference on Distributed Computing Systems (ICDCS)},
ABSTRACT = { This paper proposes an Adaptive CORBA Template (ACT), which
enables run-time improvements to CORBA applications in
response to unanticipated changes in either their functional
requirements or their execution environments. ACT enhances
CORBA applications by weaving adaptive code into the
applications' object request brokers (ORBs) at run time. The
woven code intercepts and adapt the requests, replies, and
exceptions that pass through the ORBs. ACT itself is
language- and ORB-independent. Specifically, ACT can be used
to develop an object-oriented framework in any language that
supports dynamic loading of code and can be applied to any
CORBA ORB that supports portable interceptors. Moreover, ACT
can be integrated with other adaptive CORBA frameworks and
can be used to support interoperation among otherwise
incompatible frameworks. To evaluate the performance and
functionality of ACT, we implemented a prototype in Java to
support unanticipated adaptation in non-functional concerns,
such as quality-of-service and system-resource management.
Our experimental results show that the overhead introduced
by the ACT infrastructure is negligible, while the
adaptations offered are highly flexible.},
MONTH = {March},
YEAR = {2004},
ADDRESS = {Tokyo, Japan},
URL = {ftp://ftp.cse.msu.edu/pub/crg/PAPERS/icdcs-04-act.pdf}
}
@INPROCEEDINGS{tang-icdcs04,
AUTHOR = {C. Tang and P. K. McKinley},
TITLE = {A Distributed Approach to Topology-Aware Overlay Path
Monitoring},
BOOKTITLE = {Proceedings of the 24th IEEE Int'l Conference on
Distributed Computing Systems (ICDCS)},
ADDRESS = {Tokyo, Japan},
MONTH = {March},
YEAR = {2004},
URL = {ftp://ftp.cse.msu.edu/pub/crg/PAPERS/icdcs-04-tang.pdf}
}
@INPROCEEDINGS{DARES-2004,
TITLE = {Perimorph: Run-Time Composition and State Management for Adaptive Systems},
AUTHOR = {E. P. Kasten and P. K. McKinley},
BOOKTITLE = {Proceedings of Fourth International Workshop on Distributed Auto-Adaptive and Reconfigurable Systems (DARES), in conjunction with ICDCS 2004},
ADDRESS = {Hachioji, Japan},
MONTH = {March},
YEAR = {2004},
PAGES = {332-337},
URL = {ftp://ftp.cse.msu.edu/pub/crg/PAPERS/dares04.pdf}
}
@INPROCEEDINGS{tang-icnp03,
AUTHOR = {C. Tang and P. K. McKinley},
TITLE = {On the Cost-Quality Tradeoff in Topology-Aware Overlay Path
Probing},
BOOKTITLE = {Proceedings of the 11th IEEE International Conference on Network
Protocols (ICNP)},
PAGES = {268-279},
ADDRESS = {Atlanta, Georgia},
MONTH = {November},
YEAR = {2003},
URL = {ftp://ftp.cse.msu.edu/pub/crg/PAPERS/icnp-03.pdf}
}
@INPROCEEDINGS{tang-mswim03,
AUTHOR = {C. Tang and P. K. McKinley},
TITLE = {Modeling Multicast Packet Losses in Wireless {LANs}},
BOOKTITLE = {Proceedings of the Sixth ACM International Workshop on Modeling,
Analysis and Simulation of Wireless and Mobile Systems (MSWiM) (in conjunction
with ACM Mobicom 2003)},
PAGES = {130-133},
ADDRESS = {San Diego, California},
MONTH = {September},
YEAR = {2003},
URL = {ftp://ftp.cse.msu.edu/pub/crg/PAPERS/mswim-03.pdf}
}
@INPROCEEDINGS{MetaSockets,
AUTHOR = {S. M. Sadjadi and P. K. McKinley and E. P. Kasten},
TITLE = {Architecture and Operation of an Adaptable Communication Substrate},
BOOKTITLE = {Proceedings of the Ninth IEEE International Workshop on Future Trends of Distributed Computing Systems (FTDCS'03)},
YEAR = {2003},
MONTH = {May},
PAGES = {46-55},
ADDRESS = {San Juan, Puerto Rico},
ABSTRACT = {This paper describes the internal architecture and operation of an adaptable communication component called the MetaSocket. MetaSockets are created using Adaptive Java, a reflective extension to Java that enables a component's internal architecture and behavior to be adapted at run time in response to external stimuli. This paper describes how adaptive behavior is implemented in MetaSockets, as well as how MetaSockets interact with other adaptive components, such as decision makers and event mediators. Results of experiments on a mobile computing testbed demonstrate how MetaSockets respond to dynamic wireless channel conditions in order to improve the quality of interactive audio streams delivered to iPAQ handheld computers. },
URL = {ftp://ftp.cse.msu.edu/pub/crg/PAPERS/ftdcs-03.pdf}
}
@INPROCEEDINGS{AOP-WOSS02,
AUTHOR = {Z.~Yang and B.~H.~C. Cheng and R.~E.~K.~Stirewalt and J.~Sowell and S.~M.~Sadjadi and P.~K.~McKinley},
TITLE = {An Aspect-Oriented Approach to Dynamic Adaptation},
BOOKTITLE = {Proceedings of the ACM SIGSOFT Workshop on Self-Healing Systems (WOSS02)},
OPTCROSSREF = {},
OPTKEY = {},
OPTPAGES = {},
YEAR = {2002},
OPTEDITOR = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTSERIES = {},
ADDRESS = {Charleston, South Carolina},
MONTH = {November},
OPTORGANIZATION = {IEEE Computer Society},
OPTPUBLISHER = {},
OPTANNOTE = {},
URL = {ftp://ftp.cse.msu.edu/pub/crg/PAPERS/woss02.pdf},
ABSTRACT = {This paper presents an aspect-oriented approach to dynamic adaptation. A systematic process for defining where, when, and how an adaptation is to be incorporated into an application is presented. Specifically, the paper presents a two-phase approach to dynamic adaptation, where the first phase prepares a non-adaptive program for adaptation, and the second phase implements the adaptation at run time. This approach is illustrated with a distributed conferencing application.
}
}
@INPROCEEDINGS{MSKK02.WEARABLE,
AUTHOR = {P. K. McKinley and S. Sadjadi and E. P. Kasten and R. Kalaskar},
TITLE = {Programming Language Support for Adaptable Wearable Computing},
BOOKTITLE = {Proceedings of the Sixth International Symposium on Wearable Computers},
ADDRESS = {Seattle, Washington},
MONTH = {October},
YEAR = {2002},
URL = {ftp://ftp.cse.msu.edu/pub/crg/PAPERS/iswc02.pdf},
ABSTRACT = {
This paper investigates the use of programming language constructs
to realize adaptive behavior in support of collaboration among users of
wearable and handheld computers.
A prototype language, Adaptive Java, contains primitives
that permit programs to modify their own operation
in a principled manner.
In a case study, Adaptive Java was used to construct
MetaSocket components, whose composition and behavior
can be adapted to changing conditions
during execution. MetaSockets were then integrated into Pavilion, a web-based
collaboration framework, and experiments were conducted
on a mobile computing testbed containing wearable, handheld, and laptop computer systems.
Performance results demonstrate the utility of MetaSockets to improving the
quality of interactive audio streams and reliable data transfers among
collaborating users.
}
}
@INPROCEEDINGS{McSK02.ICTS,
AUTHOR = {P. K. McKinley and S. M. Sadjadi and E. P. Kasten},
TITLE = {An Adaptive Software Approach to Intrusion Detection and Response},
BOOKTITLE = {Proceedings of the 10th International Conference on Telecommunication Systems, Modeling and Analysis},
PAGES = {},
YEAR = {2002},
OPTEDITOR = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTSERIES = {},
ADDRESS = {Monterey, California},
MONTH = {October},
OPTORGANIZATION = {IEEE Computer Society},
OPTPUBLISHER = {},
OPTANNOTE = {},
URL = {ftp://ftp.cse.msu.edu/pub/crg/PAPERS/icts10.ps.gz},
ABSTRACT = {
This paper proposes the use of programming
language constructs to support adaptive self-monitoring
and self-reporting software.
The methods are particularly well-suited to wireless mobile
devices, where limited resources may constrain
the use of certain software audits.
An adaptive software architecture is described
that supports run-time transformations on software components,
enabling them to report
internal details on how they are being used to other parts
of the system.
Effectively, any component of the system can be turned into
an "informer" at run time, and the nature of the
reported
information can be adapted dynamically based on changing
conditions or directives from another authority, such
as an intrusion detection system.
A prototype implementation is described.
The operation of the system is demonstrated through an experiment in
which it detects and responds to a malicious host that
multicasts "noise" packets to a wireless iPAQ handheld computer.
}
}
@INPROCEEDINGS{SaMK02.DOA,
AUTHOR = {S. M. Sadjadi and P. K. McKinley and E. P. Kasten},
TITLE = {MetaSockets: Run-Time Support for Adaptive Communication Services (Poster Summary)},
BOOKTITLE = {Addendum to the Proceedings of the 2002 International Symposium on Distributed Objects and Applications},
PAGES = {},
YEAR = {2002},
OPTEDITOR = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTSERIES = {},
ADDRESS = {Irvine, California},
MONTH = {October},
OPTORGANIZATION = {},
OPTPUBLISHER = {},
OPTANNOTE = {},
URL = {ftp://ftp.cse.msu.edu/pub/crg/PAPERS/doa02.pdf},
ABSTRACT = {
This paper describes the use of the Adaptive Java programming
language to develop an
adaptable communication component called the MetaSocket.
MetaSockets are created from existing Java socket classes, but
their structure and behavior can be adapted at run time in
response to external stimuli.
Results of experiments
on a mobile computing testbed demonstrate how
MetaSockets respond to dynamic wireless channel conditions
in order to improve the quality
of interactive audio streams delivered to iPAQ handheld computers.
}
}
@INPROCEEDINGS{TaMc02.protocol,
AUTHOR = {Chiping Tang and P. K. McKinley},
TITLE = {Adaptive Reliable Multicast in Wireless {LANs}},
BOOKTITLE = {Proceedings of the IEEE International Conference on Networking},
ADDRESS = {Atlanta, Georgia},
MONTH = {August},
YEAR = {2002},
URL = {ftp://ftp.cse.msu.edu/pub/crg/PAPERS/icn-2002-tang.pdf},
ABSTRACT = {
Wireless local area networks pose new challenges to error
recovery and flow control in reliable multicast
protocols. Limited wireless bandwidth, as well as queuing losses
caused by the asymmetric wired/wireless interactions, demands
more effective approaches for reducing packet losses. Moreover,
a protocol must dynamically adjust its behavior to changing
environmental conditions. In this paper, we propose and evaluate
such a protocol, called the Adaptive FEC-based Reliable Multicast
(AFRM) protocol. The protocol uses both proactive FEC and
reactive FEC, adapting relevant parameters to current conditions.
Both local and global NACK suppression are applied, but in a
manner that accommodates delays due to access point queuing.
Finally, the AFRM flow control strategy uses a novel method to
differentiate propagation-related packet losses from queueing
losses. Experimental and simulation results show the protocol
has good performance in terms of throughput in most cases. Those
factors that negatively affect performance are highlighted as
topics of future research.
}
}
@INPROCEEDINGS{GeMc02.LDM,
AUTHOR = {Peng Ge and Philip K. McKinley},
TITLE = {Leader-Driven Multicast for Video Streaming on Wireless {LANs}},
BOOKTITLE = {Proceedings of the IEEE International Conference on Networking},
ADDRESS = {Atlanta, Georgia},
MONTH = {August},
YEAR = {2002},
URL = {ftp://ftp.cse.msu.edu/pub/crg/PAPERS/icn-2002-ge.pdf},
ABSTRACT = {
The IEEE 802.11 MAC layer uses RTS/CTS/ACK signaling to improve
the reliability of unicast transmissions, but in current products
there is no special signaling support for multicast
transmissions. Therefore, the packet loss rate of multicast
communication is generally higher than that of unicast
communication. This paper evaluates a new MAC-layer multicasting
technique called Leader-Driven Multicast (LDM). Instead of
multicasting to a group address, the source node sends a unicast
stream to the address of a leader node among the receivers. All
other receivers passively receive this unicast stream, including
retransmissions. This paper investigates the effects of the LDM
protocol on interactive video multicasting across WLANs. Results
are presented from a simulation study using different packet loss
models and different loss correlations among receivers. The
results indicate that LDM is potentially beneficial even when
there is no loss correlation among receivers. When losses do
exhibit some positive correlation LDM can provide a very high
quality multicast stream to WLAN nodes, especially when combined
with application-level error control techniques.
}
}
@INPROCEEDINGS{ZLM05.Piped.LCPC,
AUTHOR = {J. Zhang and J. Lee and P. K. McKinley},
TITLE = {Optimizing Java Piped I/O Stream Library for Performance},
BOOKTITLE = {Proceedings of the 15th Workshop on Languages and Compilers for Parallel Computing (LCPC)},
YEAR = {2002},
ADDRESS = {College Park, Maryland},
MONTH = {July}
}
@INPROCEEDINGS{KMSS02.AOPDCS,
AUTHOR = {E. Kasten and P. K. McKinley and S. Sadjadi and R. Stirewalt},
TITLE = {Separating Introspection and Intercession in Metamorphic Distributed Systems},
BOOKTITLE = {Proceedings of the IEEE
Workshop on Aspect-Oriented Programming for Distributed Computing, in conjunction with
ICDCS 2002},
ADDRESS = {Vienna, Austia},
MONTH = {July},
YEAR = {2002},
URL = {ftp://ftp.cse.msu.edu/pub/crg/PAPERS/aopdcs-02.ps.gz},
ABSTRACT = {
Many middleware platforms use computational reflection to support
adaptive functionality. Most approaches intertwine the activity
of observing behavior (introspection) with the activity of
changing behavior (intercession). This paper explores the use of
language constructs to separate these parts of reflective
functionality. This separation and "packaging" of reflective
primitives is intended to facilitate the design of correct and
consistent adaptive middleware. A prototype language, called
Adaptive Java, is described in which this functionality is
realized through extensions to the Java programming language. A
case study is described in which "metamorphic" socket components
are created from regular socket classes and used to realize
adaptive behavior on wireless network connections.
}
}
@INPROCEEDINGS{SHAMAN-02,
AUTHOR = {Philip K. McKinley and E. P. Kasten and S. M. Sadjadi and Zhinan Zhou},
TITLE = {Realizing Multi-Dimensional Software Adaptation},
BOOKTITLE = {Proceedings of the ACM
Workshop on Self-Healing, Adaptive and self-MANaged
Systems, held in conjunction with the
16th Annual ACM International Conference on Supercomputing},
ADDRESS = {New York City},
MONTH = {June},
YEAR = {2002},
URL = {ftp://ftp.cse.msu.edu/pub/crg/PAPERS/shaman02.pdf},
ABSTRACT = {
This paper describes the use of programming
language constructs to support run-time software adaptation.
A prototype language, Adaptive Java, contains primitives
that permit programs to modify their own operation
in a principled manner.
In case studies, Adaptive Java is being used to
support adaptation for different cross-cutting concerns
associated with heterogeneous
mobile computing and critical infrastructure
protection.
Examples are described in which Adaptive Java components
support dynamic quality-of-service on wireless networks,
run-time energy management for handheld computers,
and self-auditing of potential security threats in
distributed environments.
}
}
@INPROCEEDINGS{GeMc02.IPCCC,
AUTHOR = {P. Ge and P. K. McKinley},
TITLE = {Comparisons of Error Control Techniques for Wireless Video
Multicasting},
BOOKTITLE = {Proceedings of the IEEE International Performance,
Computing, and Communications Conference},
ADDRESS = {Phoenix, Arizona},
MONTH = {April},
YEAR = {2002},
URL = {ftp://ftp.cse.msu.edu/pub/crg/PAPERS/ipccc-02.ps.gz},
ABSTRACT = {
This paper explores three different methods, employed separately
and in combination, to improve the quality of video delivery on
wireless local area networks. The approaches are: leader-driven
multicast (LDM), the monitoring of MAC layer unicast
(re)transmissions by other receivers; application-level forward
error correction (FEC) using block erasure codes; and negative
feedback from selected receivers in the form of extra parity
requests (EPR). The performance of these three methods is
evaluated using both experimentation on a mobile computing
testbed and simulation. The results indicate that, while LDM is
helpful in improving the raw packet reception rate, the
combination of FEC and EPR is most effective in improving the
frame delivery rate.
}
}
@ARTICLE{cdsmsl01,
AUTHOR = {B. Cheng and L. Dillon and K. Stirewalt and
P. McKinley and S. Kulkarni and J. Lee},
TITLE = {Automated Development and Run-Time Adaptation of
Interactive Distributed Applications},
JOURNAL = {NCO Workshop on New Visions for Software Design and Productivity: Research and Applications},
YEAR = {2001},
OPTKEY = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTPAGES = {},
MONTH = {December},
ADDRESS = {Nashville, Tennessee},
OPTNOTE = {},
OPTANNOTE = {},
ABSTRACT = {}
}
@INPROCEEDINGS{McPA01.MIDDLEWARE,
AUTHOR = {P. K. McKinley and U. I. Padmanabhan and N. Ancha},
TITLE = {Experiments in Composing Proxy Audio Services for Mobile Users},
BOOKTITLE = {Proceedings of the IFIP/ACM International Conference on
Distributed Systems Platforms (Middleware 2001)},
ADDRESS = {Heidelberg, Germany},
MONTH = {November},
YEAR = {2001},
PAGES = {99--120},
URL = {ftp://ftp.cse.msu.edu/pub/crg/PAPERS/middleware-2001.ps.gz},
ABSTRACT = {
This paper describes an experimental study in the use of a
composable proxy framework to improve the quality of interactive
audio streams delivered to mobile hosts. Two forward error
correction (FEC) proxylets are developed, one using block erasure
codes, and the other using the GSM 06.10 encoding algorithm.
Separately, each type of FEC improves the ability of the audio
stream to tolerate errors in a wireless LAN environment. When
composed in a single proxy, however, they cooperate to correct
additional types of burst errors. Results are presented from a
performance study conducted on a mobile computing testbed.
}
}
@INPROCEEDINGS{GeMc01.MNS,
AUTHOR = {Peng Ge and Philip K. McKinley},
TITLE = {Experimental Evaluation of Error Control for Video Multicast over Wireless {LANs}},
BOOKTITLE = {Proceedings of the Third
International Workshop on Multimedia Network Systems},
ADDRESS = {Phoenix, Arizona},
MONTH = {April},
YEAR = {2001}
}
@INPROCEEDINGS{McPa01.WNMC,
AUTHOR = {Philip K. McKinley and U. I. Padmanabhan},
TITLE = {Design of Composable Proxy Filters for Mobile Computing},
BOOKTITLE = {Proceedings of the Second
International Workshop on Wireless Networks and Mobile Computing},
ADDRESS = {Phoenix, Arizona},
MONTH = {April},
YEAR = {2001}
}
@INPROCEEDINGS{stir01:ssr,
AUTHOR = {R. E. K. Stirewalt and L. K. Dillon},
TITLE = {Generation of Visitor
Components that Implement Program Transformations},
BOOKTITLE = {Proc.~ACM Symp.~Software Reuse},
PAGES = {86--94},
YEAR = {2001},
ADDRESS = {Toronto},
MONTH = MAY
}
@INPROCEEDINGS{stir01:icse01a,
AUTHOR = { R. E. K. Stirewalt and L. K. Dillon },
TITLE = { A component-based approach to building formal
analysis tools },
BOOKTITLE = { Proc.~2001 IEEE Inter.\ Conf.\ Software Engineering},
YEAR = 2001,
PAGES = { 167--166 },
ADDRESS = {Toronto},
MONTH = MAY
}
@UNPUBLISHED{stir00:applicative-visitor-framework,
AUTHOR = {R. E. Kurt Stirewalt and Laura K. Dillon},
TITLE = {Lightweight Analysis Components: An Improvement Over Monolithic
Tools and Environments},
YEAR = 2000,
MONTH = MAR,
NOTE = {Submitted}
}
@UNPUBLISHED{stir00:semantic-rule-processor-framework,
AUTHOR = {R. E. Kurt Stirewalt and Laura K. Dillon},
TITLE = {Amalia: A Generator Framework for Lightweight Analysis Components},
YEAR = 2000,
MONTH = MAR,
NOTE = {Submitted}
}
@UNPUBLISHED{stirewalt:scp-subm04,
AUTHOR = {R. E. K. Stirewalt and R. Behrends and L. K. Dillon},
TITLE = {A Model-Based Semantics for Synchronization Contracts
in Object-Oriented Languages},
NOTE = {accepted (pending minor revision)
to {\it Science of Computer Programming\/}},
OPTKEY = {},
OPTMONTH = {},
OPTYEAR = {},
OPTANNOTE = {}
}
@INPROCEEDINGS{stockman:asee04,
AUTHOR = {G. Stockman and P. Albee and L. Dillon and J. Oleszkiewicz},
TITLE = {CS1 and CS2 Programming Exams for Assessing Learning
and Teaching},
BOOKTITLE = {Proc. of the ASEE Annual Conference and Exposition},
OPTCROSSREF = {},
OPTKEY = {},
OPTPAGES = {},
YEAR = {2004},
OPTEDITOR = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTSERIES = {},
OPTADDRESS = {Salt Lake City},
MONTH = JUN,
OPTORGANIZATION = {},
OPTPUBLISHER = {},
OPTANNOTE = {}
}
@INPROCEEDINGS{stockman:aseencs04,
AUTHOR = {G. Stockman and P. Albee and L. Dillon and J. Oleszkiewicz},
TITLE = {CS1 and CS2 Programming Exams for Assessing Learning
and Teaching},
BOOKTITLE = {Proc. ASEE North Central Section Spring Conference},
OPTCROSSREF = {},
OPTKEY = {},
OPTPAGES = {},
YEAR = {2004},
OPTEDITOR = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTSERIES = {},
OPTADDRESS = {Kalamazoo, MI},
MONTH = APR,
OPTORGANIZATION = {},
OPTPUBLISHER = {},
OPTANNOTE = {}
}
@PROCEEDINGS{berkeley-workshop-temporal-and-realtime-specs,
BOOKTITLE = {Proc. Berkeley Workshop on Temporal and Real-Time
Specification},
TITLE = {Proc. Berkeley Workshop on Temporal and Real-Time
Specification},
YEAR = 1990,
EDITOR = {Peter B. Ladkin and Fritz H. Vogt},
ADDRESS = {International Computer Science Institute, Berkeley, CA},
MONTH = AUG
}
@PROCEEDINGS{fse94,
TITLE = {Proc.\ 2nd ACM SIGSOFT Symp.\ Foundations of Software Engineering},
BOOKTITLE = {Proc.\ 2nd ACM SIGSOFT Symp.\ Foundations of Software Engineering},
YEAR = 1994,
PUBLISHER = {ACM Press},
ADDRESS = {New Orleans},
MONTH = DEC
}
@PROCEEDINGS{svl93,
TITLE = {Proc.\ 1993 IEEE Symp.\ Visual Languages},
BOOKTITLE = {Proc.\ 1993 IEEE Symp.\ Visual Languages},
YEAR = 1993,
PUBLISHER = {IEEE Computer Society Press},
ADDRESS = {Bergen, Norway},
MONTH = AUG,
NOTE = {},
KEYWORDS = {}
}
@PROCEEDINGS{tav4,
TITLE = {Proc. 4th ACM Symp. Testing, Analysis and Verification},
BOOKTITLE = {Proc. 4th ACM Symp. Testing, Analysis and Verification},
ADDRESS = {Victoria, British Columbia},
MONTH = OCT,
YEAR = 1991,
PUBLISHER = {ACM Press},
ORGANIZATION = {ACM SIGSOFT}
}
@ARTICLE{shapiro05precision,
AUTHOR = {Jonathan K. Shapiro C. V. Hollot and Don Towsley},
TITLE = {Trading Precision for Stability in Congestion Control with Probabilistic Packet Marking},
JOURNAL = {ICNP 2005},
MONTH = {November},
YEAR = {2005},
NOTE = {To appear},
OPTKEY = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTPAGES = {},
OPTMONTH = {},
OPTNOTE = {},
OPTANNOTE = {}
}
@ARTICLE{figueiredo05incentives,
AUTHOR = {Daniel Figueiredo and Jonathan K. Shapiro and Don Towsley},
TITLE = {Incentives to Promote Availability in Peer-to-Peer Anonymity Systems},
JOURNAL = {ICNP 2005},
MONTH = {November},
YEAR = {2005},
NOTE = {To appear},
OPTKEY = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTPAGES = {},
OPTMONTH = {},
OPTNOTE = {},
OPTANNOTE = {}
}
@ARTICLE{adbk04,
AUTHOR = {A. Arora and P. Dutta and S. Bapat and V. Kulathumani and H. Zhang and V. Naik and V. Mittal and H. Cao and M. Demirbas and M. Gouda and Y-R. Choi and T. Herman and S. S. Kulkarni and U. Arumugam and M. Nesterenko and A. Vora and M. Miyashita},
TITLE = {A line in the sand: A wireless sensor network for target detection, classification, and tracking},
JOURNAL = {Computer Networks (Elsevier), Special Issue on Military Communications Systems and Technologies},
YEAR = {2004},
OPTKEY = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTPAGES = {},
OPTMONTH = {},
OPTNOTE = {},
OPTANNOTE = {}
}
@ARTICLE{barrier,
AUTHOR = {S. S. Kulkarni and A. Arora},
TITLE = {Multitolerant Barrier Synchronization},
JOURNAL = {Information Processing Letters},
YEAR = {1997},
OPTKEY = {},
VOLUME = {64},
NUMBER = {1},
MONTH = {October},
PAGES = {29--36},
OPTNOTE = {},
OPTANNOTE = {}
}
@INPROCEEDINGS{bk05deas,
AUTHOR = {K. Biyani and S. S. Kulkarni},
TITLE = {Building Component Families to Support Adaptation},
BOOKTITLE = {International Workshop on Design and Evolution of
Autonomic Application Softwar
e, ICSE},
OPTCROSSREF = {},
OPTKEY = {},
OPTPAGES = {},
YEAR = {2005},
OPTEDITOR = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTSERIES = {},
OPTADDRESS = {},
MONTH = {May},
OPTORGANIZATION = {},
OPTPUBLISHER = {},
OPTNOTE = {},
OPTANNOTE = {}
}
@ARTICLE{ck05adhoc,
AUTHOR = {G. Chakrabarti and S. S. Kulkarni},
TITLE = {Load Balancing and Resource Reservation in Mobile Ad-Hoc Networks},
JOURNAL = {Ad Hoc Networks},
YEAR = {2005},
NOTE = {To appear},
OPTKEY = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTPAGES = {},
OPTMONTH = {},
OPTNOTE = {},
OPTANNOTE = {}
}
@ARTICLE{dcs98,
AUTHOR = {A.~Arora and S.~S.~Kulkarni},
TITLE = {Detectors and Correctors: {A} Theory of Fault-Tolerance Components},
JOURNAL = {International Conference on Distributed Computing Systems},
YEAR = {1998},
OPTKEY = {},
OPTVOLUME = {},
OPTNUMBER = {},
MONTH = {May},
PAGES = {436--443},
OPTANNOTE = {}
}
@ARTICLE{dk,
AUTHOR = {D. M. Dhamdhere and S. S. Kulkarni},
TITLE = {A token based $k$ resilient mutual exclusion algorithm for distributed systems},
OPTCROSSREF = {},
OPTKEY = {},
JOURNAL = {Information Processing Letters},
YEAR = {1994},
VOLUME = {50},
OPTNUMBER = {},
PAGES = {151-157},
OPTMONTH = {},
OPTNOTE = {},
OPTANNOTE = {}
}
@ARTICLE{ek04dsn,
AUTHOR = {A. Ebnenasir and S. S. Kulkarni},
TITLE = {{SAT}-Based Synthesis of Fault-Tolerance},
JOURNAL = {In the Fast Abstracts of the International Conference on Dependable Systems and Networks, Palazzo dei Congressi, Florence, Italy},
YEAR = {2004},
OPTKEY = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTPAGES = {},
OPTMONTH = {},
OPTNOTE = {},
OPTANNOTE = {}
}
@ARTICLE{ek04savcbs,
AUTHOR = {A. Ebnenasir and S. S. Kulkarni},
TITLE = {Hierarchical Presynthesized Component for Automatic Addition of Fault-Tolerance: A Case Study},
JOURNAL = {Proceedings of ACM Workshop on Specification and Verification of Component-Based Systems (SAVCBS), Newport Beach, California, USA},
YEAR = {2004},
OPTKEY = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTPAGES = {},
OPTMONTH = {},
OPTNOTE = {},
OPTANNOTE = {}
}
@ARTICLE{ek05edcc,
AUTHOR = {A. Ebnenasir and S. S. Kulkarni},
TITLE = {Adding Fault-Tolerance Using Pre-Synthesized Components},
JOURNAL = {Fifth European Dependable Computing Conference},
YEAR = {2005},
NOTE = {To appear},
OPTKEY = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTPAGES = {},
OPTMONTH = {},
OPTNOTE = {},
OPTANNOTE = {}
}
@ARTICLE{ftrtft2000,
AUTHOR = {S.~S.~Kulkarni and A.~Arora},
TITLE = {Automating the Addition of Fault-Tolerance},
JOURNAL = {Formal Techniques in Real-Time and Fault-Tolerant Systems},
YEAR = {2000},
OPTKEY = {},
OPTVOLUME = {},
OPTNUMBER = {},
PAGES = {82--93},
OPTMONTH = {},
OPTNOTE = {},
OPTANNOTE = {}
}
@MISC{ftsyn,
AUTHOR = {A.~Ebnenasir and S. S. ~Kulkarni},
TITLE = {{FTSyn}: A Framework For Automatic Synthesis of Fault-Tolerance},
OPTCROSSREF = {},
OPTKEY = {},
HOWPUBLISHED = {\url{http://www.cse.msu.edu/~ebnenasi/research/tools/ftsyn.htm} },
YEAR = {},
VOLUME = {},
NUMBER = {},
PAGES = {},
OPTMONTH = {},
OPTNOTE = {},
OPTANNOTE = {}
}
@ARTICLE{graybox,
AUTHOR = {A. Arora and M. Demirbas and S. Kulkarni. },
TITLE = {Graybox stabilization},
JOURNAL = {International Conference on Dependable Systems and Networks (DSN'2001)},
YEAR = {2001},
OPTKEY = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTPAGES = {},
MONTH = {July},
OPTNOTE = {},
OPTANNOTE = {}
}
@ARTICLE{icpp98,
AUTHOR = {S.~S.~Kulkarni and A.~Arora},
TITLE = {Low-cost
Fault-tolerance in Barrier Synchronizations},
JOURNAL = {International Conference on Parallel Processing},
YEAR = {1998},
OPTKEY = {},
OPTVOLUME = {},
OPTNUMBER = {},
MONTH = {August},
PAGES = {132--139},
OPTNOTE = {},
OPTANNOTE = {}
}
@ARTICLE{ka03opodis,
AUTHOR = {S. S. Kulkarni and M (U) Arumugam},
TITLE = {Transformations for Write-All-With-Collision Model},
JOURNAL = {On Principles of Distributed Systems},
YEAR = {2003},
OPTKEY = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTPAGES = {},
OPTMONTH = {},
OPTNOTE = {},
OPTANNOTE = {}
}
@ARTICLE{ka03sss,
AUTHOR = {S. S. Kulkarni and M (U) Arumugam},
TITLE = {Collision free communication in sensor networks},
JOURNAL = {Symposium on Self-stabilization, San Francisco, CA, Lecture Notes in Computer Science vol 2704},
YEAR = {2003},
OPTKEY = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTPAGES = {},
OPTMONTH = {},
OPTNOTE = {},
OPTANNOTE = {}
}
@ARTICLE{ka04adsn,
AUTHOR = {S. S. Kulkarni and M (U) Arumugam},
TITLE = {TDMA Service for Sensor Networks},
JOURNAL = {Assurance in Distributed Systems and Networks (ADSN)},
YEAR = {2004},
OPTKEY = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTPAGES = {},
OPTMONTH = {},
OPTNOTE = {},
OPTANNOTE = {}
}
@ARTICLE{ka05COMNET_Transformations,
AUTHOR = {S. S. Kulkarni and M. Arumugam},
TITLE = {Transformations for Write-All-With-Collision Model},
JOURNAL = {Computer Communications (Elsevier), Special Issue on Dependable Wireless Sensor Networks},
YEAR = {2005},
OPTKEY = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTPAGES = {},
OPTMONTH = {},
NOTE = {to appear},
OPTANNOTE = {}
}
@ARTICLE{ka05causalobserver,
AUTHOR = {S. S. Kulkarni and M. Arumugam},
TITLE = {Approximate Causal Observer},
JOURNAL = {Transactions of Society of Instrument and Control Engineers, Special Issue on Networked Sensing Systems},
YEAR = {2005},
OPTKEY = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTPAGES = {},
OPTMONTH = {},
NOTE = {to appear},
OPTANNOTE = {}
}
@INBOOK{ka05sno,
AUTHOR = {S. S. Kulkarni and M(U). Arumugam},
TITLE = {SS-TDMA: A self-stabilizing MAC for sensor networks},
CHAPTER = {Sensor Network Operations},
PUBLISHER = {IEEE Press},
YEAR = {2005},
NOTE = {To appear},
OPTKEY = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTSERIES = {},
OPTTYPE = {},
OPTADDRESS = {},
OPTEDITION = {},
OPTMONTH = {},
OPTPAGES = {},
OPTNOTE = {},
OPTANNOTE = {}
}
@ARTICLE{ka97fsttcs,
AUTHOR = {S.~S.~Kulkarni and A.~Arora},
TITLE = {Compositional Design of Multitolerant Repetitive Byzantine Agreement},
JOURNAL = {Proceedings of the Seventeenth International Conference on Foundations of Software Technology and Theoretical Computer Science, Kharagpur, India},
YEAR = {1997},
OPTKEY = {},
OPTVOLUME = {},
OPTNUMBER = {},
MONTH = {December},
PAGES = {169-183},
NOTE = {},
OPTANNOTE = {}
}
@ARTICLE{ka97wss,
AUTHOR = {S. S.~Kulkarni and A. Arora},
TITLE = {Compositional Design of Multitolerant Repetitive {B}yzantine Agreement (preliminary version)},
JOURNAL = {Third Workshop on Self-Stabilizing Systems (WSS 97), University of California, Santa Barbara},
YEAR = {1997},
OPTKEY = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTMONTH = {},
OPTPAGES = {},
OPTNOTE = {},
OPTANNOTE = {}
}
@ARTICLE{kb03icice,
AUTHOR = {S. S. Kulkarni and B. Bruhadeshwar},
TITLE = {Adaptive Rekeying for Secure Multicast},
JOURNAL = {IEEE/IEICE Special issue on Communications: Transactions on
Communications},
YEAR = {2003},
OPTKEY = {},
VOLUME = {E86-B},
NUMBER = {10},
PAGES = {2948-2956},
MONTH = {October},
OPTNOTE = {},
OPTANNOTE = {}
}
@INPROCEEDINGS{kb03podsy,
AUTHOR = {S. S. Kulkarni and K. Biyani and M. Arumugam},
TITLE = {Composing Distributed Fault-tolerance Components},
BOOKTITLE = {Workshop on Principles of Dependable Systems, DSN},
OPTCROSSREF = {},
OPTKEY = {},
PAGES = {W127-136},
YEAR = {2003},
OPTEDITOR = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTSERIES = {},
OPTADDRESS = {},
MONTH = {June},
OPTORGANIZATION = {},
OPTPUBLISHER = {},
OPTNOTE = {},
OPTANNOTE = {}
}
@INPROCEEDINGS{kb04cbse,
AUTHOR = {S. S. Kulkarni and K. Biyani},
TITLE = {Correctness of Component-based Adaptation},
BOOKTITLE = {International Symposium on Component-based Software
Engineering, ICSE},
OPTCROSSREF = {},
OPTKEY = {},
PAGES = {48-58},
YEAR = {2004},
OPTEDITOR = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTSERIES = {},
OPTADDRESS = {},
MONTH = {May},
OPTORGANIZATION = {},
OPTPUBLISHER = {},
OPTNOTE = {},
OPTANNOTE = {}
}
@INPROCEEDINGS{kb04icdcit,
AUTHOR = {S. S. Kulkarni and
B. Bruhadeshwar},
TITLE = {Distributing Key Updates in Secure Dynamic Groups.},
BOOKTITLE = {Distributed Computing and Internet Technology, First International Conference, ICDCIT 2004, Bhubaneswar, India, December
22-24, 2004},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {3347},
YEAR = {2004},
PAGES = {410-419},
ISBN = {3-540-24075-6},
BIBSOURCE = {DBLP, http://dblp.uni-trier.de}
}
@ARTICLE{kb05icnp,
AUTHOR = {S. S. Kulkarni and B. Bruhadeshwar},
TITLE = {A Family of Collusion Resistant Protocols for Instantiating Security},
JOURNAL = {International Conference on Network Protocols},
YEAR = {2005},
OPTKEY = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTPAGES = {},
OPTMONTH = {},
NOTE = {to appear},
OPTANNOTE = {}
}
@INPROCEEDINGS{kb05ndss,
AUTHOR = {S. S. Kulkarni and
B. Bruhadeshwar},
TITLE = {Rekeying and Storage Cost for Multiple User Revocation.},
BOOKTITLE = { The 12th Annual Network and Distributed System Security Symposium, San Diego, California },
PUBLISHER = {Internet Society},
YEAR = {2005},
PAGES = {45-54}
}
@ARTICLE{kbe04lopstr,
AUTHOR = {S. S. Kulkarni and B. Bonakdarpour, A. Ebnenasir},
TITLE = {Mechanical Verification of Automatic Synthesis of Fault-Tolerant Programs},
JOURNAL = {International Symposium on Logic Based Program Synthesis and Transformation, (LOPSTR)},
YEAR = {2004},
OPTKEY = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTPAGES = {},
OPTMONTH = {},
OPTNOTE = {},
OPTANNOTE = {}
}
@ARTICLE{kbor05ipl,
AUTHOR = {S. S. Kulkarni and C. Bolen J. Oleszkiewicz and A. Robinson},
TITLE = {Alternators in Read/Write Atomicity},
JOURNAL = {Information Processing Letters},
YEAR = {2005},
NOTE = {to appear},
OPTKEY = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTPAGES = {},
OPTMONTH = {},
OPTNOTE = {},
OPTANNOTE = {}
}
@ARTICLE{ke02,
AUTHOR = {S. S. ~Kulkarni and A. ~Ebnenasir},
TITLE = {The Complexity of Adding Failsafe Fault-Tolerance},
JOURNAL = {International Conference on Distributed Computing Systems },
YEAR = {2002},
OPTKEY = {},
VOLUME = {},
NUMBER = {},
PAGES = {337-334},
OPTMONTH = {},
OPTNOTE = {},
OPTANNOTE = {}
}
@ARTICLE{ke03,
AUTHOR = {S. S. ~Kulkarni and A. ~Ebnenasir},
TITLE = {Enhancing The Fault-Tolerance of Nonmasking Programs},
JOURNAL = {International Conference on Distributed Computing Systems },
YEAR = {2003},
OPTKEY = {},
VOLUME = {},
NUMBER = {},
PAGES = {441-450},
OPTMONTH = {},
OPTNOTE = {},
OPTANNOTE = {}
}
@TECHREPORT{ke03framework,
AUTHOR = {S. S. Kulkarni and A. Ebnenasir},
TITLE = {A Framework for Automatic Synthesis of Fault-Tolerance},
INSTITUTION = {Michigan State University},
YEAR = {2003},
OPTKEY = {},
OPTTYPE = {},
NUMBER = {MSU-CSE-03-16},
OPTADDRESS = {},
OPTMONTH = {},
OPTNOTE = {},
OPTANNOTE = {}
}
@ARTICLE{ke04dsn,
AUTHOR = {S. S. Kulkarni and A. Ebnenasir},
TITLE = {Automated Synthesis of Multitolerance},
JOURNAL = {The International Conference on Dependable Systems and Networks},
YEAR = {2004},
OPTKEY = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTPAGES = {},
OPTMONTH = {},
OPTNOTE = {},
OPTANNOTE = {}
}
@ARTICLE{kga05COMNET_Security,
AUTHOR = {S. S. Kulkarni and M. G. Gouda and A. Arora},
TITLE = {Secret Instantiation in Ad-Hoc Network},
JOURNAL = {Computer Communications (Elsevier), Special Issue on Dependable Wireless Sensor Networks},
YEAR = {2005},
OPTKEY = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTPAGES = {},
OPTMONTH = {},
NOTE = {to appear},
OPTANNOTE = {}
}
@ARTICLE{kr05jhsn,
AUTHOR = {S. S. Kulkarni and Ravikant},
TITLE = {Stabilizing Causal Deterministic Merge},
JOURNAL = {Journal of High Speed Networks},
YEAR = {2005},
NOTE = {To appear},
OPTKEY = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTPAGES = {},
OPTMONTH = {},
OPTNOTE = {},
OPTANNOTE = {}
}
@ARTICLE{krs99,
AUTHOR = {S.~S.~Kulkarni and J.~Rushby and N.~Shankar},
TITLE = {A Case-Study in Component-Based Mechanical Verification of Fault-Tolerant Programs},
JOURNAL = {Proceedings of the 19th IEEE International Conference on Distributed Computing Systems Workshop on Self-Stabilization (WSS'99) Austin, Texas, USA},
YEAR = {1999},
OPTKEY = {},
OPTVOLUME = {},
OPTNUMBER = {},
MONTH = {June},
PAGES = {33--40},
OPTNOTE = {},
OPTANNOTE = {}
}
@ARTICLE{kw05icdcs,
AUTHOR = {S. S. Kulkarni and L. Wang},
TITLE = {{MNP}: Multihop network reprogramming service for sensor networks},
JOURNAL = {In Proceedings of the 25th International Conference on
Distributed Computing Systems (ICDCS)},
PAGES = {7-16},
MONTH = {June},
YEAR = {2005}
}
@ARTICLE{multitolerance,
AUTHOR = {A. Arora and S.~S. Kulkarni},
TITLE = {Component Based Design of Multitolerant Systems},
JOURNAL = {IEEE Transactions on Software Engineering},
YEAR = {1998},
OPTKEY = {},
VOLUME = {24},
NUMBER = {1},
MONTH = {January},
PAGES = {63--78},
OPTNOTE = {},
OPTANNOTE = {}
}
@ARTICLE{ofmp,
AUTHOR = {S. S. Kulkarni and A. Arora},
TITLE = {Once-and-Forall Management Protocol ({O}{F}{M}{P})},
JOURNAL = {Proceedings of the Fifth International Conference on Network Protocols},
YEAR = {1997},
OPTKEY = {},
OPTVOLUME = {},
OPTNUMBER = {},
MONTH = {October},
OPTPAGES = {},
OPTNOTE = {},
OPTANNOTE = {}
}
@ARTICLE{reset,
AUTHOR = {S. Kulkarni and A. Arora},
TITLE = {Multitolerance in Distributed Reset},
JOURNAL = {Chicago Journal of Theoretical Computer Science},
VOLUME = {1998},
NUMBER = {4},
PUBLISHER = {MIT Press},
MONTH = {December},
YEAR = {1998}
}
@ARTICLE{rvc_jpdc,
AUTHOR = {A. Arora and S. S. Kulkarni and M. Demirbas},
TITLE = {Resettable Vector Clocks},
JOURNAL = {Journal of Parallel and Distributed Computing},
YEAR = {2005},
OPTKEY = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTPAGES = {},
OPTMONTH = {},
OPTNOTE = {A preliminary version of this paper appears in Principles of Distributed Computing (PODC) 2000},
OPTANNOTE = {}
}
@ARTICLE{srds01,
AUTHOR = { S. S.~Kulkarni and A.~Arora and A.~Chippada.},
TITLE = { Polynomial time synthesis of Byzantine agreement.},
JOURNAL = { Symposium on Reliable Distributed Systems },
YEAR = {2001},
OPTKEY = {},
VOLUME = {},
NUMBER = {},
PAGES = {},
OPTMONTH = {},
OPTNOTE = {},
OPTANNOTE = {}
}
@PHDTHESIS{sthesis,
AUTHOR = {S.~S.~Kulkarni},
TITLE = {Component-based design of fault-tolerance},
SCHOOL = {Ohio State University},
YEAR = {1999},
OPTKEY = {},
OPTTYPE = {},
OPTADDRESS = {},
OPTMONTH = {},
OPTNOTE = {},
OPTANNOTE = {}
}
@ARTICLE{two-step,
AUTHOR = {A. Arora and S. S. Kulkarni},
TITLE = {Designing masking fault-tolerance via nonmasking fault-tolerance},
OPTCROSSREF = {},
OPTKEY = {},
JOURNAL = {IEEE Transactions on Software Engineering},
YEAR = {1998},
OPTVOLUME = {},
OPTNUMBER = {},
PAGES = {435--450},
MONTH = {June},
NOTE = {A preliminary version appears in the Proceedings of the Fourteenth Symposium on Reliable Distributed Systems, Bad Neuenahr, 1995, pages 174--185},
ANNOTE = {}
}
This file has been generated by bibtex2html 1.75