Article

Free access

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

Authors:

William E. WarnerAuthors Info & Claims

ICSE '99: Proceedings of the 21st international conference on Software engineering

Pages 142 - 151

https://doi.org/10.1145/302405.302460

Published: 16 May 1999 Publication History

PDF eReader

References

[1]

G. Berry and G. Gonthier. The ESTEREL synchronous programming language: Design, semantics, implementation. Science of Computer Programming, 19(2):87-152, November 1992.

Digital Library

Google Scholar

[2]

M. C. Browne, E. M. Clarke, and 0. Griimberg. Characterizing finite Kripke structures in propositional temporal logic. Theoretical Computer Science, 59( l/Z): 115-131, July 1988.

Digital Library

Google Scholar

[3]

R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, 35(6):677- 691, August 1986.

Digital Library

Google Scholar

[4]

J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(Z): 142-170, June 1992.

Digital Library

Google Scholar

[5]

G. Cabodi, P. Camurati, and S. Quer. Improved reachability analysis of large finite state machines. In 1996 IEEE/ACM International Conference on Computer-Aided Design, Digest of Technical Papers, pages 10-14, San Jose, California, USA, November 1996.

Digital Library

Google Scholar

[6]

W. Chan, R. J. Anderson, P. Beame, S. Burns, F. Modugno, D. Notkin, and J. D. Reese. Model checking large software specifications. IEEE Transactions on Software Engineering, 24(7):498-520, July 1998.

Digital Library

Google Scholar

[7]

W. Chan, R. J. Anderson, P. Beame, and D. Notkin. Improving efficiency of symbolic model checking for state-based system requirements. In M. Young, editor, ISSTA 98: Proceedings of the ACM SIGSOFT International Symposium on Software Testing andAnalysis, pages 102-l 12, Clearwater Beach, Florida, USA, March 1998. Published as Software Engineering Notes, 23(2).

Digital Library

Google Scholar

[8]

E. M. Clarke, E. A. Emerson, and A. P Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244-263, April 1986.

Digital Library

Google Scholar

[9]

O. Coudert, C. Berthet, and J. C. Madre. Verification of synchronous sequential machines based on symbolic execution. In J. Sifakis, editor, Automatic VerQication Methods for Finite State Systems: International Workshop Proceedings, volume 407 of Lecture Notes in Computer Science, pages 365-373, Grenoble, France, June 1989. Springer-Verlag.

Digital Library

Google Scholar

[10]

D. Harel. Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8(3):231-274, June 1987.

Digital Library

Google Scholar

[11]

D. Hare1 and A. Naamad. The STATEMATE semantics of statecharts. ACM Transactions on Software Engineering and Methodology, 5(4):293-333, October 1996.

Digital Library

Google Scholar

[12]

A. J. Hu and D. L. Dill. Efficient verification with BDDs using implicitly conjoined invariants. In C. Courcoubetis, editor, Computer Aided Veri$cation, 5th International Conference, CAV'93 Proceedings, volume 697 of Lecture Notes in Computer Science, pages 3-14, Elounda, Greece, June/July 1993. Springer-Verlag.

Crossref

Google Scholar

