Article

Formal specification comprehension: the art of reading and writing z

Authors:

Andreas Bollin,

Dominik Rauner-ReithmayerAuthors Info & Claims

FormaliSE 2014: Proceedings of the 2nd FME Workshop on Formal Methods in Software Engineering

Pages 3 - 9

https://doi.org/10.1145/2593489.2593491

Published: 03 June 2014 Publication History

Abstract

Formal Methods have been developed to provide systematic and rigorous techniques for software development. They found their place in document-driven development processes as well as in the agile world. However, reading, understanding and working with a formal specification still turns out to be a real challenge.

This paper tries to identify the underlying cause and argues that comprehensibility of a specification is one of the key factors. It presents some first findings of an extensive study investigating the readability of Z specifications and comes up with a set of recommendations in writing formal specifications so that the syntactic gap between the mathematics and the natural language requirements description can be bridged more easily.

References

[1]

R. Barden, S. Stepney, and D. Cooper. Z in Practice. Prentice-Hall, Inc., NJ, USA, 1995.

Digital Library

[2]

A. Bollin. Concept Location in Formal Specifications. Journal of Software Maintenance and Evolution – Research and Practice, 20(2):77–105, 2008.

Digital Library

[3]

A. Bollin. Is there evolution before birth? Deterioration effects of formal Z specifications. In Proceedings of the 13th international conference on Formal methods and software engineering, ICFEM’11, pages 66–81, Berlin, Heidelberg, 2011. Springer-Verlag.

Digital Library

[4]

A. Bollin. Do You Speak Z? Formal Methods under the Perspective of a Cross-Cultural Adaptation Problem. In S. Gnesi and N. Plat, editors, 1st FME Workshop on Formal Methods in Software Engineering (FormaliSE), pages 8–14. IEEE, 2013.

[5]

A. Bollin. ViZ – Visualize, Measure, and Comprehend. http://viz.uni-klu.ac.at, Page last visited: Jan. 2014.

[6]

A. Diller. Z - An Introduction to Formal Methods. John Wiley and Sons, 1999.

Digital Library

[7]

N. E. Fenton and S. L. Pfleeger. Software Metrics: A Rigorous and Practical Approach. PWS Publishing Co., Boston, MA, USA, 2nd edition, 1998.

Digital Library

[8]

K. Finney, K. Rennolls, and A. Fedorec. Measuring the comprehensibility of z specifications. J. Syst. Softw., 42(1):3–15, July 1998.

Digital Library

[9]

A. M. Gravell. What is a Good Formal Specification? In Proceedings of the Fifth Annual Z User Meeting on Z User Workshop, pages 137–150, London, UK, 1991. Springer-Verlag.

Digital Library

[10]

D. Jackson. Software Abstractions - Logic, Language, and Analysis. The MIT Press, Cambridge, Massachusetts, 2006.

Digital Library

[11]

C. B. Jones, D. Jackson, and J. Wing. Formal Methods Light. Computer, 29(4):20–22, Apr. 1996.

Digital Library

[12]

P. G. Larsen, N. Battle, M. Ferreira, J. Fitzgerald, K. Lausdahl, and M. Verhoef. The overture initiative integrating tools for vdm. SIGSOFT Softw. Eng. Notes, 35(1):1–6, Jan. 2010.

Digital Library

[13]

P. G. Larsen, J. Fitzgerald, and S. Riddle. Learning by doing: Practical courses in lightweight formal methods using vdm+. Cs-tr-992, University of Newcastle upon Tyne, 2006.

[14]

J. Spivey. The Z Notation. C.A.R. Hoare Series. Prentice Hall, 1989.

Digital Library

[15]

J. A. van der Poll and P. Kotzé. What Design Heuristics May Enhance the Utility of a Formal Specification? In Proceedings of the 2002 Annual Research Conference of the South African Institute of Computer Scientists and Information Technologists on Enablement Through Technology, SAICSIT ’02, pages 179–194, 2002.

Digital Library

[16]

R. Vinter, M. Loomes, and D. Kornbrot. Applying Software Metrics to Formal Specifications: A Cognitive Approach. In 5th International Symposium on Software Metrics, pages 216–223, Bethesda, Maryland, 1998. IEEE Computer Society.

Digital Library

Cited By

Siu HLeahy KMann M(2023)STL: Surprisingly Tricky Logic (for System Validation)2023 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS)10.1109/IROS55552.2023.10342290(8613-8620)Online publication date: 1-Oct-2023
https://doi.org/10.1109/IROS55552.2023.10342290
Ratiu DGario MSchoenhaar HGnesi SPlat NDay NRossi M(2019)FASTEN: an open extensible framework to experiment with formal specification approachesProceedings of the 7th International Workshop on Formal Methods in Software Engineering10.1109/FormaliSE.2019.00013(41-50)Online publication date: 27-May-2019
https://dl.acm.org/doi/10.1109/FormaliSE.2019.00013
Goubali OGirard PGuittet LBignon AKesraoui DBoulhic LBerruet PBouillon J(2016)Evaluation of tool support for functional specification of complex systemsProceedings of the 15th Ergo'IA "Ergonomie Et Informatique Avancée" Conference10.1145/3050385.3050402(1-8)Online publication date: 6-Jul-2016
https://dl.acm.org/doi/10.1145/3050385.3050402
Show More Cited By

Index Terms

Recommendations

Formal Specification of User Interfaces: A Comparison and Evaluation of Four Axiomatic Approaches
Annals of discrete mathematics, 24

Few examples of formal specification of the semantics of user interfaces exist in the literature. This paper presents a comparison of four axiomatic approaches which we have applied to the specification of a commercial user interface-the line editor for ...
An overview of CAFE specification environment-an algebraic approach for creating, verifying, and maintaining formal specifications over networks
ICFEM '97: Proceedings of the 1st International Conference on Formal Engineering Methods

CAFE is the name of a network based environment now under development for supporting systematic creation, checking, verification, and maintenance of formal specifications. CAFE has an algebraic specification language called CafeOBJ as its main ...
Structured programming and formal specification

In the author's view structured programming consists of the use of the following: structure, abstraction, and specification. The purpose of this paper is to develop formal specifications fora nontrivial program in order to facilitate a proof of ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

FormaliSE 2014: Proceedings of the 2nd FME Workshop on Formal Methods in Software Engineering

June 2014

58 pages

ISBN:9781450328531

DOI:10.1145/2593489

Program Chairs:
Stefania Gnesi,
Nico Plat

Copyright © 2014 ACM.

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]

Sponsors

SIGSOFT: ACM Special Interest Group on Software Engineering

In-Cooperation

TCSE: IEEE Computer Society's Tech. Council on Software Engin.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 03 June 2014

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

ICSE '14

Sponsor:

SIGSOFT

ICSE '14: 36th International Conference on Software Engineering

June 3, 2014

Hyderabad, India

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

5
Total Citations
View Citations
226
Total Downloads

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

Reflects downloads up to 17 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Siu HLeahy KMann M(2023)STL: Surprisingly Tricky Logic (for System Validation)2023 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS)10.1109/IROS55552.2023.10342290(8613-8620)Online publication date: 1-Oct-2023
https://doi.org/10.1109/IROS55552.2023.10342290
Ratiu DGario MSchoenhaar HGnesi SPlat NDay NRossi M(2019)FASTEN: an open extensible framework to experiment with formal specification approachesProceedings of the 7th International Workshop on Formal Methods in Software Engineering10.1109/FormaliSE.2019.00013(41-50)Online publication date: 27-May-2019
https://dl.acm.org/doi/10.1109/FormaliSE.2019.00013
Goubali OGirard PGuittet LBignon AKesraoui DBoulhic LBerruet PBouillon J(2016)Evaluation of tool support for functional specification of complex systemsProceedings of the 15th Ergo'IA "Ergonomie Et Informatique Avancée" Conference10.1145/3050385.3050402(1-8)Online publication date: 6-Jul-2016
https://dl.acm.org/doi/10.1145/3050385.3050402
Goubali OGirard PGuittet LBignon AKesraoui DBerruet PBouillon J(2016)Designing Functional Specifications for Complex SystemsProceedings, Part I, of the 18th International Conference on Human-Computer Interaction. Theory, Design, Development and Practice - Volume 973110.1007/978-3-319-39510-4_16(166-177)Online publication date: 17-Jul-2016
https://dl.acm.org/doi/10.1007/978-3-319-39510-4_16
Huynh KBui TQuan T(2015)Instance-based web services composition and verification2015 International Conference on Communications, Management and Telecommunications (ComManTel)10.1109/ComManTel.2015.7394296(245-249)Online publication date: Dec-2015
https://doi.org/10.1109/ComManTel.2015.7394296

View Options

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

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents