Abstract
Symbolic model checking techniques have been widely and successfully applied to statically analyze dynamic properties of hardware systems. Efforts to apply this same technology to the analysis of software systems has met with a number of obstacles, such as the existence of non-finite state-spaces. This paper investigates abstractions that make it possible to cost-effectively model check specifications of software for graphical user interface (GUI) systems. We identify useful abstractions for this domain and demonstrate that they can be incorporated into the analysis of a variety of systems with similar structural characteristics. The resulting domain-specific model checking yields fast verification of naturally occur ring specifications of intended GUI behavior.
Supported in part by NSF and DARPA under grant CCR-9633388.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
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.
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.
E. Clarke, O. Grumberg, and D. Long. Model checking and abstraction. ACM Transactions on Programming Languages and Systems, 16(5):1512–1542, Sept. 1994.
R. Cleaveland, J. Parrow, and B. Steffen. The concurrency workbench: A semantics based tool for the verification of concurrent systems. ACM Transactions on Programming Languages and Systems, 15(1):36–72, Jan. 1993.
J. Corbett. Evaluating deadlock detection methods for concurrent software. IEEE Transactions on Software Engineering, 22(3), Mar. 1996. 15.
D. Dams. Abstract Interpretation and Partition Refinement for Model Checking. PhD thesis, Eindhoven University of Technology, May 1996.
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.
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.
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.
R. Jacob. Using formal specifications in the design of a human-computer interface. Communications of the ACM, 26(4):259–264, Apr. 1983.
Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, 1991.
K. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.
B. Myers. User interface software tools. ACM Transactions on ComputerHuman Interaction, 2(1):64–103, Mar. 1995.
K. Olender and L. Osterweil. Cecil: A sequencing constraint language for automatic static analysis generation. IEEE Transactions on Software Engineering, 16(3):268–280, Mar. 1990.
A. Wasserman. Extending state transition diagrams for the specification of human-computer interaction. IEEE Transactions on Software Engineering, SE-11(8):699–713, Aug. 1985.
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.
M. Young, R. Taylor, D. Levine, K. Nies, and D. Brodbeck. A concurrency analysis tool suite: Rationale, design, and preliminary experience. ACM Transactions on Software Engineering and Methodology, 4(1):64–106, Jan. 1995.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dwyer, M.B., Carr, V., Hines, L. (1997). Model checking graphical user interfaces using abstractions. In: Jazayeri, M., Schauer, H. (eds) Software Engineering — ESEC/FSE'97. ESEC SIGSOFT FSE 1997 1997. Lecture Notes in Computer Science, vol 1301. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63531-9_18
Download citation
DOI: https://doi.org/10.1007/3-540-63531-9_18
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63531-4
Online ISBN: 978-3-540-69592-9
eBook Packages: Springer Book Archive