article

Free access

Model checking graphical user interfaces using abstractions

Authors:

Matthew B. Dwyer,

Laura HinesAuthors Info & Claims

ACM SIGSOFT Software Engineering Notes, Volume 22, Issue 6

Pages 244 - 261

https://doi.org/10.1145/267896.267914

Published: 01 November 1997 Publication History

First page of PDF

References

[1]

R. Anderson, P. Beame, S. Burns, W. Chan, F. Modugno, D. Notkin, and J. Reese. Model checking large software specifications. Software Engineering Notes, 21(6):156-166, Nov. 1996. Proceedings of the Fourth ACM SIGSOFT Symposium on the Foundations of Software Engineering.

Digital Library

[2]

G. Avrunin, U. Buy, J. Corbett, L. Dillon, and J. Wileden. Automated analysis of concurrent systems with the constrained expression toolset, IEEE Transactions on Software Engineering, 17(11):1204-1222, Nov. 1991,

Digital Library

[3]

E. Clarke, O. G rumberg, and D. Long. Model checking and abstraction, ACM Tbnsactions on Programming Languages and Systems, 16(5):1512- 1542, Sept. 1994.

Digital Library

[4]

R. Cleaveland, J. Parrow, and B. Steffen. The concurrency workbench: A semantics based tool for the verification of concurrent systems. ACM fiansactions on Programming Languages and Systems, 15(1):36-72, Jan. 1993,

Digital Library

[5]

J. Corbett. Evaluating deadlock detection methods for concurrent software. IEEE Transactions on Software Engineering, 22(3), Mar. 1996.

Digital Library

[6]

D. Dams. Abstract Interpretation and Partition Refinement for Model Checlting. PhD thesis, Eindhoven University of Technology, May 1996.

[7]

L. K. Dillon, G. Kutty, L. E. Moser, P. M. Melliar-Smith, and Y. S. Ramakrishna. A graphical interval logic for specifying concurrent systems. ACM Transactions on Software Engineering and Methodology, 3(2):131-165, Apr. 1994.

Digital Library

[8]

M. Dwyer and L. Clarke. Data flow analysis for verifying properties of concurrent programs. Software Engineering Notes, 19(5):62-75, Dec. 1994. Proceedings of the ACM SIGSOFT Symposium on the Foundations of Software Engineering.

Digital Library

[9]

D. Jackson. Abstract model checking of infinite specifications. In Proceedings of FME'94 : Industrial Benefit of Formal Methods, Second International Symposium of Formal Methods Europe, pages 519-531, Oct. 1994. Springer-Verlag.

Digital Library

[10]

R. Jacob. Using formal specifications in the design of a human-computer interface. Communications of the ACM, 26(4):259-264, Apr. 1983.

Digital Library

[11]

Z. Manna and A. Pnueli. The Tempoml Logic of Reactive and Concurrent Systems : Specification. Springer-Verlag, 1991.

Digital Library

[12]

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

Digital Library

[13]

B. Myers. User interface software tools. ACM Transactions on Computer- Human Interaction, 2(1):64-103, Mar. 1995.

Digital Library

[14]

K. Olender and L. Osterweil. Cecil: A sequencing constraint language for automatic static analysis generation. IEEE Tmnsactions on Software Engineering, 16(3):268-280, Mar. 1990.

Digital Library

[15]

A. Wasserman. Extending state transition diagrams for the specification of human-computer interaction. IEEE Transactions on Software Engineering, SE11(8):699-713, Aug. 1985.

Digital Library

[16]

J. Wing and M. Vaziri-Farahani. Model checking software systems : A case study. Software Engineering Notes, 20(4):128-139, Oct. 1995. Proceedings of the Third ACM SIGSOFT Symposium on the Foundations of Software Engineering.

Digital Library

[17]

M. Young, R. Taylor, D. Levine, K. Nies, and D. Brodbeck. A concurrency analysis tool suite: Rationale, design, and preliminary experience. ACM fiansactions on Software Engineering and Methodology, 4(1):64-106, Jan. 1995.

Digital Library

Cited By

Geng MZhang XLi J(2021)Finding More Property Violations in Model Checking via the Restart PolicyElectronics10.3390/electronics1023295710:23(2957)Online publication date: 27-Nov-2021
https://doi.org/10.3390/electronics10232957
Nguyen BMemon A(2014)An Observe-Model-Exercise* Paradigm to Test Event-Driven Systems with Undetermined Input SpacesIEEE Transactions on Software Engineering10.1109/TSE.2014.230085740:3(216-234)Online publication date: 1-Mar-2014
https://dl.acm.org/doi/10.1109/TSE.2014.2300857
SKVORC DZUZAK ISRBLJIC S(2012)Formal Model for Data Dependency Analysis between Controls and Actions of a Graphical User InterfaceAdvances in Electrical and Computer Engineering10.4316/aece.2012.0101112:1(63-70)Online publication date: 2012
https://doi.org/10.4316/aece.2012.01011
Show More Cited By

