Decoupling synchronization from local control for efficient symbolic model checking of statecharts

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Decoupling synchronization from local control for efficient symbolic model checking of statecharts

Full text

Pdf (1.31 MB)

Source

International Conference on Software Engineering archive
Proceedings of the 21st international conference on Software engineering table of contents

Los Angeles, California, United States

Pages: 142 - 151

Year of Publication: 1999

ISBN:1-58113-074-0

Authors

William Chan	Department of Computer Science and Engineering, University of Washington, Box 352350, Seattle, Washington
Richard J. Anderson	Department of Computer Science and Engineering, University of Washington, Box 352350, Seattle, Washington
Paul Beame	Department of Computer Science and Engineering, University of Washington, Box 352350, Seattle, Washington
David H. Jones	The Boeing Company, Seattle, Washington
David Notkin	Department of Computer Science and Engineering, University of Washington, Box 352350, Seattle, Washington
William E. Warner	The Boeing Company, Seattle, Washington

Sponsors

IEEE-CS : Computer Society
IEEE-CS\TCSE : TC on Software Engineering
SIGADA: ACM Special Interest Group on Ada Programming Language
SIGSOFT: ACM Special Interest Group on Software Engineering
SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 3, Downloads (12 Months): 18, Citation Count: 7

Additional Information:

references cited by index terms collaborative colleagues

Tools and Actions:	Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/302405.302460 What is a DOI?

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Gérard Berry , Georges Gonthier, The ESTEREL synchronous programming language: design, semantics, implementation, Science of Computer Programming, v.19 n.2, p.87-152, Nov. 1992 [doi>10.1016/0167-6423(92)90005-V]
	2	M. C. Browne , E. M. Clarke , O. Grümberg, Characterizing finite Kripke structures in propositional temporal logic, Theoretical Computer Science, v.59 n.1-2, p.115-131, July 1988 [doi>10.1016/0304-3975(88)90098-9]
	3	Randal E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, Aug. 1986 [doi>10.1109/TC.1986.1676819]
	4	J. R. Burch , E. M. Clarke , K. L. McMillan , D. L. Dill , L. J. Hwang, Symbolic model checking: 1020 states and beyond, Information and Computation, v.98 n.2, p.142-170, June 1992 [doi>10.1016/0890-5401(92)90017-A]
	5	Gianpiero Cabodi , Paolo Camurati , Stefano Quer, Improved reachability analysis of large finite state machines, Proceedings of the 1996 IEEE/ACM international conference on Computer-aided design, p.354-360, November 10-14, 1996, San Jose, California, United States
	6	William Chan , Richard J. Anderson , Paul Beame , Steve Burns , Francesmary Modugno , David Notkin , Jon D. Reese, Model Checking Large Software Specifications, IEEE Transactions on Software Engineering, v.24 n.7, p.498-520, July 1998 [doi>10.1109/32.708566]
	7	William Chan , Richard J. Anderson , Paul Beame , David Notkin, Improving efficiency of symbolic model checking for state-based system requirements, Proceedings of the 1998 ACM SIGSOFT international symposium on Software testing and analysis, p.102-112, March 02-04, 1998, Clearwater Beach, Florida, United States
	8	E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
	9	O. Coudert , C. Berthet , J. C. Madre, Verification of synchronous sequential machines based on symbolic execution, Proceedings of the international workshop on Automatic verification methods for finite state systems, p.365-373, February 1990, Grenoble, France
	10	David Harel, Statecharts: A visual formalism for complex systems, Science of Computer Programming, v.8 n.3, p.231-274, June 1, 1987 [doi>10.1016/0167-6423(87)90035-9]
	11	David Harel , Amnon Naamad, The STATEMATE semantics of statecharts, ACM Transactions on Software Engineering and Methodology (TOSEM), v.5 n.4, p.293-333, Oct. 1996 [doi>10.1145/235321.235322]
	12	Alan J. Hu , David L. Dill, Efficient Verification with BDDs using Implicitly Conjoined Invariants, Proceedings of the 5th International Conference on Computer Aided Verification, p.3-14, June 28-July 01, 1993
	13	L. Lamport. What good is temporal logic? In R. E. A. Mason, editor, Information Processing 83: Proceedings of the IFIP 9th World Computer Congress, pages 657-668, Paris, France, September 1983. North Holland.
	14	Nancy G. Leveson , Mats Per Erik Heimdahl , Holly Hildreth , Jon D. Reese, Requirements Specification for Process-Control Systems, IEEE Transactions on Software Engineering, v.20 n.9, p.684-707, September 1994 [doi>10.1109/32.317428]
	15	Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
	16	C. R. Nobe and M. G. Bingle. Model-based development: Five processes used at Boeing. In Proceedings of the IEEE International Conference and Workshop: Engineering of Computer-Based Systems, Jerusalem, Israel, March/April 1998.
	17	C. R. Nobe , W. E. Warner, Lessons Learned from a Trial Application of Requirements Modeling Using Statecharts, Proceedings of the 2nd International Conference on Requirements Engineering (ICRE '96), p.86, April 15-18, 1996
	18	R. K. Ranjan, A. Aziz, R. K. Brayton, B. Plessier, and C. Pixley. Efficient BDD algorithms for FSM synthesis and verification. In Proceedings of IEEE/ACM International Workshop on Logic Synthesis, Lake Tahoe, USA, May 1995.
	19	Kavita Ravi , Fabio Somenzi, High-density reachability analysis, Proceedings of the 1995 IEEE/ACM international conference on Computer-aided design, p.154-158, November 05-09, 1995, San Jose, California, United States
	20	T. Sreemani and J. M. Atlee. Feasibility of model checking software requirements: A case study. In COMPASS'96, Proceedings of the 11th Annual Conference on Computer Assurance, pages 77-88, Gaithersburg, Maryland, USA, June 1996. IEEE.

CITED BY 7

	John Penix , Willem Visser , Eric Engstrom , Aaron Larson , Nicholas Weininger, Verification of time partitioning in the DEOS scheduler kernel, Proceedings of the 22nd international conference on Software engineering, p.488-497, June 04-11, 2000, Limerick, Ireland
	William Visser , SeungJoon Park , John Penix, Using predicate abstraction to reduce object-oriented programs for model checking, Proceedings of the third workshop on Formal methods in software practice, p.3-182, August 2000, Portland, Oregon, United States
	Marsha Chechik , Wei Ding, Lightweight reasoning about program correctness, Proceedings of the 2001 conference of the Centre for Advanced Studies on Collaborative research, p.1, November 05-07, 2001, Toronto, Ontario, Canada
	William Chan , Richard J. Anderson , Paul Beame , David Notkin , David H. Jones , William E. Warner, Optimizing Symbolic Model Checking for Statecharts, IEEE Transactions on Software Engineering, v.27 n.2, p.170-190, February 2001
	Subash Shankar , Sinan Asa , Vladimir Sipos , Xiaowei Xu, Reasoning about real-time statecharts in the presence of semantic variations, Proceedings of the 20th IEEE/ACM international Conference on Automated software engineering, November 07-11, 2005, Long Beach, CA, USA
	John Penix , Willem Visser , Seungjoon Park , Corina Pasareanu , Eric Engstrom , Aaron Larson , Nicholas Weininger, Verifying Time Partitioning in the DEOS Scheduling Kernel, Formal Methods in System Design, v.26 n.2, p.103-135, March 2005
	Marsha Chechik , Wei Ding, Lightweight Reasoning about Program Correctness, Information Systems Frontiers, v.4 n.4, p.363-377, December 2002