@article {12834,
	title = {Executable Specifications for Real-Time Distributed Systems},
	journal = {Electronic Notes in Theoretical Computer Science},
	volume = {203},
	year = {2008},
	month = {2008/06/05/},
	pages = {3 - 17},
	abstract = {One of the challenges in designing distributed, embedded systems is the paucity of formal, executable specification notations that provide support for both real-time and asynchronous communication. This paper describes a timed architecture design language (Timed Architecture Interaction Diagrams or TAID) that, by virtue of its formal, executable semantics, combines the benefits of synchronous specification notations with the advantages of traditional architecture description languages. In addition, TAID provides support for a variety of temporal inter-process communication (IPC) primitives as a native feature of the language, so that the encapsulated communication behavior (captured by real-time {\^a}{\texteuro}{\oe}buses{\^a}{\texteuro} in TAID) may be re-used across designs and serve as specifications for more detailed model implementations.},
	keywords = {distributed systems, Formal Methods, real-time, Simulations, Software architecture},
	isbn = {1571-0661},
	doi = {10.1016/j.entcs.2008.05.007},
	url = {http://www.sciencedirect.com/science/article/pii/S1571066108003216},
	author = {Ray,Arnab and Cleaveland, Rance}
}
@article {12813,
	title = {An Algebraic Theory Of Boundary Crossing Transitions},
	journal = {Electronic Notes in Theoretical Computer Science},
	volume = {115},
	year = {2005},
	month = {2005/01/18/},
	pages = {69 - 88},
	abstract = {This paper gives a process-algebraic semantics for the hierarchical state machine (HSM) fragment of Statecharts, in which state transitions are permitted to cross state boundaries. Although frowned upon by researchers as promoting unstructured modeling, such transitions are used extensively in practice to model parameterized start states and conditional exit states. The purpose of this work is to develop a compositional semantics for HSMs that may be fit together with compositional semantic accounts for Statecharts without boundary-crossing transitions in order to arrive at a compositional theory for virtually the whole Statecharts language. Our technical development consists of a process algebra for HSMs that is equipped with an operational semantics, an argument that bisimulation is a congruence for the algebra, a syntax-directed translation procedure for HSMs into the process algebra, and an equational axiomatization of the algebra.},
	keywords = {Compositional Semantics, Formal Methods, Process algebra, Statecharts},
	isbn = {1571-0661},
	doi = {10.1016/j.entcs.2004.09.029},
	url = {http://www.sciencedirect.com/science/article/pii/S1571066104053186},
	author = {Ray,Arnab and Cleaveland, Rance and Skou,Arne}
}
@conference {12852,
	title = {Efficient temporal-logic query checking for presburger systems},
	booktitle = {Proceedings of the 20th IEEE/ACM international Conference on Automated software engineering},
	series = {ASE {\textquoteright}05},
	year = {2005},
	month = {2005///},
	pages = {24 - 33},
	publisher = {ACM},
	organization = {ACM},
	address = {New York, NY, USA},
	abstract = {This paper develops a framework for solving temporal-logic query-checking problems for a class of infinite-state system models that compute with integer-valued variables (so-called Presburger systems, in which Presburger formulas are used to define system behavior). The temporal-logic query checking problem may be formulated as follows: given a model and a temporal logic formula with placeholders, compute a set of assignments of formulas to placeholders such that the resulting temporal formula is satisfied by the given model. Temporal-logic query checking has proved useful as a means for requirements and design understanding; existing work, however, has focused only on propositional temporal logic and finite-state systems.Our method is based on a symbolic model-checking technique that relies on proof search. The paper first introduces this model-checking approach and then shows how it can be adapted to solving the temporal queries in which formulas may contain integer variables. We also present experimental results showing the computational efficacy of our approach.},
	keywords = {Formal Methods, Model checking, on-the-fly symbolic model checking, Presburger systems, query checking},
	isbn = {1-58113-993-4},
	doi = {10.1145/1101908.1101915},
	url = {http://doi.acm.org/10.1145/1101908.1101915},
	author = {Zhang,Dezhuang and Cleaveland, Rance}
}
@article {12805,
	title = {Formal Modeling Of Middleware-based Distributed Systems},
	journal = {Electronic Notes in Theoretical Computer Science},
	volume = {108},
	year = {2004},
	month = {2004/12/13/},
	pages = {21 - 37},
	abstract = {Effective design of middleware-based systems requires modeling notations that allow the use of process-interaction schemes provided by different middleware packages directly in designs. Traditional design notations typically only support a fixed class of interprocess interaction schemes, and designers wishing to use them for modeling middleware-based systems must devote significant effort to encoding the middleware primitives in the notation. In this paper, we demonstrate how a new graphical design notation, Architectural Interaction Diagrams (AIDs), which provides parameterized support for different interaction schemes, may be used to model a real-life middleware-based system like the Event Heap coordination infrastructure of the i-Room ubiquitous computing environment.},
	keywords = {distributed systems, Formal Methods, Middleware, Software architecture},
	isbn = {1571-0661},
	doi = {10.1016/j.entcs.2004.01.010},
	url = {http://www.sciencedirect.com/science/article/pii/S1571066104051989},
	author = {Ray,Arnab and Cleaveland, Rance}
}
@article {18435,
	title = {Striving for correctness},
	journal = {Computers \& Security},
	volume = {14},
	year = {1995},
	month = {1995///},
	pages = {719 - 738},
	abstract = {In developing information technology, you want assurance that systems are secure and reliable, but you cannot have assurance or security without correctness. We discuss methods used to achieve correctness, focusing on weaknesses and approaches that management might take to increase belief in correctness. Formal methods, simulation, testing, and process modeling are addressed in detail. Structured programming, life-cycle modeling like the spiral model, use of CASE tools, use of formal methods, object-oriented design, reuse of existing code are also mentioned. Reliance on these methods involves some element of belief since no validated metrics on the effectiveness of these methods exist. Suggestions for using these methods as the basis for managerial decisions conclude the paper.},
	keywords = {Assurance, belief, correctness, Formal Methods, MATHEMATICAL MODELS, metrics, Process models, Risk management, Security testing, Silver bullets, simulation, Trustworthiness},
	isbn = {0167-4048},
	doi = {10.1016/0167-4048(95)00022-4},
	url = {http://www.sciencedirect.com/science/article/pii/0167404895000224},
	author = {Abrams,Marshall D. and Zelkowitz, Marvin V}
}
