NWPT'99
The 11th Nordic Workshop on Programming Theory
Uppsala University, Sweden, October 68, 1999
Proceedings
Preface
The objective of the Nordic Workshop on Programming Theory is to
bring together researchers from (but not limited to) the Nordic and
Baltic countries interested in programming theory, in order to improve
mutual contacts and cooperation.
The previous workshops were held in Uppsala (1989), Aalborg (1990),
Göteborg (1991 and 1995), Bergen (1992), Åbo
(1993 and 1998),
Aarhus (1994), Oslo (1996), and Tallinn
(1997).
In 1999 the workshop again took place at the MIC campus of
Uppsala University, hosted by the Department of Computer Systems.
The programme committee consisted of:
Magne Haveraaen (Bergen, NO),
HannuMatti Järvinen (Tampere, FI),
Kim G. Larsen (Aalborg, DK),
Bengt Nordstrom (Chalmers, SE),
Olaf Owe (Oslo, NO),
Hans Rischel (DTU, Lyngby, DK),
Kaisa Sere (Åbo Akademi, FI),
Jüri Vain (Inst. of Cybernetics, EE), and
Wang Yi (Uppsala, SE).
We would like to thank the authors of the submitted papers, the
invited speakers, and the members of the program committee for their
contribution to both the workshop and these proceedings. We are also
very grateful for the financial support of ASTEC, the Advanced Software
Technology competence centre.
The organizing committee:
Johan Bengtsson, Jakob Engblom, Björn Victor, and Wang Yi (chair)
(This is the online version of the proceedings, also available as Technical report 1999008 from the Department of Information Technology.)
Invited presentations

Validation of Synchronous Reactive Systems:
from Formal Verification to Automatic Testing
 Nicolas Halbwachs (VERIMAG, France)
 DataFlow Analysis as ModelChecking of Abstract Interpretations
 Bernhard Steffen (Dortmund University, Germany)

Stålmarck's method with extensions to first order logic
 Gunnar Stålmarck (Prover Technology AB, Sweden)

IndustrialStrength Functional Programming:
Experiences from the Ericsson AXD 301 Project
 Ulf Wiger (Ericsson Telecom)
Accepted submissions
 Testing


Conformance Testing of RealTime Systems with Timed Automata
 Rachel CardellOliver

Automated Generation of Test Oracles from Temporal Logic Specifications
 John Håkansson, Bengt Jonsson, Ola Lundkvist
 Synchronous Programming


Synchronous Dataflow Programming in ML
 M. Pouzet

Correct Implementations of Abstractions of Location
 Pertti Kellomäki
 Verification 1


Partial Order Reduction for Region Automata
 Dragan Bosnacki

Parametric modelchecking in PMC
 Giosué Bandini, Ronald Lutje Spelberg, Hans Toetenel

Binary Communication in Parameterized System Verification
 Parosh Aziz Abdulla, Ahmed Bouajjani, Bengt Jonsson, Marcus Nilsson

Syntactic Action Refinement in the Modal MuCalculus and its
Applications to the Verification of Reactive Systems
 Mila MajsterCederbaum, Frank Salger
 Semantics


On Semantics and Correctness of Reactive Rulebased Systems
 Man Lin, Jacek Malec, Simin NadjmTehrani

Formal Models of Dynamic Programming Constructs
 Nisse Husberg

On Shivers's Aggressive Cutoff Method A Study of the 0CFA
 Daniel Damian

Correctness of Unfold/Foldtransformations for Nondeterministic
Programs
 Björn Lisper
 Verification 2


Verification of Sequential Erlang Programs
 Gennady Chugunov, Larsåke Fredlund

Verification of State/Event Systems with Acyclic Dependencies by Quotienting
 Nicky O. Bodentien, Jacob Vestergaard, Jakob Friis, Kåre J. Kristoffersen, Kim G. Larsen
 Programming Languages


Distributed Implementation of a Process AlgebraBased
Programming Language for Embedded Systems
 Simon Mørk

Symmetry and Logic Programming
 Jinzhao Wu
 Logics and Semantics


BranchingTime Logic and Semantisc for Probabilistic Open Systems
 Purush Iyer

The AutomataTheoretic Approach Works for Global Trace Logics
 Jesper Gulmann Henriksen, Martin Leucker

Linking DC together with TRSL
 Anne Haxthausen, Xia Yong
 Software Technology


Formal Software Development using Generic Development Steps
 Axel Dold

On Modelling Feature Interaction in Telecommunications
 Bengt Jonsson, Tiziana Margaria, Gustaf Naeser, Jan Nyström, Bernhard Steffen

A generic tool for expressing the development of validations
 J.P. Bodeveix, M. Filali
 Case Studies


Verifying Distributed LEGO RCX Programs Using UPPAAL
 Morten Laursen, Rune Gee Madsen, Steffen Kondrup Mortensen

Modeling and Analysis of a Field Bus Protocol Using Uppaal
 Alexandre David, Ulf Hammar, Wang Yi

Guided Synthesis of Control Programs using Uppaal for an
Industrial Batch Plant
 Thomas Hune, Kim G. Larsen, Paul Pettersson
 Type and Proof Theory


Incorporating tuple types to C++
 Jaakko Järvi

Programming in MartinLöf Type Theory Unification  A nontrivial
Example
 Ana Bove

Extending the Window Inference Method
 Jeanette Heidenberg
 Hybrid Systems


General Hybrid Action Systems
 RalphJohan Back, Luigia Petre, Iván Porres Paltor

Linear Hybrid Action Systems
 Mauno Rönkkö, Xuandong Li

Case Study : A Temperature Control System Modeling and Verification
Using Action Systems Formalism Parallel Composition of Two or More
Control Systems Simultaneous Control
 RalphJohan Back, Cristina Cerschi, Iván Porres Paltor

Component based technique for hybrid control systems design
 Jüri Vain, Alar Kuusik, Marko Kääramees
 UML


An Outline of UML Class Diagram Semantics Using PVSSL
 Demissie B. Aredo, Issa Traoré, Ketil Stølen

An Implementation of UML State Machine Semantics for Model Checking
 Johan Lilius, Henri Sara

Code Generation for Hierarchical Systems
 Gerd Behrmann, Kåre Kristoffersen, Kim G. Larsen

Specifying the Abstract Layer of a Graphical Editor
 Orieta Celiku
 Propositional Logics & SAT


An Analogue of Stålmarck's Method for Intuitionistic Propositional
Logic
 Tarmo Uustalu

Symbolic Reachability Analysis Based on SAT Solvers
 Parosh Aziz Abdulla, Per Bjesse, Niklas Een
 ObjectOriented Techniques


OUN: A Formalism for Open, Object Oriented, Distributed Systems
 Olaf Owe, Isabelle Ryl

Object Integrity & Sharing <= True ObjectOrientation
 Harri Hakonen, Ville Leppänen, Timo Raita, Tapio Salakoski, Jukka Teuhola
 Logics and Semantics


The Decision Procedure for FinitelyValued Modal Propositional Logics
 Jurate Sakalauskaite

Correctness of migration in a subset of Obliq
 Hans Hüttel, Josva Kleist, Uwe Nestmann
 Action Systems


Mobile Components as Topological Action Systems
 L. Petre, M. Waldén

An Action Systems Approach to the FEAL8 Algorithm
 Tiberiu Seceleanu, Sören Holmström