Michael Westergaard's Homepage

This post has 2874 words. Reading it will take approximately 14 minutes.

Journals

2011

• M. Westergaard and L. M. Kristensen, “A Graphical Approach to Component-based and Extensible Model Checking Platforms,” in Transactions on Petri Nets and Other Models of Concurrency, 2011.
  [Bibtex]

  @inproceedings{asaptopnoc,
  author = {Westergaard, Michael and Kristensen, Lars Michael},
  title = {A Graphical Approach to Component-based and Extensible Model Checking Platforms},
  booktitle = {Transactions on Petri Nets and Other Models of Concurrency},
  howpublished = {To appear},
  year = {2011}
  }

2009

• S. Evangelista, M. Westergaard, and L. M. Kristensen, “The ComBack Method Revisited: Caching Strategies and Extension with Delayed Duplicate Detection,” Transactions on Petri Nets and Other Models of Concurrency, vol. 3, pp. 189-215, 2009.
  [Bibtex]

  @article{combacktopnoc,
  author = {Evangelista, Sami and Westergaard, Michael and Kristensen, Lars Michael},
  affiliation = {Aarhus University Computer Science Department Denmark},
  title = {The ComBack Method Revisited: Caching Strategies and Extension with Delayed Duplicate Detection},
  journal = {Transactions on Petri Nets and Other Models of Concurrency},
  series = {Lecture Notes in Computer Science},
  editor = {Jensen, Kurt and Billington, Jonathan and Koutny, Maciej},
  publisher = {Springer Berlin / Heidelberg},
  isbn = {},
  pages = {189-215},
  xvolume = {5800},
  volume = {3},
  doi = {10.1007/978-3-642-04856-2_8},
  note = {10.1007/978-3-642-04856-2_8},
  abstract = {The ComBack method is a memory reduction technique for explicit state space search algorithms. It enhances hash compaction with state reconstruction to resolve hash conflicts on-the-fly thereby ensuring full coverage of the state space. In this paper we provide two means to lower the run-time penalty induced by state reconstructions: a set of strategies to implement the caching method proposed in [20], and an extension through delayed duplicate detection that allows to group reconstructions together to save redundant work.},
  year = {2009}
  }

Conferences, reviewed

2011

• F. M. Maggi, M. Westergaard, M. Montali, and W. van der Aalst, “Runtime Verification of LTL-Based Declarative Process Models,” in Proc. of RV, 2011.
  [Bibtex]

  @inproceedings{conflicting,
  author = {Maggi, Fabrizio Maria and Westergaard, Michael and Montali, Marco and van der Aalst, Wil M. P.},
  title = {Runtime Verification of LTL-Based Declarative Process Models},
  booktitle = {Proc. of RV},
  howpublished = {To appear},
  year = {2011}
  }

• M. Westergaard, “Better Algorithms for Analyzing and Enacting Declarative Workflow Languages Using LTL,” in Proc. of BPM, 2011.
  [Bibtex]

  @inproceedings{improved-translation,
  author = {Westergaard, Michael},
  title = {Better Algorithms for Analyzing and Enacting Declarative Workflow Languages Using LTL},
  booktitle = {Proc. of BPM},
  howpublished = {To appear},
  year = {2011}
  }

• F. M. Maggi, M. Montali, M. Westergaard, and W. van der Aalst, “Monitoring Business Constraints with Linear Temporal Logic: An Approach Based on Colored Automata,” in Proc. of BPM, 2011.
  [Bibtex]

  @inproceedings{colored-automata,
  author = {Maggi, Fabrizio Maria and Montali, Marco and Westergaard, Michael and van der Aalst, Wil M. P.},
  title = {Monitoring Business Constraints with Linear Temporal Logic: An Approach Based on Colored Automata},
  booktitle = {Proc. of BPM},
  howpublished = {To appear},
  year = {2011}
  }

