@conference {16336,
	title = {Specification-based Testing of Reactive Software: Tools and Experiments},
	booktitle = {Software Engineering, International Conference on},
	year = {1997},
	month = {1997///},
	pages = {525 - 525},
	publisher = {IEEE Computer Society},
	organization = {IEEE Computer Society},
	address = {Los Alamitos, CA, USA},
	abstract = {Testing commercial software is expensive and time consuming. Automated testing methods promise to save a great deal of time and money throughout the software industry. One approach that is well-suited for the reactive systems found in telephone switching systems is specification-based testing.We have built a set of tools to automatically test softmare applications for violations of safety properties expressed in temporal logic. Our testing system automatically constructs finite state machine oracles corresponding to safety properties, builds test harnesses, and integrates them with the application. The test harness then generates inputs automatically to test the application.We describe a study examining the feasibility of this approach for testing industrial applications. To conduct this study we formally modeled an Automatic Protection Switching system (APS), which is an application common to many telephony systems. We then asked a number of computer science graduate students to develop several versions of the APS and use our tools to test them. We found that the tools are very effective, save significant amounts of human effort (at the expense of machine resources), and are easy to use. We also discuss improvements that are needed before we can use the tools with professional developers building commercial products.},
	keywords = {empirical studies, reactive systems, specification-based testing, temporal logic},
	doi = {http://doi.ieeecomputersociety.org/10.1109/ICSE.1997.610373},
	author = {Jagadeesan,Lalita Jategaonkar and Porter, Adam and Puchol,Carlos and Ramming,J. Christopher and Votta,Lawrence G.}
}
@conference {12799,
	title = {Efficient model checking via the equational μ-calculus},
	booktitle = {, Eleventh Annual IEEE Symposium on Logic in Computer Science, 1996. LICS {\textquoteright}96. Proceedings},
	year = {1996},
	month = {1996/07/27/30},
	pages = {304 - 312},
	publisher = {IEEE},
	organization = {IEEE},
	abstract = {This paper studies the use of an equational variant of the modal μ-calculus as a unified framework for efficient temporal logic model checking. In particular we show how an expressive temporal logic, CTL*, may be efficiently translated into the μ-calculus. Using this translation, one may then employ μ-calculus model-checking techniques, including on-the-fly procedures, BDD-based algorithms and compositional model-checking approaches, to determine if systems satisfy formulas in CTL*},
	keywords = {Automata, BDD-based algorithms, Boolean functions, Calculus, compositional model-checking approaches, computational complexity, Computer science, CTL*, Data structures, Encoding, equational variant, equational μ-calculus, Equations, expressive temporal logic, Logic, Maintenance, modal μ-calculus, Model checking, on-the-fly procedures, Surges, temporal logic, temporal logic model checking, unified framework},
	isbn = {0-8186-7463-6},
	doi = {10.1109/LICS.1996.561358},
	author = {Bhat,G. and Cleaveland, Rance}
}
@conference {12787,
	title = {Efficient on-the-fly model checking for CTL},
	booktitle = {, Tenth Annual IEEE Symposium on Logic in Computer Science, 1995. LICS {\textquoteright}95. Proceedings},
	year = {1995},
	month = {1995/06/26/29},
	pages = {388 - 397},
	publisher = {IEEE},
	organization = {IEEE},
	abstract = {This paper gives an on-the-fly algorithm for determining whether a finite-state system satisfies a formula in the temporal logic CTL. The time complexity of our algorithm matches that of the best existing {\textquotedblleft}global algorithm{\textquotedblright} for model checking in this logic, and it performs as well as the best known global algorithms for the sublogics CTL and LTL. In contrast with these approaches, however, our routine constructs the state space of the system under consideration in a need-driven fashion and will therefore perform better in practice},
	keywords = {Algorithm design and analysis, Automata, computational complexity, Computer science, CTL, Encoding, finite automata, finite-state system, global algorithm, Logic, LTL, on-the-fly model checking, Performance analysis, Safety, State-space methods, sublogic, temporal logic, time complexity},
	isbn = {0-8186-7050-9},
	doi = {10.1109/LICS.1995.523273},
	author = {Bhat,G. and Cleaveland, Rance and Grumberg,O.}
}
@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.}
}
