short-paper

Using State Machines for the Visualisation of Specifications via Refinement

Authors:

Colin Pilbrow,

Steve ReevesAuthors Info & Claims

ASWEC ' 15 Vol. II: Proceedings of the ASWEC 2015 24th Australasian Software Engineering Conference

Pages 106 - 110

https://doi.org/10.1145/2811681.2811702

Published: 28 September 2015 Publication History

Get Access

Abstract

We talk in this paper about using state machines and refinement to characterise the visualisation of a computation.

We use Z specifications to give examples of systems in the usual way, and then use Z schemas to also represent states and transitions in state machines, which we consider to be a particular kind of visualisation of a specified system.

We have investigated the principle of substitutivity and the idea of downward simulation to check whether or not a refinement relation exists between the specification and the state machine. We are looking at this because we believe that the soundness of the visualisation can be captured by such a refinement relationship.

References

[1]

A. Akingbade, T. Finley, D. Jackson, P. Patel, and S. H. Rodger. Jawaa: Easy web-based animation from cs 0 to advanced cs courses. In In Proceedings of the 34 th ACM SIGCSE Technical Symposium on Computer Science Education (SIGCSE 2003, pages 162--166. ACM Press, 2003.

Digital Library

Google Scholar

[2]

D. Goldson. A symbolic calculator for non-strict functional programs. The Computer Journal, 37(3):177--187, 1994.

Crossref

Google Scholar

[3]

M. C. Henson and S. Reeves. Investigating Z. Journal of Logic and Computation, 10(1):1--30, 2000.

Crossref

Google Scholar

[4]

J. A. Jones, M. J. Harrold, and J. Stasko. Visualization of test information to assist fault localization. In In Proceedings of the 24th International Conference on Software Engineering, pages 467--477, 2002.

Digital Library

Google Scholar

[5]

C. Morgan. Programming From Specifications (2nd ed.). Prentice Hall International (UK) Ltd., Hertfordshire, UK, UK, 1998.

Digital Library

Google Scholar

[6]

ProB Project. http://stups.hhu.de/prob/.

Google Scholar

[7]

S. Reeves, D. Goldson, P. Fung, T. O'Shea, M. Hopkins, and R. Bornat. The Calculator Project-formal reasoning about programs. In M. Purvis, editor, Proceedings of Software Education Conference (SRIG-ET'94), pages 166--173. IEEE Computer Society Press, 1995.

Crossref

Google Scholar

[8]

J. Spivey. An Introduction to Z and Formal Specification. IEE Software Engineering Journal, 4(1):40--50, 1989.

Digital Library

Google Scholar

[9]

J. M. Spivey. Understanding Z: A Specification Language and its Formal Semantics, volume 3 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1988.

Digital Library

Google Scholar

[10]

N. Wirth. Program development by stepwise refinement. Communications of the ACM, 14(4):221--227, April 1971.

Digital Library

Google Scholar

[11]

J. Woodcock and J. Davies. Using Z: Specification, Refinement and Proof. Prentice Hall, 1996.

Digital Library

Google Scholar

Cited By

View all

Pilbrow CReeves S(2017)Characterising Sound Visualisations of Specifications Using Micro-Charts and Refinement2017 24th Asia-Pacific Software Engineering Conference Workshops (APSECW)10.1109/APSECW.2017.16(5-8)Online publication date: Dec-2017
https://doi.org/10.1109/APSECW.2017.16
Pilbrow CReeves S(2017)Characterising Sound Visualisations of Specifications Using Micro-Charts and Refinement2017 24th Asia-Pacific Software Engineering Conference (APSEC)10.1109/APSEC.2017.74(612-617)Online publication date: Dec-2017
https://doi.org/10.1109/APSEC.2017.74

Recommendations

Generating finite state machines from abstract state machines
ISSTA '02: Proceedings of the 2002 ACM SIGSOFT international symposium on Software testing and analysis

We give an algorithm that derives a finite state machine (FSM) from a given abstract state machine (ASM) specification. This allows us to integrate ASM specs with the existing tools for test case generation from FSMs. ASM specs are executable but have ...
Generating finite state machines from abstract state machines

We give an algorithm that derives a finite state machine (FSM) from a given abstract state machine (ASM) specification. This allows us to integrate ASM specs with the existing tools for test case generation from FSMs. ASM specs are executable but have ...
Analyzing tabular requirements specifications using infinite state model checking
MEMOCODE '06: Proceedings of the Fourth ACM/IEEE International Conference on Formal Methods and Models for Co-Design

This paper investigates the application of infinite state model checking to the formal analysis of requirements specifications in the SCR (software cost reduction) tabular notation using action language verifier (ALV). After reviewing the SCR method and ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

ASWEC ' 15 Vol. II: Proceedings of the ASWEC 2015 24th Australasian Software Engineering Conference

September 2015

171 pages

ISBN:9781450337960

DOI:10.1145/2811681

Editors:
Fei-Ching (Diana) Kuo
Swinburne University of Technology, Australia
,
Stuart Marshall
Victoria University of Wellington, New Zealand
,
Haifeng Shen
Flinders University, Australia
,
Markus Stumptner
University of South Australia, Australia
,
M. Ali Babar
University of Adelaide, Australia

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 the author(s) 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].

In-Cooperation

Australian Comp Soc: Australian Computer Society

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 28 September 2015

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Short-paper
Research
Refereed limited

Conference

ASWEC ' 15 Vol. II

ASWEC ' 15 Vol. II: ASWEC 2015 24th Australasian Software Engineering Conference

September 28 - October 1, 2015

SA, Adelaide, Australia

Acceptance Rates

ASWEC ' 15 Vol. II Paper Acceptance Rate 12 of 27 submissions, 44%;

Overall Acceptance Rate 12 of 27 submissions, 44%

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
42
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 16 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Pilbrow CReeves S(2017)Characterising Sound Visualisations of Specifications Using Micro-Charts and Refinement2017 24th Asia-Pacific Software Engineering Conference Workshops (APSECW)10.1109/APSECW.2017.16(5-8)Online publication date: Dec-2017
https://doi.org/10.1109/APSECW.2017.16
Pilbrow CReeves S(2017)Characterising Sound Visualisations of Specifications Using Micro-Charts and Refinement2017 24th Asia-Pacific Software Engineering Conference (APSEC)10.1109/APSEC.2017.74(612-617)Online publication date: Dec-2017
https://doi.org/10.1109/APSEC.2017.74

View Options

Login options

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

Cited By

Recommendations

Generating finite state machines from abstract state machines

Generating finite state machines from abstract state machines

Analyzing tabular requirements specifications using infinite state model checking