• M. Westergaard and F. M. Maggi, “Modeling and Verification of a Protocol for Operational Support Using Coloured Petri Nets,” , L. M. Kristensen and L. Petrucci, Ed., Springer Berlin / Heidelberg, 2011, vol. 6709, pp. 169-188.
  [Bibtex]

  @incollection{osprotocol,
  author = {Westergaard, Michael and Maggi, Fabrizio Maria},
  affiliation = {Department of Mathematics and Computer Science, Eindhoven University of Technology, The Netherlands},
  title = {Modeling and Verification of a Protocol for Operational Support Using Coloured Petri Nets},
  booktitle = {Applications and Theory of Petri Nets},
  series = {Lecture Notes in Computer Science},
  editor = {Kristensen, Lars Michael and Petrucci, Laure},
  publisher = {Springer Berlin / Heidelberg},
  isbn = {},
  pages = {169-188},
  volume = {6709},
  doi = {10.1007/978-3-642-21834-7_10},
  note = {10.1007/978-3-642-21834-7_10},
  abstract = {In this paper, we describe the modeling and analysis of a protocol for operational support during workflow enactment. Operational support provides online replies to questions such as  is my execution valid?  and  how do I end the execution in the fastest/cheapest way? , and may be invoked multiple times for each execution.   Multiple applications (operational support providers) may be able to answer such questions, so a protocol supporting this should be able to handle multiple providers, maintain data between queries about the same execution, and discard information when it is no longer needed.    We present a coloured Petri net model of a protocol satisfying our requirements. The model is used both to make our requirements clear by building a model-based prototype before implementation and to verify that the devised protocol is correct.    We present techniques to make analysis of the large state-space of the model possible, including modeling techniques and an improved state representation for coloured Petri nets allowing explicit representation of state spaces with more than 108 states on a normal PC.    We briefly describe our implementation in the process mining tool ProM and how we have used it to improve an existing provider.},
  year = {2011}
  }

2010

• L. M. Kristensen and M. Westergaard, “Automatic Structure-Based Code Generation from Coloured Petri Nets: A Proof of Concept,” , S. Kowalewski and M. Roveri, Ed., Springer Berlin / Heidelberg, 2010, vol. 6371, pp. 215-230.
  [Bibtex]

  @incollection{codegeneration,
  author = {Kristensen, Lars Michael and Westergaard, Michael},
  affiliation = {Department of Computer Engineering, Bergen University College, Norway},
  title = {Automatic Structure-Based Code Generation from Coloured Petri Nets: A Proof of Concept},
  booktitle = {Formal Methods for Industrial Critical Systems},
  series = {Lecture Notes in Computer Science},
  editor = {Kowalewski, Stefan and Roveri, Marco},
  publisher = {Springer Berlin / Heidelberg},
  isbn = {},
  pages = {215-230},
  volume = {6371},
  doi = {10.1007/978-3-642-15898-8_14},
  note = {10.1007/978-3-642-15898-8_14},
  abstract = {Automatic code generation based on Coloured Petri Net (CPN) models is challenging because CPNs allow for the construction of abstract models that intermix control flow and data processing, making translation into conventional programming constructs difficult. We introduce Process-Partitioned CPNs (PP-CPNs) which is a subclass of CPNs equipped with an explicit separation of process control flow, message passing, and access to shared and local data. We show how PP-CPNs caters for a four phase structure-based automatic code generation process directed by the control flow of processes. The viability of our approach is demonstrated by applying it to automatically generate an Erlang implementation of the Dynamic MANET On-demand (DYMO) routing protocol specified by the Internet Engineering Task Force (IETF).},
  year = {2010}
  }

2009

• M. Westergaard, L. M. Kristensen, and M. Kuusela, “Towards Cosimulating SystemC and Coloured Petri Net Models for SoC Functional and Performance Evaluation,” in ∥roceedings of 21st European Modeling and Simulation Symposium, 2009.
  [Bibtex]

  @inproceedings{cosimulation,
  author = {Westergaard, Michael and Kristensen, Lars Michael and Kuusela, Maija},
  affiliation = {Department of Computer Science, University of Aarhus, IT-parken, Aabogade 34, DK-8200 Aarhus N Denmark},
  title = {Towards Cosimulating SystemC and Coloured Petri Net Models for SoC Functional and Performance Evaluation},
  booktitle = {∥roceedings of 21st European Modeling and Simulation Symposium},
  year = {2009}
  }

2007

