Skip to main content
SpringerLink
Log in

Formal Specification and Verification

  • Chapter
Software Engineering and Environment

Part of the book series: Software Science and Engineering ((SSEN))

  • 90 Accesses

Abstract

Once requirements are fully understood, it is important to have them documented and verified. This stage is critical, since no one wants to waste hundreds of employee hours developing a software package that does not function as expected. Requirements specification can be done in terms of the logical components involved, their respective inputs, outputs and desired relationships, and constraint to be imposed. States and possible state transitions can also be incorporated into a requirements specification; in this case the requirements specification may be executable. Indeed some requirements specification languages are executable (e.g., Petri net; see Section 3.6).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Alford, M. IEEE Computer 18:4, 36–46 (Apr. 1985).

    Article  Google Scholar 

  2. Shoenfield, J. R. Mathematical logic (Addison-Wesley, Reading, MA, 1967).

    MATH  Google Scholar 

  3. Genesereth, M. R., and Nilsson, N. J. Logical foundations of artificial intelligence (Morgan-Kaufmann, Palo Alto, CA, 1988).

    Google Scholar 

  4. Nilsson, N. J. Principles of artificial intelligence (Morgan Kaufmann, Palo Alto, CA, 1980).

    MATH  Google Scholar 

  5. Ullman, J. D. Principles of database systems, 2d ed. (Computer Science Press, Potomac, MD, 1982).

    MATH  Google Scholar 

  6. Gallaire, H., Minker, J., and Nicolas, J. M. ACM Computing Surveys 16, 153–185 (June 1984).

    Article  MathSciNet  MATH  Google Scholar 

  7. Spivey, J. M. Z notation: a reference manual (Prentice-Hall, New York, 1988).

    Google Scholar 

  8. Imperato, M. An introduction to Z (Chartwell-Bratt, Bromley, Kent, U.K., 1991).

    Google Scholar 

  9. Sheu, P. C-Y., and Yoo, S. B. “A deductive approach to software reuse.” Proc. of 1994 International Conference on Software Engineering and Knowledge Engineering (Latvia, June, 1994).

    Google Scholar 

  10. Chang, C. L., and Lee, R. C. T. Symbolic logic and mechanical theorem proving (Academic Press, New York, 1973).

    MATH  Google Scholar 

  11. Horebeek, I. V., and Lewi, J. Algebraic specifications in software engineering, an introduction (Springer-Verlag, New York, 1989).

    Book  Google Scholar 

  12. Reichel, H. Initial computability algebraic specifications and partial algebras (Oxford Science Publications, New York, 1987).

    MATH  Google Scholar 

  13. IEEE Transactions on Software Engineering, Special Issue on Algebraic Specifications SE-11:3, 242–251 (Mar. 1985).

    Google Scholar 

  14. Ehrig, H., and Mahr, B. Fundamentals of algebraic specification 1: equations and initial semantics (Springer-Verlag, New York, 1985)

    Book  MATH  Google Scholar 

  15. Guttag, J. V., Horning, J. J., and Wing, J. M. IEEE Software 2:5, 24–36 (Sept. 1985).

    Article  Google Scholar 

  16. Peterson, J. L. Net theory and the modeling of systems (Prentice-Hall, New York, 1981).

    Google Scholar 

  17. Peterson, J. L. ACM Computing Surveys 9:3, 223–252 (Sept. 1977).

    Article  MATH  Google Scholar 

  18. Ramamoorthy, C. V., and Ho, G. IEEE Transactions on Software Engineering SE-6:5, 440–449 (Sept. 1980).

    Article  MathSciNet  Google Scholar 

  19. Reisig, W. Theoretical Computer Science 80, 1–34 (1991).

    Article  MathSciNet  MATH  Google Scholar 

  20. Hoare, C. A. R. IEEE Computer 20:9, 85–91 (Sept. 1987).

    Article  MathSciNet  Google Scholar 

  21. Owicki, S., and Lamport, L. ACM Transactions on Programming Languages and Systems 4:3, 455–495 (July 1982).

    Article  MATH  Google Scholar 

  22. Lamport, L., and Schneider, F. B. ACM Transactions on Programming Languages and Systems 6:2, 281–296 (Apr. 1984).

    Article  MATH  Google Scholar 

  23. Liu, L. Y., and Shyamasundar, R. K. IEEE Transactions on Software Engineering SE-16:3, 373–388 (Apr. 1990).

    Article  Google Scholar 

  24. Karp, R. M., and Miller, R. E. SI AM Journal of Applied Math. 14 (Nov. 1966).

    Google Scholar 

  25. Hack, M. Decidability questions for Petri nets (Ph.D. diss., MIT, 1975).

    Google Scholar 

  26. Gostelow, K. P., Flow of control, resource allocation, and the proper termination of programs (Ph.D. diss., University of California, Los Angeles, 1971).

    Google Scholar 

  27. Leveson, N. G. IEEE Transactions on Software Engineering SE-13:3, 386–397 (Mar. 1987).

    Article  Google Scholar 

  28. Leveson, N. G. Communication ACM 34:2, 36–46 (Feb. 1991).

    Article  Google Scholar 

  29. Coolahan, J. E., and Roussopoulos, N. IEEE Transactions on Software Engineering SE-9.9, 603 (Sept. 1983).

    Article  Google Scholar 

  30. Davis, R., and King, J. In Machine intelligence, vol. 8 ( Elcock and Michie, eds.) (Wiley, New York, 1976), pp. 279–90.

    Google Scholar 

  31. Hall, A. IEEE Software 7:9, 11–20 (Sept. 1990).

    Article  Google Scholar 

  32. Wing, J. M. IEEE Computer 23:9, 8–24 (Sept. 1990).

    Article  Google Scholar 

  33. Jones, C. B. Systematic software development using VDM (Prentice-Hall, New York, 1986).

    MATH  Google Scholar 

  34. Lamport, L. ACM Transactions on Programming Languages and Systems 5:2, 190–222 (Apr. 1983).

    Article  MATH  Google Scholar 

  35. Hoare, C. A. R. Communication ACM 21:8, 666 (Aug. 1978).

    Article  MathSciNet  MATH  Google Scholar 

  36. Zave, P., and Schell, W. IEEE Transactions on Software Engineering SE-12:2, 312–325 (Feb. 1986).

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of California, Irvine, Irvine, California, USA

    Phillip C.-Y. Sheu

Authors
  1. Phillip C.-Y. Sheu
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

Copyright information

© 1997 Springer Science+Business Media New York

About this chapter

Cite this chapter

Sheu, P.CY. (1997). Formal Specification and Verification. In: Software Engineering and Environment. Software Science and Engineering. Springer, Boston, MA. https://doi.org/10.1007/978-1-4615-5907-8_3

Download citation

  • DOI: https://doi.org/10.1007/978-1-4615-5907-8_3

  • Publisher Name: Springer, Boston, MA

  • Print ISBN: 978-1-4613-7710-8

  • Online ISBN: 978-1-4615-5907-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation