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.
of applications that employ the pattern. The concept is illustrated by examples from general software engineering and more specialised properties for embedded software.
| Original language | English |
|---|---|
| Title of host publication | Formal Methods and Hybrid Real-Time Systems : Essays in Honour of Dines Bjørner and Zhou Chaochen on the Occasion of Their 70th Birthdays |
| Editors | Cliff Jones, Zhiming Liu, Jim Woodcock |
| Place of Publication | Berlin /Heidelberg |
| Publisher | Springer |
| Publication date | 2007 |
| Pages | 399-413 |
| ISBN (Print) | 978-3-540-75220-2 |
| Publication status | Published - 2007 |
| Series | Lecture Notes in Computer Science |
|---|---|
| Volume | 4700 |