Design Verifikation Patterns

Research output: ResearchBook chapter

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.
Close

Details

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.
Original languageEnglish
Title of host publicationFormal Methods and Hybrid Real-Time Systems : Essays in Honour of Dines Bjørner and Zhou Chaochen on the Occasion of Their 70th Birthdays
EditorsCliff Jones, Zhiming Liu, Jim Woodcock
Place of PublicationBerlin /Heidelberg
PublisherSpringer
Publication date2007
Pages399-413
ISBN (Print)978-3-540-75220-2
StatePublished - 2007
Publication categoryResearch
Peer-reviewedNo
SeriesLecture Notes in Computer Science
Volume4700
ID: 13211483