Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Homepage of Ulrik Larsen

Homepage of Ulrik Larsen

Ulrik Mathias Nyman Larsen
Born: 2nd of December 1978

Ph.D. Student
Center for Embedded Software Systems (CISS)
Department of Computer Science
Aalborg University
Fr. Bajersvej 7B
DK-9220 Aalborg East
Room: B2-206
Phone: ((+45) 96 35) 72 26
ulrikl AT cs dot aau dot dk

My calendar

Project Description:

Automatic test case generation and distributed model checking.

The motivation behind the project is to extend the applicability of formal models of software systems, by to different approaches.

Model based test case generation.
Distributed model checking algorithms.

The aim of model based test case generation is to automatically generate relevant test cases from a formal model. This can be used as an addition to verification, such that the final product can be tested against the requirements of the formal model. Test case generation methods can also be aimed at handling systems that are too large for verification, such that the formal models of such systems still could be put to use in validating the design and implementation of the system.
The aim of distributed model checking is to extend the domain of models that can be verified within reasonable time. Greater and greater computing resources are always becoming available, but these resources are not always in the form of a single processor. Multi processor machines are more and more commonplace, thus it is necessary to use both, parallelism at the local level to speed up verification, and distributed resources at larger levels in order to be able to verify larger models.
There are also some possibilities in using the power of distribution in combination with testing. Distributed algorithms can be used to speed up the generation of test cases. Test execution can also be distributed, thus aiming at faster discovery of errors, by having multiple computers executing different test cases from the same test suite against identical implementations under test.

Tools and Models

I will concentrate on applying these techniques in relation to two different tools and corresponding modeling languages.

Uppaal and timed automata:

A university tool developed in cooperation between Aalborg University and Uppsala University.

visualSTATE and state/event machines:

During the fall of 2003 and the spring of 2004 I have, as a research assistant, been part of a cooperation project between CISS and the company IAR Systems A/S that develop the visualSTATE tool. The purpose of the cooperation was to implement automatic test case generation in the visualSTATE tool. I will continue to cooperate closely with IAR Systems both on test case generation and on other issues in relation to visualSTATE.

Projekt beskrivelse på Dansk

Student Projects: 1998 - 2003

Pictures of our cats Leif and Fie