Abstract
Refining informal ideas into appropriate formal expressions is an essential and skillful activity in writing pre-post style formal specifications. This activity usually involves decisions to be made by the writer and can be error-prone. Experience shows that this activity is also a challenge to many practitioners, and a big hurdle for introducing formal specification techniques into industry. This paper describes a pattern system approach to deal with this problem. The pattern system is composed of a set of inter-related patterns, and each pattern provides a framework for constructing certain kind of formal expression with some common properties. Unlike the way conventional design patterns are used, our pattern system is expected to support a systematic and automated formalization of informal ideas, with the characteristic that the writer only needs to work on the informal level while an appropriate formal expression will be efficiently derived. We focus on discussions of the issues such as pattern definition, pattern classification, the structure of pattern system, and mechanism to use the pattern system.
This work is supported in part by NII Collaborative Research Program. Shaoying Liu is also supported by the NSFC Grant (No. 60910004) and 973 Program of China Grant (No. 2010CB328102). This work is also supported by Science and Technology Commission of Shanghai Municipality under Grant No. 10510704900 and Shanghai Leading Academic Discipline Project(Project Number: J50103).
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Silverstein, M., Alexander, C., Ishikawa, S.: A Pattern Language: Towns, Buildings, Construction. Oxford University Press, Oxford (1977)
Miller, A., Manolescu, D., Kozaczynski, W.: The growing divide in the patterns world. IEEE Software 24(4), 61–67 (2007)
Johnson, R., Gamma, E., Helm, R.: Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley Professional, Reading (1994)
Grunske, L.: Specification Patterns For Probabilistic Quality Properties. In: Proceedings of the 30th International Conference on Software Engineering, pp. 31–40 (2008)
He, X., Ding, J., Mo, L.: 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)
Kurita, T., Nakatsugawa, Y., Ohta, Y.: Applying Formal Specification Method in the Development of an Embedded Mobile FeliCa IC Chip. In: Proceedings of the 2005 Software Symposium, Japan, pp. 73–80 (June 2005) (in Japanese)
Liu, S.: Formal Engineering for Industrial Software Development. Springer, Heidelberg (2004)
Liu, S., Takahashi, K., Hayashi, T., Nakayama, T.: Teaching Formal Methods in the Context of Software Engineering. In SIGCSE Bulletin 41(2), 17–23 (2009)
Corbett, J.C., Dwyer, M.B., Avrunin, G.S.: Pattern in property specifications for finite-state verification. In: 21th International Conference on Software Engineering, pp. 411–420. ACM, New York (1999)
Parnas, D.L.: Really Rethinking Formal Methods. Computer 43(1), 28–34 (2010)
Sahara, S.: An Experience of Applying Formal Method on a Large Business Application. In: Proceedings of 2004 Symposium of Science and Technology on System Verification, Osaka, Japan, February 4-6, pp. 93–100. National Institute of Advanced Industrial Science and Technology (AIST) (2004) (in Japanese)
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. (eds.) ZB 2003. LNCS, vol. 2651, pp. 2–19. Springer, Heidelberg (2003)
The VDM-SL Tool Group: Users Manual for the IFAD VDM-SL tools. Technical Report IFAD-VDM-4, The Institute of Applied Computer Science (IFAD) (December 1994)
Woodcock, J., Larsen, P.G., Bicarregui, J., Fitzgerald, J.: Formal Methods: Practice and Experience. ACM Computing Surveys 41(4) (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Wang, X., Liu, S., Miao, H. (2010). A Pattern System to Support Refining Informal Ideas into Formal Expressions. In: Dong, J.S., Zhu, H. (eds) Formal Methods and Software Engineering. ICFEM 2010. Lecture Notes in Computer Science, vol 6447. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16901-4_43
Download citation
DOI: https://doi.org/10.1007/978-3-642-16901-4_43
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-16900-7
Online ISBN: 978-3-642-16901-4
eBook Packages: Computer ScienceComputer Science (R0)