research-article

Applying Formal Software Synthesis

Author:

Richard K. JülligAuthors Info & Claims

IEEE Software, Volume 10, Issue 3

Pages 11 - 22

https://doi.org/10.1109/52.210596

Published: 01 May 1993 Publication History

Publisher Site

Abstract

A software synthesis method that combines elements of graphical tools, specification writing, and code construction is discussed. Practical applications of the components and efforts to integrate them into a conceptually coherent prototype environment are described. The hallmarks of the approach are the use of formal methods and a general-purpose inference engine, supported by a comprehensive, interactive development environment. The development model is a formal method, but it differs from other formal approaches in that its notations are used primarily to represent programming knowledge and support automated code generation. The performance of the system is also described.

References

[1]

1. D.R. Smith, "Structure and Design of Global Search Algorithms," Tech. Report KES.U.87.12, Kestrel Institute, Palo Alto, Calif., 1987.

Google Scholar

[2]

1. D.R. Smith, "Constructing Specification Morphisms," Tech. Report KES.U.92.1, Kestrel Institute, Palo Alto, Calif., 1992.

Google Scholar

[3]

2. L-M. Gilham, A. Goldberg, and T.C. Wang, "Toward Reliable Reactive Systems," Proc. Int'l Workshop Software Specification and Design, IEEE CS Press, Los Alamitos, Calif., 1989, pp. 68-74.

Crossref

Google Scholar

[4]

3. T.C. Wang and A. Goldberg, "A Mechanical Verifier for Supporting the Design of Reliable Reactive Systems," Proc. Int'l Symp. Software Reliability Engineering, IEEE CS Press, Los Alamitos, Calif., 1991, pp. 131-138.

Google Scholar

[5]

4. D.R. Smith, "Kids--A Semi-Automatic Program Development System," IEEE Trans. Software Eng., Sept. 1990, pp. 1024- 1043.

Digital Library

Google Scholar

[6]

5. L. Blaine and A. Goldberg, "Dtre--A Semi-Automatic Transformation System," Constructing Programs from Specifications, B. Moller, ed., North-Holland, Amsterdam, 1991, pp. 165-204.

Google Scholar

[7]

6. D.R. Smith, "Track Assignment in an Air Traffic Control System: A Rational Reconstruction of System Design," Proc. Knowledge-Based Software Eng. Conf., IEEE CS Press, Los Alamitos, Calif., 1992, pp. 60-68.

Digital Library

Google Scholar

[8]

7. S. Westfold, C. Green, and D. Zimmerman, "Automated Design of Displays for Technical Data," tech. report, Kestrel Institute, Palo Alto, Calif., 1990.

Google Scholar

[9]

8. J. Fiadeiro and T. Maibaum, "Temporal Theories as Modularisation Units for Concurrent System Specification," tech. report, Imperial College, London, 1991.

Google Scholar

Cited By

View all

Hemer DLindsay P(1996)The CARE toolset for developing verified programs from formal specificationsProceedings of the Proceedings of the Fourth International Symposium on Assessment of Software Tools (SAST '96)10.5555/546972.829427Online publication date: 22-May-1996
https://dl.acm.org/doi/10.5555/546972.829427

Recommendations

SPARE: A Development Environment for Program Analysis Algorithms

A tool that bridges the gap between the theory and practice of program analysis specifications is described. The tool supports a high-level specification language that enables clear and concise expression of analysis algorithms. The denotational nature ...
Automatic Derivation of Formal Software Specifications from Informal Descriptions

SPECIFIER, an interactive system which derives formal specifications of data types and programs from their informal descriptions, is described. The process of deriving formal specifications is viewed as a problem-solving process. The system uses common ...
From a formal dynamic semantics of Sisal to a Sisal environment
HICSS '95: Proceedings of the 28th Hawaii International Conference on System Sciences

We present a formal definition of the dynamic semantics of a significant part of the language Sisal 2.0 in the structural operational style of Natural Semantics, namely Typoi inference rules, within the Centaur system, a generic specification ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

IEEE Software Volume 10, Issue 3

May 1993

98 pages

ISSN:0740-7459

Issue’s Table of Contents

Publisher

IEEE Computer Society Press

Washington, DC, United States

Publication History

Published: 01 May 1993

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

1
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 02 Oct 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Hemer DLindsay P(1996)The CARE toolset for developing verified programs from formal specificationsProceedings of the Proceedings of the Fourth International Symposium on Assessment of Software Tools (SAST '96)10.5555/546972.829427Online publication date: 22-May-1996
https://dl.acm.org/doi/10.5555/546972.829427

Abstract

References

Cited By

Recommendations

SPARE: A Development Environment for Program Analysis Algorithms

Automatic Derivation of Formal Software Specifications from Informal Descriptions

From a formal dynamic semantics of Sisal to a Sisal environment

Comments

Information

Published In

Publisher

Publication History

Author Tags

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations