Abstract
Difficulty in the construction of formal specifications is one of the great gulfs that separate formal methods from industry. Though more and more practitioners become interested in formal methods as a potential technique for software quality assurance, they have also found it hard to express ideas properly in formal notations. This paper proposes a pattern-based approach to tackling this problem where a set of patterns are defined in advance. Each pattern provides an expression in informal notation to describe a type of functions and the method to transform the informal expression into a formal expression, which enables the development of a supporting tool to automatically guide one to gradually formalize the specification. We take the SOFL notation as an example to discuss the underlying principle of the approach and use an example to illustrate how it works in practice.
This work is supported in part by Okawa Foundation, Hosei University, Science and Technology Commission of Shanghai Municipality under Grant No. 10510704900 and Shanghai Leading Academic Discipline Project(Project Number: J50103). It is also supported by the NSFC Grant (No. 60910004) and 973 Program of China Grant (No. 2010CB328102).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Meyer, B.: Eiffel: The Language. Prentice Hall Object-Oriented Series (1991)
Burdy, L., Cheon, Y., Cok, D., Ernst, M., Kiniry, J., Leavens, G.T., Rustan, K., Leino, M., Poll, E.: An Overview of JML Tools and Applications. International Journal on Software Tools for Technology Transfer 7(3), 212–232 (2005)
Liu, S.: Formal Engineering for Industrial Software Development. Springer, Heidelberg (2004)
Gamma, E., Helm, R., Johnson, R.: Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley Professional (1994)
Larman, C.: Applying UML and Patterns: An Introduction to Object-Oriented Analysis and Design and Iterative Development, 3rd edn. Prentice Hall (2004)
France, R.B., Ghosh, S.: A uml-based pattern specification technique. IEEE Transactions on Software Engineering 30, 193–206 (2004)
Soundarajan, N., Hallstrom, J.O.: Responsibilities and rewards : Specifying design patterns. In: 26th International Conference on Software Engineering, pp. 666–675 (2004)
Stepney, S., Polack, F., Toyn, I.: An Outline Pattern Language for Z: Five Illustrations and Two Tables. In: Bert, D., Bowen, J.P., King, S., Walden, M. (eds.) ZB 2003. LNCS, vol. 2651, pp. 2–19. Springer, Heidelberg (2003)
Ding, J., Mo, L., He, X.: An approach for specification construction using property-preserving refinement patterns. In: 23th Annual ACM Symposium on Applied Computing, pp. 797–803. ACM, New York (2008)
Konrad, S., Cheng, B.H.C.: Real-time specification patterns. In: 27th International Conference on Software Engineering, pp. 372–381. ACM, New York (2005)
Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Pattern in property specifications for finite-state verification. In: 21th International Conference on Software Engineering, pp. 411–420. ACM, New York (1999)
Manolescu, D., Kozaczynski, W., Miller, A.: The growing divide in the patterns world. IEEE Software 24(4), 61–67 (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Wang, X., Liu, S., Miao, H. (2011). A Pattern-Based Approach to Formal Specification Construction. In: Kim, Th., et al. Software Engineering, Business Continuity, and Education. ASEA 2011. Communications in Computer and Information Science, vol 257. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-27207-3_16
Download citation
DOI: https://doi.org/10.1007/978-3-642-27207-3_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-27206-6
Online ISBN: 978-3-642-27207-3
eBook Packages: Computer ScienceComputer Science (R0)