@article {12795,
	title = {Priority and abstraction in process algebra},
	journal = {Information and Computation},
	volume = {205},
	year = {2007},
	month = {2007/09//},
	pages = {1426 - 1458},
	abstract = {More than 15 years ago, Cleaveland and Hennessy proposed an extension of the process algebra CCS in which some actions may take priority over others. The theory was equipped with a behavioral congruence based on strong bisimulation.This article gives a full account of the challenges in, and the solutions employed for, defining a semantic theory of observation congruence for this process algebra. A full-abstraction result is presented whose proof relies on a novel approach based on successive approximations for identifying the largest congruence contained in an intuitive but na{\~A}{\textasciimacron}ve equivalence. Prioritized observation congruence is also characterized equationally for the class of finite processes, while its utility for system verification is demonstrated by an illustrative example.
},
	keywords = {Axiomatization, Bisimulation, Full abstraction, Observation congruence, Priority, Process algebra},
	isbn = {0890-5401},
	doi = {10.1016/j.ic.2007.05.001},
	url = {http://www.sciencedirect.com/science/article/pii/S0890540107000624},
	author = {Cleaveland, Rance and L{\~A}{\textonequarter}ttgen,Gerald and Natarajan,V.}
}
@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}
}
@article {12822,
	title = {Generic tools for verifying concurrent systems},
	journal = {Science of Computer Programming},
	volume = {42},
	year = {2002},
	month = {2002/01//},
	pages = {39 - 47},
	abstract = {Despite the enormous strides made in automatic verification technology over the past decade and a half, tools such as model checkers remain relatively underused in the development of software. One reason for this is that the bewildering array of specification and verification formalisms complicates the development and adoption by users of relevant tool support. This paper proposes a remedy to this state of affairs in the case of finite-state concurrent systems by describing an approach to developing customizable yet efficient verification tools.},
	keywords = {Model checking, Operational semantics, Process algebra, Specification, verification, Verification tools},
	isbn = {0167-6423},
	doi = {10.1016/S0167-6423(01)00033-8},
	url = {http://www.sciencedirect.com/science/article/pii/S0167642301000338},
	author = {Cleaveland, Rance and Sims,Steven T.}
}
@conference {12783,
	title = {Verifying an intelligent structural control system: a case study},
	booktitle = {Real-Time Systems Symposium, 1994., Proceedings.},
	year = {1994},
	month = {1994/12/07/9},
	pages = {271 - 275},
	publisher = {IEEE},
	organization = {IEEE},
	abstract = {Describes the formal verification of the timing properties of the design of an intelligent structural control system using the Concurrency Workbench, an automatic verification tool for finite-state processes. The high-level design of the system is first given in Modechart, a graphical specification language for real-time systems, and then translated into a temporal process algebra supported by the Workbench. The facilities provided by this tool are then used to analyze the system and ultimately show it to be correct},
	keywords = {automatic verification tool, case study, Concurrency Workbench, Distributed computing, Distributed control, distributed processing, finite automata, finite-state processes, formal verification, graphical specification language, high-level design, intelligent control, intelligent structural control system verification, Logic, Modechart, Process algebra, Real time systems, real-time systems, Specification languages, structural engineering computing, temporal logic, temporal process algebra, time-varying systems, Timing, timing properties, visual languages},
	isbn = {0-8186-6600-5},
	doi = {10.1109/REAL.1994.342708},
	author = {Elseaidy,W. M and Cleaveland, Rance and Baugh,J. W.}
}
@conference {12796,
	title = {RTSL: a language for real-time schedulability analysis},
	booktitle = {Real-Time Systems Symposium, 1993., Proceedings.},
	year = {1993},
	month = {1993/12/01/3},
	pages = {274 - 283},
	publisher = {IEEE},
	organization = {IEEE},
	abstract = {The paper develops a generalized approach to schedulability analysis that is mathematically founded in a process algebra called RTSL. Within RTSL one may describe the functional behavior, timing behavior, timing constraints (or deadlines), and scheduling discipline for real-time systems. The formal semantics of RTSL then allows the reachable state space of finite state systems to be automatically generated and searched for timing exceptions. We provide a generalized schedulability analysis technique to perform this state-based analysis},
	keywords = {Algebra, Algorithm design and analysis, Dynamic scheduling, Failure analysis, finite state machines, finite state systems, formal logic, formal semantics, functional behavior, generalized approach, generalized schedulability analysis technique, Process algebra, Processor scheduling, reachable state space, Real time systems, real-time schedulability analysis, Real-Time Specification Language, real-time systems, RTSL, scheduling, Scheduling algorithm, scheduling discipline, Specification languages, state-based analysis, State-space methods, Time factors, Timing, timing behavior, timing constraints, timing exceptions},
	isbn = {0-8186-4480-X},
	doi = {10.1109/REAL.1993.393489},
	author = {Fredette,A. N and Cleaveland, Rance}
}
