This is an old revision of the document!
Please visit mareniers.wix.com/home for a personal homepage of me.
Some of the topics I am currently working on are listed below:
The Structured Operational Semantics of languages such as (Hybrid) Chi and CIF 2.0 result in infinite transition systems. One of the reasons of infinity can be that there are many solutions to a differential equation or to a predicate describing an update of the model variables. Another reason for infinity is in the way flow transitions are generated with different durations.
In this research we try to replace the concrete SOS by a symbolic SOS in which the values of the model variables are not incorporated yet in the semantics. It is our goal to obtain a finite symbolic transition system that may be instantiated to deliver the concrete transition system by incorporating appropriate valuations of model variables. We study the possibilities to base the development of a simulator for CIF 2.0 on such a symbolic SOS. Other (sub-)lines of research in this subject are
First experiments indicate that indeed it is possible to give a Symbolic SOS for the language CIF 2.0 (without scope operators). A formal relationship is established between the original concrete SOS and the new Symbolic SOS. As soon as these results are published this will be mentioned here.
We are developing a succesor for the modelling languages Chi (Chi 1) and Hybrid Chi (Chi 2). The language should allow for the combined specification of both discrete-event and continuous-time behaviour of systems. In due time, a simulator for this language will be developed. We are also considering to apply verification technology to models given in this language. On the technical side, we feel that the language should be a conservative extension of the basic process algbras from the book Process Algebra: Equational Theories of Communicating Processes by J.C.M. Baeten, T. Basten and M.A. Reniers.
We try to specify type checking for CIF 2.0 expressions by means of a deduction system in Modular SOS. Ultimately, we strive to generate an implementation of a type checker based on such a specification.
* 4B050 Werktuigbouwkunde in Vogelvlucht