Index Terms

Model checking graphical user interfaces using abstractions
1. Human-centered computing
  1. Human computer interaction (HCI)
    1. Interactive systems and tools
      1. User interface management systems
2. Software and its engineering
  1. Software notations and tools
    1. Development frameworks and environments
      1. Integrated and visual development environments

Recommendations

Graphical user interfaces

This article provides a brief introduction to graphical user interfaces or GUIs. The first section defines graphical user interfaces, describes interface components, and the different types of GUIs. This is followed by a short discussion of GUI design ...
Creating highly-interactive and graphical user interfaces by demonstration

It is very time-consuming and expensive to create the graphical, highly-interactive styles of user interfaces that are increasingly common. User Interface Management Systems (UIMSs) attempt to make the creation of user interfaces easier, but most ...
Transforming graphical interfaces into auditory interfaces

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGSOFT Software Engineering Notes

ACM SIGSOFT Software Engineering Notes Volume 22, Issue 6

Nov. 1997

527 pages

ISSN:0163-5948

DOI:10.1145/267896

Editors:
Mehdi Jazayeri
Technische Univ. Wien, Vienna, Austria
,
Helmut Schauer
Univ. of Zurich, Zurich, Switzerland

Issue’s Table of Contents

ESEC '97/FSE-5: Proceedings of the 6th European SOFTWARE ENGINEERING conference held jointly with the 5th ACM SIGSOFT international symposium on Foundations of software engineering
November 1997
536 pages
ISBN:3540635319
Editors:
Mehdi Jazayeri
Technische Univ. Wien, Vienna, Austria
,
Helmut Schauer
Univ. Zurich, Zurich, Switzerland

Copyright © 1997 Authors.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 November 1997

Published in SIGSOFT Volume 22, Issue 6

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

26
Total Citations
View Citations
798
Total Downloads

Downloads (Last 12 months)115
Downloads (Last 6 weeks)20

Reflects downloads up to 29 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Geng MZhang XLi J(2021)Finding More Property Violations in Model Checking via the Restart PolicyElectronics10.3390/electronics1023295710:23(2957)Online publication date: 27-Nov-2021
https://doi.org/10.3390/electronics10232957
Nguyen BMemon A(2014)An Observe-Model-Exercise* Paradigm to Test Event-Driven Systems with Undetermined Input SpacesIEEE Transactions on Software Engineering10.1109/TSE.2014.230085740:3(216-234)Online publication date: 1-Mar-2014
https://dl.acm.org/doi/10.1109/TSE.2014.2300857
SKVORC DZUZAK ISRBLJIC S(2012)Formal Model for Data Dependency Analysis between Controls and Actions of a Graphical User InterfaceAdvances in Electrical and Computer Engineering10.4316/aece.2012.0101112:1(63-70)Online publication date: 2012
https://doi.org/10.4316/aece.2012.01011
Strecker JMemon A(2009)Testing Graphical User InterfacesEncyclopedia of Information Science and Technology, Second Edition10.4018/978-1-60566-026-4.ch596(3739-3744)Online publication date: 2009
https://doi.org/10.4018/978-1-60566-026-4.ch596
Memon AQing Xie (2004)Using transient/persistent errors to develop automated test oracles for event-driven softwareProceedings. 19th International Conference on Automated Software Engineering, 2004.10.1109/ASE.2004.1342736(186-195)Online publication date: 2004
https://doi.org/10.1109/ASE.2004.1342736
Dwyer MRobby Tkachuk OVisser W(2004)Analyzing interaction orderings with model checkingProceedings. 19th International Conference on Automated Software Engineering, 2004.10.1109/ASE.2004.1342733(154-163)Online publication date: 2004
https://doi.org/10.1109/ASE.2004.1342733
White LWhite LLeung H(2002)Regression TestingEncyclopedia of Software Engineering10.1002/0471028959.sof279Online publication date: 15-Jan-2002
https://doi.org/10.1002/0471028959.sof279
White L(2002)Testing of Graphical User InterfacesEncyclopedia of Software Engineering10.1002/0471028959.sof147Online publication date: 15-Jan-2002
https://doi.org/10.1002/0471028959.sof147
Gu TSun CMa XCao CXu CYao YZhang QLu JSu ZAtlee JBultan TWhittle J(2019)Practical GUI testing of Android applications via model abstraction and refinementProceedings of the 41st International Conference on Software Engineering10.1109/ICSE.2019.00042(269-280)Online publication date: 25-May-2019
https://dl.acm.org/doi/10.1109/ICSE.2019.00042
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
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

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

Full Access

Get this Publication

Media

Figures

Other

Tables

View Issue’s Table of Contents