• M. Westergaard, L. M. Kristensen, G. S. Brodal, and L. Arge, “The ComBack Method – Extending Hash Compaction with Backtracking,” , J. Kleijn and A. Yakovlev, Ed., Springer Berlin / Heidelberg, 2007, vol. 4546, pp. 445-464.
  [Bibtex]

  @incollection{comback,
  author = {Westergaard, Michael and Kristensen, Lars Michael and Brodal, Gerth Stølting and Arge, Lars},
  affiliation = {Department of Computer Science, University of Aarhus, IT-parken, Aabogade 34, DK-8200 Aarhus N Denmark},
  title = {The ComBack Method – Extending Hash Compaction with Backtracking},
  booktitle = {Petri Nets and Other Models of Concurrency – ICATPN 2007},
  series = {Lecture Notes in Computer Science},
  editor = {Kleijn, Jetty and Yakovlev, Alex},
  publisher = {Springer Berlin / Heidelberg},
  isbn = {},
  pages = {445-464},
  volume = {4546},
  doi = {10.1007/978-3-540-73094-1_26},
  note = {10.1007/978-3-540-73094-1_26},
  abstract = {This paper presents the ComBack method for explicit state space exploration. The ComBack method extends the well-known hash compaction method such that full coverage of the state space is guaranteed. Each encountered state is mapped into a compressed state descriptor (hash value) as in hash compaction. The method additionally stores for each state an integer representing the identity of the state and a backedge to a predecessor state. This allows hash collisions to be resolved on-the-fly during state space exploration using backtracking to reconstruct the full state descriptors when required for comparison with newly encountered states. A prototype implementation of the ComBack method is used to evaluate the method on several example systems and compare its performance to related methods. The results show a reduction in memory usage at an acceptable cost in exploration time.},
  year = {2007}
  }

2005

• L. M. Kristensen, M. Westergaard, and P. C. Nørgaard, “Model-Based Prototyping of an Interoperability Protocol for Mobile Ad-Hoc Networks,” , J. Romijn, G. Smith, and J. van de Pol, Ed., Springer Berlin / Heidelberg, 2005, vol. 3771, pp. 266-286.
  [Bibtex]

  @incollection{ncw,
  author = {Kristensen, Lars Michael and Westergaard, Michael and Nørgaard, Peder Christian},
  affiliation = {Department of Computer Science, University of Aarhus, IT-parken, Aabogade 34, DK-8200 Aarhus N, Denmark},
  title = {Model-Based Prototyping of an Interoperability Protocol for Mobile Ad-Hoc Networks},
  booktitle = {Integrated Formal Methods},
  series = {Lecture Notes in Computer Science},
  editor = {Romijn, Judi and Smith, Graeme and van de Pol, Jaco},
  publisher = {Springer Berlin / Heidelberg},
  isbn = {},
  pages = {266-286},
  volume = {3771},
  doi = {10.1007/11589976_16},
  note = {10.1007/11589976_16},
  abstract = {We present an industrial project conducted at Ericsson Danmark A/S, Telebit where formal methods in the form of Coloured Petri Nets (CP-nets or CPNs) have been used for the specification of an interoperability protocol for routing packets between fixed core networks and mobile ad-hoc networks. The interoperability protocol ensures that a packet flow between a host in a core network and a mobile node in an ad-hoc network is always relayed via one of the closest gateways connecting the core network and the mobile ad-hoc network. This paper shows how integrated use of CP-nets and application-specific visualisation have been applied to build a model-based prototype of the interoperability protocol. The prototype consists of two parts: a CPN model that formally specifies the protocol mechanisms and a graphical user interface for experimenting with the protocol. The project demonstrates that the use of formal modelling combined with the use of application-specific visualisation can be an effective approach to rapidly construct an executable prototype of a communication protocol.},
  year = {2005}
  }

2004

• T. Mailund and M. Westergaard, “Obtaining Memory-Efficient Reachability Graph Representations Using the Sweep-Line Method,” , K. Jensen and A. Podelski, Ed., Springer Berlin / Heidelberg, 2004, vol. 2988, pp. 177-191.
  [Bibtex]

  @incollection{patchgraph,
  author = {Mailund, Thomas and Westergaard, Michael},
  affiliation = {Department of Computer Science, University of Aarhus, IT-parken, Aabogade 34, DK-8200 Aarhus N, Denmark},
  title = {Obtaining Memory-Efficient Reachability Graph Representations Using the Sweep-Line Method},
  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems},
  series = {Lecture Notes in Computer Science},
  editor = {Jensen, Kurt and Podelski, Andreas},
  publisher = {Springer Berlin / Heidelberg},
  isbn = {},
  pages = {177-191},
  volume = {2988},
  doi = {10.1007/978-3-540-24730-2_16},
  note = {10.1007/978-3-540-24730-2_16},
  abstract = {This paper is concerned with a memory-efficient representation of reachability graphs. We describe a technique that enables us to represent each reachable marking in a number of bits close to the theoretical minimum needed for explicit state enumeration. The technique maps each state vector onto a number between zero and the number of reachable states and uses the sweep-line method to delete the state vectors themselves. A prototype of the proposed technique has been implemented and experimental results are reported.},
  year = {2004}
  }

Reviewed Tool Papers at Conferences

2011

• M. Westergaard and F. M. Maggi, “Declare: A Tool Suite for Declarative Workflow Modeling and Enactment,” in BPM Tools, 2011.
  [Bibtex]

  @inproceedings{declare,
  author = {Westergaard, Michael and Maggi, Fabrizio Maria},
  title = {Declare: A Tool Suite for Declarative Workflow Modeling and Enactment},
  booktitle = {BPM Tools},
  year = {2011}
  }

• M. Westergaard, “Access/CPN 2.0: A High-Level Interface to Coloured Petri Net Models,” , L. M. Kristensen and L. Petrucci, Ed., Springer Berlin / Heidelberg, 2011, vol. 6709, pp. 328-337.
  [Bibtex]

  @incollection{accesscpn2,
  author = {Westergaard, Michael},
  affiliation = {Department of Mathematics and Computer Science, Eindhoven University of Technology, The Netherlands},
  title = {Access/CPN 2.0: A High-Level Interface to Coloured Petri Net Models},
  booktitle = {Applications and Theory of Petri Nets},
  series = {Lecture Notes in Computer Science},
  editor = {Kristensen, Lars Michael and Petrucci, Laure},
  publisher = {Springer Berlin / Heidelberg},
  isbn = {},
  pages = {328-337},
  volume = {6709},
  doi = {10.1007/978-3-642-21834-7_19},
  note = {10.1007/978-3-642-21834-7_19},
  abstract = {This paper introduces Access/CPN 2.0, which extends Access/ CPN with high-level primitives for interacting with coloured Petri net (CPN) models in Java programs. The primitives allow Java programs to monitor and interact with places and transitions during execution, and embed entire programs as subpages of CPN models or embed CPN models as parts of programs. This facilitates building environments for systematic testing of program components using a CPN models. We illustrate the use of Access/CPN 2.0 in the context of business processes by embedding a workflow system into a CPN model.},
  year = {2011}
  }

2009

• M. Westergaard and L. M. Kristensen, “The Access/CPN Framework: A Tool for Interacting with the CPN Tools Simulator,” , G. Franceschinis and K. Wolf, Ed., Springer Berlin / Heidelberg, 2009, vol. 5606, pp. 313-322.
  [Bibtex]

  @incollection{accesscpn,
  author = {Westergaard, Michael and Kristensen, Lars Michael},
  affiliation = {Aarhus University Department of Computer Science Denmark},
  title = {The Access/CPN Framework: A Tool for Interacting with the CPN Tools Simulator},
  booktitle = {Applications and Theory of Petri Nets},
  series = {Lecture Notes in Computer Science},
  editor = {Franceschinis, Giuliana and Wolf, Karsten},
  publisher = {Springer Berlin / Heidelberg},
  isbn = {},
  pages = {313-322},
  volume = {5606},
  doi = {10.1007/978-3-642-02424-5_19},
  note = {10.1007/978-3-642-02424-5_19},
  abstract = {Coloured Petri nets (CP-nets or CPNs) is a widely used formalism for describing concurrent systems. CPN Tools provides a mature environment for constructing, simulating, and performing analysis of CPN models. CPN Tools also has limitations if, for example, one wishes to extend the analysis capabilities or to integrate CPN models into external applications. In this paper we present Access/CPN, a framework that facilitates such extensions. Access/CPN consists of two interfaces: one written in Standard ML, which is very close to the simulator component of CPN Tools, and one written in Java, providing an object-oriented representation of CPN models, a means to load models created using CPN Tools, and an interface to the simulator. We illustrate Access/CPN by providing the complete implementation of a simple command-line state space exploration tool.},
  year = {2009}
  }

• M. Westergaard, S. Evangelista, and L. M. Kristensen, “ASAP: An Extensible Platform for State Space Analysis,” , G. Franceschinis and K. Wolf, Ed., Springer Berlin / Heidelberg, 2009, vol. 5606, pp. 303-312.
  [Bibtex]

  @incollection{asap,
  author = {Westergaard, Michael and Evangelista, Sami and Kristensen, Lars Michael},
  affiliation = {Aarhus University Department of Computer Science Denmark},
  title = {ASAP: An Extensible Platform for State Space Analysis},
  booktitle = {Applications and Theory of Petri Nets},
  series = {Lecture Notes in Computer Science},
  editor = {Franceschinis, Giuliana and Wolf, Karsten},
  publisher = {Springer Berlin / Heidelberg},
  isbn = {},
  pages = {303-312},
  volume = {5606},
  doi = {10.1007/978-3-642-02424-5_18},
  note = {10.1007/978-3-642-02424-5_18},
  abstract = {The ASCoVeCo State space Analysis Platform (ASAP) is a tool for performing explicit state space analysis of coloured Petri nets (CPNs) and other formalisms. ASAP supports a wide range of state space reduction techniques and is intended to be easy to extend and to use, making it a suitable tool for students, researchers, and industrial users that would like to analyze protocols and/or experiment with different algorithms. This paper presents ASAP from these two perspectives.},
  year = {2009}
  }

2006

• M. Westergaard and K. Lassen, “The BRITNeY Suite Animation Tool,” , S. Donatelli and Thiagarajan, Ed., Springer Berlin / Heidelberg, 2006, vol. 4024, pp. 431-440.
  [Bibtex]

  @incollection{britney,
  author = {Westergaard, Michael and Lassen, Kristian},
  affiliation = {Department of Computer Science, University of Aarhus, IT-parken, Aabogade 34, DK-8200 Aarhus N, Denmark},
  title = {The BRITNeY Suite Animation Tool},
  booktitle = {Petri Nets and Other Models of Concurrency - ICATPN 2006},
  series = {Lecture Notes in Computer Science},
  editor = {Donatelli, Susanna and Thiagarajan, P.},
  publisher = {Springer Berlin / Heidelberg},
  isbn = {},
  pages = {431-440},
  volume = {4024},
  doi = {10.1007/11767589_26},
  note = {10.1007/11767589_26},
  abstract = {This paper describes the BRITNeY suite, a tool which enables users to create visualizations of formal models. BRITNeY suite is integrated with CPN Tools, and we give an example of how to extend a simple stop-and-wait protocol with a visualization in the form of message sequence charts. We also show examples of animations created during industrial projects to give an impression of what is possible with the BRITNeY suite.},
  year = {2006}
  }

2003

• A. V. Ratzer, L. Wells, H. M. Lassen, M. Laursen, J. F. Qvortrup, M. S. Stissing, M. Westergaard, S. Christensen, and K. Jensen, “CPN Tools for Editing, Simulating, and Analysing Coloured Petri Nets,” , W. van der Aalst and E. Best, Ed., Springer Berlin / Heidelberg, 2003, vol. 2679, pp. 450-462.
  [Bibtex]

  @incollection{cpntools03,
  author = {Ratzer, Anne Vinter and Wells, Lisa and Lassen, Henry Michael and Laursen, Mads and Qvortrup, Jacob Frank and Stissing, Martin Stig and Westergaard, Michael and Christensen, Søren and Jensen, Kurt},
  affiliation = {University of Aarhus IT-parken Department of Computer Science Aabogade 34 DK-8200 Århus N Denmark},
  title = {CPN Tools for Editing, Simulating, and Analysing Coloured Petri Nets},
  booktitle = {Applications and Theory of Petri Nets 2003},
  series = {Lecture Notes in Computer Science},
  editor = {van der Aalst, Wil and Best, Eike},
  publisher = {Springer Berlin / Heidelberg},
  isbn = {},
  pages = {450-462},
  volume = {2679},
  doi = {10.1007/3-540-44919-1_28},
  note = {10.1007/3-540-44919-1_28},
  abstract = {CPN Tools is a tool for editing, simulating and analysing Coloured Petri Nets. The GUI is based on advanced interaction techniques, such as toolglasses, marking menus, and bi-manual interaction. Feedback facilities provide contextual error messages and indicate dependency relationships between net elements. The tool features incremental syntax checking and code generation which take place while a net is being constructed. A fast simulator efficiently handles both untimed and timed nets. Full and partial state spaces can be generated and analysed, and a standard state space report contains information such as boundedness properties and liveness properties. The functionality of the simulation engine and state space facilities are similar to the corresponding components in Design/CPN, which is a widespread tool for Coloured Petri Nets.},
  year = {2003}
  }