|Reseach topic:||Processes in object analysis/design|
|Keywords:||Processes, object oriented analysis, process algebra, model checking, dynamic creation, polymorphic creation, transactions, component composition.|
|Thesis title?||Objects and Processes|
Integrating transactions and model checking with object oriented analysis
(Expected around december 2001)
|Description:||Model checking is an approach to verify precisely defined processes and their interactions, to ensure such things as absense of deadlock, termination and user-defined (temporal) properties. This does not scale up to object analysis, because analysis deals with more complicated process structures and because object oriented processes are often badly defined. I fight both problems in my PhD research.|
|Files to pull:||
My PhD thesis is done!|
Philosophy behind my Life Cycle Research
Paul (initial OO checker tool)
Life cycles (current research)
|Guiding senior:||Maarten Fokkinga|
My PhD research is a continuation of a project that our department's
Database group had performed for Compuware/Uniface.
That project has finished late 1999, and from that time on I spent my time solely on my PhD research and on teaching.
In the course of our work for Compuware, I developed a protocol checker named Paul, which is not under further development anymore.
Our lessons learnt from Paul will help us setting up a new process model for object oriented analysis.
We could have gone with the flow and use state charts, but these are simply too ill-defined and attempts to overcome this have stumbled over piles of disadvantages of state charts --- it seems better to me to define my own model instead.
This model is captured in our Life cycles, which are simple process models with great expressiveness and an elegantly simple semantics.
It has been designed as a practical language for object oriented analysis, but it seems to be possible to apply verification algorithms to it as well.
For verification, we are greatly inspired by work on model checking, but a problem is that most, if not all, approaches known to us can only check on bounded numbers of process instances, rendering the technique useless for conservative verification of object systems, where objects are created without bounds.
So, this is another problem I intend to solve, by peeking at theorem proving techniques.
The end result of my PhD research should be a theory plus supporting tools, for process verification in object oriented models.
The verifications will hopefully include common goals as well as user-specified (content-related) constraints on the object models.
If you're interested in a bit more, get the draft introduction chapter.