KAOS method support formal and semi-formal language to specify sofware requirements. http://www.info.ucl.ac.be/~avl/ReqEng.html

Thank you Omid Jafarinezhad, I will look into it.

Depends on what aspect of object-oriented systems you want to specify. Can you be more precise? What exactly is it that you want to specify or verify and why is it that you want to combine semi-formal and formal methods?

You could look into the Design by Contract family of languages, like JML (for Java) or Spec# for (C#).

take care,

Nikos

Kim Mens, Thanks for the response. Usually the OO systems are specified using a set of models mostly by diagrams. I feel there is a need to specify the entire system more rigorously. There comes the need for formal methods. Many works I have come across using Z/Object Z with UML, Event B with UML etc. The objective of every such combination/integration is to increase the reliability of the software system.

there are other methods like hoar logic and csp etc..

The correctness is of paramount importance while specifying the system and verification in establishing the same....

I think that UML is a visual specification method but at the same time is not that strong to prove or disprove the system behaviors and its properties.

UML

Event-B is a rigorous formal method for system specification. Rodin is an Eclipse-based IDE that provides tool support for Event-B. One Rodin plug-in is UML-B which, as its name suggests, combines UML and B. You may want to google Colin Snook (EECS/Univ Southampton), which is the main designer and maintainer of UML-B, I believe. He has also authored several papers on this approach.

Thanks David Déharbe, Are you working on uml-B?

Kumaresan, actually I do not work on UML-B. But I have seen a presentation by Prof Colin Snook and I have been impressed.

I also recommend JML and Spec#. I think, the very good things about these languages are:

- The languages are Formal

- There are a wide range of tools available for verification , specification generation and other stuff related to the language

- Wide range of papers, specially for JML

- Active community for learning

- Also they are familiar to the developer. I think one reason that developers do not approach to formal methods is that mathematical rigorous ways are difficult to learn and developers are not comfortable with.

Here is a very good paper regarding JML:

http://www.cs.ru.nl/E.Poll/publications/sttt05.pdf

Hope it helps,

Cheers

VDM++ can be used for the rigorous specification and verification of Object Oriented based development. VDM++ is an Object Oriented formal language. It is rigorous and ensures the correctness properties of the software. All types of properties can be specified by it.

It has a very efficient state of the art Eclipse based IDE tool named Overture. Overture is Open Source based on Eclipse and freely available for download.\

Do go for it..

And give your feedback,

Cheers

Dr. Nadeem.