W.J. Toetenel

(that's me)

Contact Information

Dr.Ir. W.J. Toetenel
Zuidplansoen 4
2628 BL Delft
Room 2.405
Tel: +31-152782518
Fax: +31-152787141

Electronic mail address w.j.toetenel@twi.tudelft.nl

Web address http://sepc.twi.tudelft.nl/~toet


(this page is currently under construction)

Employee Information

Job title
Universitair Hoofdocent Programmeren, Programmeertalen en Vertalers

Teaching activities:

Research activities:

Department or workgroup
My department's name : section SEPC (Software Engineering, Programming languages and Compilers)

prof. dr. ir. J. van Katwijk

Back to Top

Current Projects

Project : TTT (Type-checked Tree Tool)
TTT is to be a simple tool to generate C-language Data structures. It offers a data type definition facility similar to the VDM-SL data definition sublanguage, and a data generation facility that offers a complete range of data manipulation tools for creation, manipulation and destruction of data type values. Its main objective is to create simple data interfaces between applications written in the C language. TTT is tailored with respect to application within tools that manipulate very large data structures, such as verification tools using model-checking techniques.

The main difference between TTT and similar tools is the simplicity of the data definition language (DDL) and the dynamic type-checking facility of the constructed data type values. The DDL offers a model-oriented datatype structure similar to the approach taken in the VDM-SL specification language. DDL build-in data types include composite and union types, set, sequence and map types, tuple types and basic types such as integer, boolean and real types. Further DDL enables the definition of complex user-defined data types based on these build-in data types. For each build-in data type TTT offers a complete range of value manipulating functions, including the support for composite type values, set, sequence, map and tuple values. The support for complete tree structured data values include type checking facilities, tree copying, relational operators (equality and inequality), fast tree reading and writing operations, tree traversal operations, tree destruction and memory management operations and simple tree property management operations.

The usage of TTT is simple. The first step is the development of a DDL description of the data types for which support is to be generated. Next, a single application of the TTT generator results in a pre-compiled library containing all generated support functions and a C language header file which embodies the interface to the library functions. Now the user can develop applications using the library functions of the generated library. The library is created by the GNU C language translator tools.

Currently a prototype of TTT is operational and being used to develop a model-checker for a process algebra based formal specification language, MTCCS, developed within the research group of SEPC. Within the next months the prototype will be further refined and made available to others through the TTT www page.

Project: TVS (Toolset for Verification and Simulation)
The TVS project aims at the development of a toolset for verification and simulation of formal specifications of real-time embedded systems. The toolset is currently being build. See here for more details. Its first components will be a simulator-generator that accepts a abstract syntax and simulation semantics of the formal specification language for which specifications should be simulated, with front-ends for MTCCS and ASTRAL specifications and a verification tool for MTCSS specifications.
Project: MTCCS (Model-oriented Timed CCS)
MTCCS is a formal specification notation derived from TCCS and VDM-SL. It combines the data specific modelling powers of VDM-SL with the time and concurrency specific modelling features of TCCS. Currently the MTCCS notation is under construction. The notation is exercised within the context of several case studies. The projects comprises of the development of a MTCCS support environment, consisting of a MTCCS front-end, a MTCCS to XTGRAPH notation, a MTCCS/XTGRAPHS analyser and simulator.

Back to Top

Hot List

Back to Top

Personal Interests

Formal specification and design of real-time embedded systems
The area is complex and challenging. My interests include the "hybrid" systems and the role of Java as implementation language for real-time embedded systems.
Tool construction for analysis and simulation of formal notations for real-time embedded systems
Analysis techniques such as model-checking are currently being adapted to be used within the context of real-time embedded systems. A lot of experience and research is needed to develop algorithms that can be applied on case studies of realistic size.

Back to Top

Recent Publications

(will be added shortly)

Back to Top

Copyright W.J.Toetenel, TU Delft, TWI
Last revised: December 10, 1999.