Looking for a set of specific Problems to work on for my doctoral work
KAOS method support formal and semi-formal language to specify sofware requirements. http://www.info.ucl.ac.be/~avl/ReqEng.html
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.
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.
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.
- Badges
- Science topic
- Similar topics
- Computer Science and Engineering
- Software