Formal Methods And Patterns

Although nobody has so far showed how to formalize "design patterns", many of the design motifs that patterns contain can be formalized as demonstrated here for the "gang of four" patterns:

Tools can be used used to specify patterns and to verify that an implementation conforms with the specification: --AmnonEden

I think there are 3 ways in which there could be a fruitful interaction between ideas about patterns and about formal or rigorous techniques (compare FormalMethods).

-- AlanWills. I undertake to modify the above when and as persuaded by any ensuing debate.

If you understand WhyPatternsAreDifferent, you might worry that any attempt to formalize patterns lets people conveniently dodge the integrative, generative, and human aspects of patterns that contribute to the QualityWithoutAName. That is, formal methods try to give a name to the QualityWithoutAName, 'nuf said...

I'll advocate the formalization of patterns when society believes it is a good idea to formalize poetry beyond its form. -- JimCoplien

A rocket ship with 232 million dollars on the line, should not be reciting random poetry into the air out the exhaust pipe for a nice fireworks display. And, lately, are FormalistsTakingOverThisWiki?

I wholeheartedly agree with Jim that any attempt to formalize the notion of patterns misses the boat, but I do think that there are things that can benefit from formalization IN patterns.

Ward has noted elsewhere in WikiWikiWeb that some of the coding patterns that used to be used in assembly language coding have now been put into compilers. That sort of growth from art to science over time will also take some of what's useful in certain patterns and move them into tools and formal methods over time.

The point is not to formalize the "pattern" per se. The point is to formalize what the pattern is referring to. Remember that the map is not the thing.

KyleBrown

Kyle -- could you give an example of what you mean? For example, when I look at http://csg.uwaterloo.ca/patterns.html, it doesn't strike any chords in me, and I think it is counter to what we want to achieve. Alexander said: 

 I was no longer willing to start looking at any pattern unless
 it presented itself to me as having the capacity to connect up
 with some part of this quality [the quality without a name].
 Unless a particular pattern actually was capable of generating
 the kind of life and spirit that we are now discussing, and that
 it had this quality itself, my tendency was to dismiss it, even
 though we explored many, many patterns.


     -- StephenGrabow?, "Christopher Alexander:  The Search for
        a new paradigm."
That URL just falls short on "life" and "spirit."

See also

Eden A. H, J. Gil, A. Yehudai (1996). A Formal Language for Design Patterns. The 3rd Annual Conference on the Pattern Languages of Programs - PLoP(Washington University technical report WUCS-97-07)

and Mikkonen,T., Formalizing Design Patterns, Proceedings of the International Conference on Software Engineering, 1998. ACM Press. (p.115)

I agree with JimCoplien's statement above. Formalizing design patterns is too reminiscent of ToddCoram's story under KoansMetaphorsAndParables

Don't get me wrong, I haven't got anything against the papers cited above but I have encountered someone who's never done any OOP (let alone used a pattern) who's decided to define the meaning of "Design Pattern" mathematically. I'm not making this up 8-(

^Insert extensions, remarks and pointers to news and list discussions.^

See also: PeopleInterestedInFormalPatterns

--- Reliable and timely

Dependable distributed system typically utilize a hierarchy of protocols to provide for reliable and timely services. Such protocols have both dependability and real-time attributes, and the analysis of these protocols is a problem of growing complexity.

The development of precise and accurate formal specifications of these protocols and their subsequent formal verification to gain assurance have been a great challenge. Exploiting the inherent modularity in the design of most dependable protocols, in this thesis, we present our modular approach to specification composition and verification of dependable distributed protocol. In particular, we consider redundancy management protocols that are needed to manage redundant resources used in the system for dependability purposes.

Utilizing building-block protocols inherently used in redundancy management protocols, we perform compositional specification and verification of a checkpointing and recovery protocol based on them.

The key idea is that if a library of these basic components, like the primitives and sub-protocols are being formulated, then these elements aid in systematic and hierarchical development of dependable distributed protocols.

The main contribution of this thesis to illustrate the fact that by defining a priori validated building-blocks for dependable distributed protocols, larger and more complex protocols can be easily specified and verified. For a mechanical support in formal verification process, we use formal tools such as Specware and PVS.

from:

pdf:

CategoryFormalMethods

EditText of this page (last edited August 16, 2014) or FindPage with title or text search