@misc{spin-site,
  key = {SPIN},
  note = {SPIN web site \url{http://netlib.bell-labs.com/netlib/spin/whatispin.html}},
  url = {http://netlib.bell-labs.com/netlib/spin/whatispin.html}
}

@misc{vandv-site,
  key = {VV},
  note = {Verification \& Validation web site \url{http://ase.arc.nasa.gov/docs/vandv.html}},
  url = {http://ase.arc.nasa.gov/docs/vandv.html}
}

@misc{assurance-site,
  key = {NASA},
  note = {NASA Software Assurance Technology Center web site \url{http://satc.gsfc.nasa.gov/assure/agbsec5.txt}},
  url = {http://satc.gsfc.nasa.gov/assure/agbsec5.txt}
}

@misc{telelogic-site,
  key = {Telelogic},
  note = {Telelogic web site \url{http://www.telelogic.com/}},
  url = {http://www.telelogic.com/}
}

@article{1028100,
  author = {Ronen I. Brafman and Carmel Domshlak and Solomon E. Shimony},
  doi = {http://doi.acm.org/10.1145/1028099.1028100},
  issn = {1046-8188},
  journal = {ACM Trans. Inf. Syst.},
  number = {4},
  pages = {503--539},
  publisher = {ACM Press},
  title = {Qualitative decision making in adaptive presentation of structured information},
  volume = {22},
  year = {2004}
}

@inproceedings{sen04statistical,
  author = {K. Sen and M. Viswanathan and G. Agha},
  title = {Statistical model checking of black-box probabilistic systems},
  booktitle = {16th conference on Computer Aided Verification (CAV)},
  month = {July},
  year = {2004},
  pages = {202--215},
  volume = {3114},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  http = {citeseer.ist.psu.edu/sen04statistical.html},
  pdf = {http://www-osl.cs.uiuc.edu/docs/statver/statver.pdf},
  abstract = {We propose a new statistical approach to analyzing stochastic systems against specifications given in a sublogic of continuous stochastic logic (CSL). Unlike past numerical and statistical analysis methods, we assume that the system under investigation is an unknown, deployed black-box that can be passively observed to obtain sample traces, but cannot be controlled. Given a set of executions (obtained by Monte Carlo simulation) and a property, our algorithm checks, based on statistical hypothesis testing, whether the sample provides evidence to conclude the satisfaction or violation of a property, and computes a quantitative measure (p-value of the tests) of confidence in its answer; if the sample does not provide statistical evidence to conclude the satisfaction or violation of the property, the algorithm may respond with a ''don't know'' answer. We implemented our algorithm in a Java-based prototype tool called VeStA, and experimented with the tool using case studies analyzed in [15]. Our empirical results show that our approach may, at least in some cases, be faster than previous analysis methods. }
}

@inproceedings{Agha2005,
  author = {Gul Agha and Carl Gunter and Michael Greenwald and Sanjeev Khanna and Jose Meseguer and Koushik Sen and Prasanna Thati},
  title = {Formal Modeling and Analysis of {DoS} Using Probabilistic Rewrite Theories},
  booktitle = {Workshop on Foundations of Computer Security (FCS)},
  optpages = {},
  year = {2005},
  optvolume = {},
  optnumber = {},
  optseries = {},
  month = {June},
  pdf = {http://www-faculty.cs.uiuc.edu/~cgunter/dist/AghaGGKMST05.pdf},
  abstract = {Existing models for analyzing the integrity and confidentiality of protocols need to be extended to enable the analysis of availability. Prior work on such extensions shows promising applications to the development of new DoS countermeasures. Ideally it should be possible to apply these countermeasures systematically in a way that preserves desirable properties already established. This paper investigates a step toward achieving this ideal by describing a way to expand term rewriting theories to include probabilitic aspects that can show the effectiveness of DoS countermeasures. In particular, we consider the shared channel model, in which adversaries and valid participants share communication bandwidth according to a probabilistic interleaving model, and a countermeasure known as selective verification applied to the handshake steps of the TCP reliable transport protocol. These concepts are formulated in a probabilistic extension of the Maude term rewriting sytem and automated techniques are used to demonstrate the effectiveness of the countermeasures.}
}

@phdthesis{Par02,
  author = {D. Parker},
  title = {Implementation of Symbolic Model Checking for Probabilistic Systems},
  school = {University of Birmingham},
  month = {August},
  year = {2002},
  pdf = {http://www.cs.bham.ac.uk/~dxp/papers/davesthesis.pdf},
  abstract = {In this thesis, we present efficient implementation techniques for probabilistic model checking, a method which can be used to analyse probabilistic systems such as randomised distributed algorithms, fault-tolerant processes and communication networks. A probabilistic model checker inputs a probabilistic model and a specification, such as ''the message will be delivered with probability 1'', ''the probability of shutdown occurring is at most 0.02'' or ''the probability of a leader being elected within 5 rounds is at least 0.98'', and can automatically verify if the specification is true in the model. \par Motivated by the success of symbolic approaches to non-probabilistic model checking, which are based on a data structure called binary decision diagrams (BDDs), we present an extension to the probabilistic case, using multi-terminal binary decision diagrams (MTBDDs). We demonstrate that MTBDDs can be used to perform probabilistic analysis of large, structured models with more than 7.5 billion states, way out of the reach of conventional, explicit techniques, based on sparse matrices. We also propose a novel, hybrid approach, combining features of both symbolic and explicit implementations and show, using results from a wide range of case studies, that this technique can almost match the speed of sparse matrix based implementations, but uses significantly less memory. This increases, by approximately an order of magnitude, the size of model which can be handled on a typical workstation.}
}

@article{937558,
  author = {Jeremy Bryans and Howard Bowman and John Derrick},
  title = {Model checking stochastic automata},
  journal = {ACM Trans. Comput. Logic},
  volume = {4},
  number = {4},
  year = {2003},
  issn = {1529-3785},
  pages = {452--492},
  doi = {http://doi.acm.org/10.1145/937555.937558},
  publisher = {ACM Press},
  address = {New York, NY, USA},
  abstract = {Modern distributed systems include a class of applications in which non-functional requirements are important. In particular, these applications include multimedia facilities where real time constraints are crucial to their correct functioning. In order to specify such systems it is necessary to describe that events occur at times given by probability distributions; stochastic automata have emerged as a useful technique by which such systems can be specified and verified.However, stochastic descriptions are very general, in particular they allow the use of general probability distribution functions, and therefore their verification can be complex. In the last few years, model checking has emerged as a useful verification tool for large systems. In this article we describe two model checking algorithms for stochastic automata. These algorithms consider how properties written in a simple probabilistic real-time logic can be checked against a given stochastic automaton.}
}

@article{377990,
  author = {Rajeev Alur and Kousha Etessami and Salvatore La Torre and Doron Peled},
  title = {Parametric temporal logic for ``model measuring''},
  journal = {ACM Trans. Comput. Logic},
  volume = {2},
  number = {3},
  year = {2001},
  issn = {1529-3785},
  pages = {388--407},
  doi = {http://doi.acm.org/10.1145/377978.377990},
  publisher = {ACM Press},
  address = {New York, NY, USA},
  abstract = {We extend the standard model checking paradigm of linear temporal logic, LTL, to a ``model measuring'' paradigm where one can obtain more quantitative information beyond a ``Yes/No'' answer. For this purpose, we define a parametric temporal logic, PLTL, which allows statements such as ``a request p is followed in at most x steps by a response q,'' where x is a free variable. We show how one can, given a formula ***(x1...,xk) of PLTL and a system model K satisfies the property ***, but if so find valuations which satisfy various optimality criteria. In particular, we present algorithms for finding valuations which minimize (or maximize) the maximum (or minimum) of all parameters. Theses algorithms exhibit the same PSPACE complexity as LTL model checking. We show that our choice of syntax for PLTL lies at the threshold of decidability for parametric temporal logics, in that several natural extensions have undecidable ``model measuring'' problems.}
}

@article{Meseguer92,
  author = {Jos{\'e} Meseguer},
  issn = {0304-3975},
  journal = {Theoretical Computer Science},
  keywords = {concurrency conditional rewriting},
  month = {April},
  number = {1},
  pages = {73--155},
  publisher = {Elsevier Science Publishers Ltd.},
  title = {Conditional rewriting logic as a unified model of concurrency},
  doi = {http://dx.doi.org/10.1016/0304-3975(92)90182-F},
  volume = {96},
  year = {1992},
  abstract = {Rewriting with conditional rewrite rules modulo a set $E$ of structural axioms provides a general framework for unifying a wide variety of models of concurrency. Concurrent rewriting coincides with logical deduction in \textit{conditional rewriting logic}, a logic of actions whose models are concurrent systems. This logic is sound and complete and has initial models. In addition to general models interpreted as concurrent systems which provide a more operational style of semantics, more restricted semantics with an incresingly denotational flavor such as preorder, poset, cpo, and standard algebraic models appear as special cases of the model theory. This permits dealing with operational and denotational issues within the same model theory and logic. A programming language called Maude whose modules are rewriting logic theories is defined and given denotational and operational semantics. Maude provides a simple unification of concurrent programming with functional and object-oriented programming and supports high level declarative programming of concurrent systems.}
}

This file was generated by bibtex2html 1.96.