Abstract
Design Verification Patterns are formal specifications that define the semantics of design patterns. For each design pattern, the corresponding verification pattern give a set of proof obligations. They must be discharged for a correct implementation of the pattern. Additionally there is a set of properties that may be used in the design and verification of applications that employ the pattern. The concept is illustrated by examples from general software engineering and more specialised properties for embedded software.
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
Bass, L., Clements, P., Kazman, R.: Software Architecture in Practice. Addison-Wesley, Reading (1999)
Bjørner, D.: Software Engineering. In: Domains, Requirements and Software Design. Texts in Theoretical Computer Science, vol. 3, Springer, Heidelberg (2006)
Chalin, P., Kiniry, J.R., Leavens, G.T., Poll, E.: Beyond assertions: Advanced specification and verification with JML and ESC/Java2. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 342–363. Springer, Heidelberg (2006)
Damm, W., Hungar, H., Olderog, E.-R.: On the verification of cooperating traffic agents. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2003. LNCS, vol. 3188, pp. 77–110. Springer, Heidelberg (2004)
Damm, W., Hungar, H., Olderog, E.-R.: Verification of cooperating travel agents. International Journal of Control 79(5), 395–421 (2006)
Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns. Addison-Wesley, Reading (1995)
Object Management Group. Unified Modeling Language: Superstructure, version 2.0, final adopted specification (2005), http://www.omg.org/uml/,formal/05-07-04
He, J., Hoare, C.A.R., Fränzle, M., Müller-Olm, M., Olderog, E.-R., Schenke, M., Hansen, M.R., Ravn, A.P., Rischel, H.: Provably correct systems. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) Formal Techniques in Real-Time and Fault-Tolerant Systems. LNCS, vol. 863, pp. 288–335. Springer, Heidelberg (1994)
He, J., Li, X., Liu, Z.: rCOS: A refinement calculus for object systems. Theoretical Computer Science 365(1-2), 109–142 (2006)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)
Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice-Hall, Englewood Cliffs (1998)
Hoenicke, J., Olderog, E.-R.: Combining Specification Techniques for Processes Data and Time. In: Butler, M., Petre, L., Sere, K. (eds.) IFM 2002. LNCS, vol. 2335, pp. 245–266. Springer, Heidelberg (2002)
Hoenicke, J.: Combination of Processes, Data, and Time. PhD thesis, Fachbereich Informatik Universitt Oldenburg (2006)
Langmaack, H., Ravn, A.P.: The procos project: Provably correct systems. In: Bowen, J. (ed.) Towards Verified Systems. Real-Time Safety Critical Systems, ch. Appendix B. vol. 2, Elsevier, Amsterdam (1994)
Larman, C.: Applying UML and Patterns: An Introduction to Object-Oriented Analysis and Design and the Unified Process, 2nd edn. Prentice-Hall, Englewood Cliffs (2001)
Liu, Z., He, J., Li, X.: rCOS: A relational calculus of components. In: Mathematical Frameworks for Component Software, pp. 207–238. World Scientific, Singapore (2006)
Liu, Z., Mencl, V., Ravn, A.P., Yang, L.: Harnessing theories for tool support. In: Proceedings of International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2006) (November 2006) (An extended version is found as UNU-IIST Technical Report 335, August 2006)
Long, Q., Qiu, Z., Liu, Z., Shao, L., He, J.: POST: a case study for an incremental development in rCOS. In: Van Hung, D., Wirsing, M. (eds.) ICTAC 2005. LNCS, vol. 3722, pp. 485–500. Springer, Heidelberg (2005)
Meyer, B.: Object-oriented software construction, 2nd edn. Prentice-Hall, Englewood Cliffs (1997)
Meyer, R., Faber, J., Rybalchenko, A.: Model checking duration calculus: A practical approach. In: Barkaoui, K., Cavalcanti, A., Cerone, A. (eds.) ICTAC 2006. LNCS, vol. 4281, pp. 332–346. Springer, Heidelberg (2006)
Möller, M., Olderog, E.-R., Rasch, H., Wehrheim, H.: Linking CSP-OZ with UML and Java: A case study. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol. 2999, Springer, Heidelberg (2004)
Moszkowski, B.: A temporal logic for multilevel reasoning about hardware. Computer 18(2), 10–19 (1985)
Olderog, E.-R., Ravn, A.P., Skakkebæk, J.U.: Refining system requirements to program specifications (chapter 5). In: Heitmeyer, C., Mandrioli, D. (eds.) Formal Methods in Real-Time Systems. Trends in Software-Engineering, pp. 107–134. Wiley, Chichester (1996)
Rischel, H., Cuellar, J., Mørk, S., Ravn, A.P., Wildgruber, I.: Development of safety-critical real-time systems. In: Bartosek, M., Staudek, J., Wiedermann, J. (eds.) SOFSEM 1995. LNCS, vol. 1012, pp. 206–235. Springer, Heidelberg (1995)
Rumbaugh, J., Jacobson, I., Booch, G.: The Unified Modelling Language Reference Manual. Addison-Wesley, Reading (1999)
Smith, G.: The Object-Z specification language. Kluwer Academic Publishers, Norwell, MA, USA (2000)
Soundarajan, N., Hallstrom, J.O.: Responsibilities and rewards: specifying design patterns. In: Proceedings 26th International Conference on Software Engineering, ICSE 2004, May 2004, pp. 666–675. IEEE Computer Society Press, Los Alamitos (2004)
Szyperski, C.: Component Software: Beyond Object-Oriented Programming. Addison-Wesley, Reading (1997)
Zhou, C., Hansen, M.R., Ravn, A.P., Rischel, H.: Duration specifications for shared processors. In: Vytopil, J. (ed.) Formal Techniques in Real-Time and Fault-Tolerant Systems. LNCS, vol. 571, pp. 21–32. Springer, Heidelberg (1991)
Zhou, C., Hansen, M.R.: Duration Calculus: A Formal Approach to Real-Time Systems. In: Monographs in Theoretical Computer Science. An EATCS Series, Springer, Heidelberg (2004)
Zhou, C.C., Hoare, C.A.R., Ravn, A.P.: A calculus of durations. Information Processing Letters 40(5), 269–276 (1991)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Knudsen, J., Ravn, A.P., Skou, A. (2007). Design Verification Patterns. In: Jones, C.B., Liu, Z., Woodcock, J. (eds) Formal Methods and Hybrid Real-Time Systems. Lecture Notes in Computer Science, vol 4700. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-75221-9_18
Download citation
DOI: https://doi.org/10.1007/978-3-540-75221-9_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-75220-2
Online ISBN: 978-3-540-75221-9
eBook Packages: Computer ScienceComputer Science (R0)