Nisse Husberg

Docent (Verification)
address: Helsinki University of Technology, Department of Computer Science,
Theoretical Computer Science Laboratory (former Digital Systems) ,
room T-B255 ( Computer Science Building), Otnäsvägen 15, FIN-02150 ESBO, Finland.
Post address: PB 5400, FIN-02015 ESBO, Finland.
Home address: Bos-Sestu, FIN-07850 Hindersby, Finland.
tel: +358-9-451 3254, +358-40-769 0402 (mobile), +358-19-614 056 (home)
email: Nisse.Husberg"in domain"hut.fi
Office hour: Tuesdays 15:00-16:00 in the Computer Science Building, room T-B255

Plan:

Main project: Maria - A Modular Reachability Analyzer - is a new analyzer based on PROD and EMMA Extendible Multi-Method Analyzer for SDL (originally made for Nokia Telecommunications).

A high level Petri net model of a distributed dynamic channel allocation algorithm can be found here (presented at the High Level Petri Net Workshop in Aarhus, June 2000).

The use of Emma at Nokia Telecommunications was presented at the FM'99 conference in Toulouse 20-24 October in a paper[abstract]:

Nisse Husberg & Tapio Manner: "Emma: Developing an Industrial Reachability Analyser for SDL"

There was a presentation of handling dynamic constructs in Emma (and Maria) at the 11th Nordic Workshop on Programming Theory, Uppsala, Sweden October 6-8 1999:

Nisse Husberg: Formal Models of Dynamic Programming Constructs

The distributed dynamic channel allocation algorithm in

[DDCA95] R. Prakash, N. G. Shivaratri and M. Singhal: Distributed Dynamic Channel Allocation for Mobile Computing. In the Proceedings of the 14th ACM Symposium on Principles of Distributed Computing (PODC), Ottawa, Canada, Pages 47-56, August 21-23, 1995.

was presented at the SMC'99 in Tokyo, October 13-15 1999 by Nisse Husberg[abstract]:

Leo Ojala, *Nisse Husberg, and Simo Blom: "Modelling a Distributed Dynamic Channel Allocation Algorithm for Mobile Computing Using Predicate/Transition Nets"

(a model of this algorithm has been analysed using Maria).

There is a report from the Workshop on Concurrency, Specification & Programming in Berlin September 25-27 1996:
Nisse Husberg: SDL Modelling with High Level Petri Nets
(Sorry, but the Figures 2, 5 and 7 could not be included in the document itself).

Another report containing some new results is:
Nisse Husberg, Markus Malmqvist and Tero Jyrinki: Emma: A Tool for Analysis of SDL Programs (Postscript file).

A third paper is:
Nisse Husberg: Formal Models for Real Programs (Postscript file)
from the 8th Nordic Workshop on Programming Theory in Oslo 4-6 December 1996 .

Other projects: The use of (flow) graphs and category theory for modelling parallel and distributed systems.

Thesis "High Level Distributed Transition Systems" available in Postscript form (almost 2M).

Recent projects: Working on an uniform approach to Petri nets.

Teaching

Tik.79.185: Verification seminar.

Tik.79.193: Formal Description Techniques for Concurrent Systems.

Breidbaand (broadband)

Very personal homepage

Last change: 11 Januar 2005