[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.

Google Scholar

[14]

N. G. Leveson, M. P E. Heimdahl, H. Hildreth, and J. D. Reese. Requirements specification for process-control systems. IEEE Transactions on Software Engineering, 20(9), September 1994.

Digital Library

Google Scholar

[15]

K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.

Digital Library

Google Scholar

[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.

Google Scholar

[17]

C. R. Nobe and W. E. Warner. Lessons learned from a trial application of requirements modeling using statecharts. In Proceedings of the 2nd International Conference on Requirements Engineering, pages 86-93, Colorado Springs, USA, April 1996. IEEE.

Digital Library

Google Scholar

[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.

Google Scholar

[19]

K. Ravi and E Somenzi. High-density reachability analysis. In 1995 IEEE/ACM International Conference on Computer- Aided Design, Digest of Technical Papers, pages 154-158, San Jose, California, USA, November 1995.

Digital Library

Google Scholar

[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.

Crossref

Google Scholar

Cited By

View all

Sugumar GSelvamuthukumaran RNovak MDragicevic T(2019)Supervisory Energy-Management Systems for Microgrids: Modeling and Formal VerificationIEEE Industrial Electronics Magazine10.1109/MIE.2019.289376813:1(26-37)Online publication date: Mar-2019
https://doi.org/10.1109/MIE.2019.2893768
Karna AChen YYu HZhong HZhao J(2018)The role of model checking in software engineeringFrontiers of Computer Science: Selected Publications from Chinese Universities10.1007/s11704-016-6192-012:4(642-668)Online publication date: 1-Aug-2018
https://dl.acm.org/doi/10.1007/s11704-016-6192-0
Qianchuan Zhao Krogh B(2006)Formal verification of statecharts using finite-state model checkersIEEE Transactions on Control Systems Technology10.1109/TCST.2006.87692114:5(943-950)Online publication date: Sep-2006
https://doi.org/10.1109/TCST.2006.876921
Show More Cited By

Index Terms

Decoupling synchronization from local control for efficient symbolic model checking of statecharts
1. Software and its engineering
  1. Software creation and management
    1. Designing software
      1. Requirements analysis
  2. Software organization and properties
    1. Software functional properties
      1. Formal methods
        Model checking
2. Theory of computation
  1. Logic
    1. Verification by model checking

Recommendations

Optimizing Symbolic Model Checking for Statecharts
Special issue on 1999 international conference on software engineering

Symbolic model checking based on binary decision diagrams is a powerful formal verification technique for reactive systems. In this paper, we present various optimizations for improving the time and space efficiency of symbolic model checking for systems ...
Model Checking Large Software Specifications

In this paper, we present our experiences in using symbolic model checking to analyze a specification of a software system for aircraft collision avoidance. Symbolic model checking has been highly successful when applied to hardware systems. We are ...
Improving efficiency of symbolic model checking for state-based system requirements
ISSTA '98: Proceedings of the 1998 ACM SIGSOFT international symposium on Software testing and analysis

We present various techniques for improving the time and space efficiency of symbolic model checking for system requirements specified as synchronous finite state machines. We used these techniques in our analysis of the system requirements specification ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

ICSE '99: Proceedings of the 21st international conference on Software engineering

May 1999

741 pages

ISBN:1581130740

DOI:10.1145/302405

Chairmen:
Barry Boehm
Univ. of Southern Califoria, Los Angeles
,
David Garlan
Carnegie Mellon Univ., Pittsburgh, PA
,
Jeff Kramer
Imperial College, London, UK

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 16 May 1999

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

ICSE99

Sponsor:

SIGPLAN
SIGAda
SIGSOFT
IEEE-CS
IEEE-CS\TCSE

ICSE99: 1999 International Conference on Software Engineering

May 16 - 22, 1999

California, Los Angeles, USA

Acceptance Rates

Overall Acceptance Rate 276 of 1,856 submissions, 15%

Upcoming Conference

ICSE 2025

2025 IEEE/ACM 46th International Conference on Software Engineering

April 26 - May 3, 2025

Ottawa , ON , Canada

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

13
Total Citations
View Citations
327
Total Downloads

Downloads (Last 12 months)61
Downloads (Last 6 weeks)11

Reflects downloads up to 20 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Sugumar GSelvamuthukumaran RNovak MDragicevic T(2019)Supervisory Energy-Management Systems for Microgrids: Modeling and Formal VerificationIEEE Industrial Electronics Magazine10.1109/MIE.2019.289376813:1(26-37)Online publication date: Mar-2019
https://doi.org/10.1109/MIE.2019.2893768
Karna AChen YYu HZhong HZhao J(2018)The role of model checking in software engineeringFrontiers of Computer Science: Selected Publications from Chinese Universities10.1007/s11704-016-6192-012:4(642-668)Online publication date: 1-Aug-2018
https://dl.acm.org/doi/10.1007/s11704-016-6192-0
Qianchuan Zhao Krogh B(2006)Formal verification of statecharts using finite-state model checkersIEEE Transactions on Control Systems Technology10.1109/TCST.2006.87692114:5(943-950)Online publication date: Sep-2006
https://doi.org/10.1109/TCST.2006.876921
Shankar SAsa SSipos VXu XRedmiles DEllman TZisman A(2005)Reasoning about real-time statecharts in the presence of semantic variationsProceedings of the 20th IEEE/ACM International Conference on Automated Software Engineering10.1145/1101908.1101945(243-252)Online publication date: 7-Nov-2005
https://dl.acm.org/doi/10.1145/1101908.1101945
Yavuz-Kahveci TBultan T(2005)Verification of parameterized hierarchical state machines using action language verifierProceedings of the 2nd ACM/IEEE International Conference on Formal Methods and Models for Co-Design10.1109/MEMCOD.2005.1487897(79-88)Online publication date: 11-Jul-2005
https://dl.acm.org/doi/10.1109/MEMCOD.2005.1487897
Penix JVisser WPark SPasareanu CEngstrom ELarson AWeininger N(2005)Verifying Time Partitioning in the DEOS Scheduling KernelFormal Methods in System Design10.1007/s10703-005-1490-426:2(103-135)Online publication date: 1-Mar-2005
https://dl.acm.org/doi/10.1007/s10703-005-1490-4
Chechik MDing W(2002)Lightweight Reasoning about Program CorrectnessInformation Systems Frontiers10.1023/A:10208836254954:4(363-377)Online publication date: 1-Dec-2002
https://dl.acm.org/doi/10.1023/A%3A1020883625495
Chechik MDing WHarris HWoodsworth ABauer MJohnson J(2001)Lightweight reasoning about program correctnessProceedings of the 2001 conference of the Centre for Advanced Studies on Collaborative research10.5555/782096.782097Online publication date: 5-Nov-2001
https://dl.acm.org/doi/10.5555/782096.782097
Qianchuan Zhao Krogh B(2001)Formal verification of Statecharts using finite-state model checkersProceedings of the 2001 American Control Conference. (Cat. No.01CH37148)10.1109/ACC.2001.945563(313-318 vol.1)Online publication date: 2001
https://doi.org/10.1109/ACC.2001.945563
Chan WAnderson RBeame PNotkin DJones DWarner W(2001)Optimizing Symbolic Model Checking for StatechartsIEEE Transactions on Software Engineering10.1109/32.90896127:2(170-190)Online publication date: 1-Feb-2001
https://dl.acm.org/doi/10.1109/32.908961
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Index Terms

Recommendations

Optimizing Symbolic Model Checking for Statecharts

Model Checking Large Software Specifications

Improving efficiency of symbolic model checking for state-based system requirements