Publications

This post has 8422 words. Reading it will take approximately 42 minutes.

Bacon Number 4
Erdös Number 4
h-index 20
i10-index 31
Citations ≥ 1900

Some of my publications can be seen on DBLP, via CiteSeer, or on Google Scholar.

 
”Journals”

2013

  • [PDF] [DOI] W. M. P. Aalst, C. Stahl, and M. Westergaard, “Strategies for Modeling Complex Processes Using Colored Petri Nets,” Transactions on Petri Nets and Other Models of Concurrency, vol. 7, pp. 6-55, 2013.
    [Bibtex]
    @article{cpncourse,
    year={2013},
    isbn={978-3-642-38142-3},
    booktitle={Transactions on Petri Nets and Other Models of Concurrency VII},
    journal={Transactions on Petri Nets and Other Models of Concurrency},
    xvolume={7480},
    volume = 7,
    series={Lecture Notes in Computer Science},
    editor={Jensen, Kurt and Aalst, Wil M.P. and Balbo, Gianfranco and Koutny, Maciej and Wolf, Karsten},
    doi={10.1007/978-3-642-38143-0_2},
    title={Strategies for Modeling Complex Processes Using Colored Petri Nets},
    url={http://dx.doi.org/10.1007/978-3-642-38143-0_2},
    publisher={Springer Berlin Heidelberg},
    keywords={Colored Petri nets; Design patterns; CPN Tools},
    author={Aalst, Wil M.P. and Stahl, Christian and Westergaard, Michael},
    pages={6-55}
    }
  • [DOI] M. Westergaard, D. Fahland, and C. Stahl, “Grade/CPN: A Tool and Temporal Logic for Testing Colored Petri Net Models in Teaching,” Transactions on Petri Nets and Other Models of Concurrency, vol. 8, pp. 180-202, 2013.
    [Bibtex]
    @article{gradecpntopnoc,
    year={2013},
    isbn={978-3-642-40464-1},
    booktitle={Transactions on Petri Nets and Other Models of Concurrency VIII},
    journal={Transactions on Petri Nets and Other Models of Concurrency},
    xvolume={8100},
    volume={8},
    series={Lecture Notes in Computer Science},
    editor={Koutny, Maciej and Aalst, WilM.P. and Yakovlev, Alex},
    doi={10.1007/978-3-642-40465-8_10},
    title={Grade/CPN: A Tool and Temporal Logic for Testing Colored Petri Net Models in Teaching},
    url={http://dx.doi.org/10.1007/978-3-642-40465-8_10},
    publisher={Springer Berlin Heidelberg},
    author={Westergaard, Michael and Fahland, Dirk and Stahl, Christian},
    pages={180-202}
    }

2012

  • [PDF] [DOI] T. Mailund, A. E. Halager, M. Westergaard, J. Y. Dutheil, K. Munch, L. N. Andersen, G. Lunter, K. Prüfer, A. Scally, A. Hobolth, and M. H. Schierup, “A New Isolation with Migration Model along Complete Genomes Infers Very Different Divergence Processes among Closely Related Great Ape Species,” PLoS Genet, vol. 8, iss. 12, p. e1003125, 2012.
    [Bibtex]
    @article{migration,
        author = {Mailund, , Thomas AND Halager, , Anders E. AND Westergaard, , Michael AND Dutheil, , Julien Y. AND Munch, , Kasper AND Andersen, , Lars N. AND Lunter, , Gerton AND Prüfer, , Kay AND Scally, , Aylwyn AND Hobolth, , Asger AND Schierup, , Mikkel H.},
        journal = {PLoS Genet},
        publisher = {Public Library of Science},
        title = {A New Isolation with Migration Model along Complete Genomes Infers Very Different Divergence Processes among Closely Related Great Ape Species},
        year = {2012},
        month = {12},
        volume = {8},
        url = {http://dx.doi.org/10.1371%2Fjournal.pgen.1003125},
        pages = {e1003125},
        abstract = {Author Summary

    Next-generation sequencing technology has enabled the generation of whole-genome data for many closely related species. For population genetic inference we have sequenced many loci, but only in a few individuals. We present a new method that allows inference of the divergence process based on two closely related genomes, modelled as gradual isolation in an isolation with migration model. This allows estimation of the initial time of restricted gene flow, the cessation of gene flow, as well as the population sizes, migration rates, and recombination rates. We show by simulations that the parameter estimation is accurate with genome-wide data and use the model to disentangle the divergence processes among three sets of closely related great ape species: bonobo/chimpanzee, eastern/western gorillas, and Sumatran/Bornean orang-utans. We find allopatric speciation for bonobo and chimpanzee and non-allopatric speciation for the gorillas and orang-utans. We also consider the split between humans and chimpanzees/bonobos and find evidence for non-allopatric speciation, similar to that within gorillas and orang-utans.

    }, number = {12}, doi = {10.1371/journal.pgen.1003125} }
  • [PDF] [DOI] M. Westergaard, “Verifying Parallel Algorithms and Programs Using Coloured Petri Nets,” Transactions on Petri Nets and Other Models of Concurrency, vol. 6, pp. 146-168, 2012.
    [Bibtex]
    @article{paralleltopnoc,
    year={2012},
    isbn={978-3-642-35178-5},
    booktitle={Transactions on Petri Nets and Other Models of Concurrency VI},
    journal ={Transactions on Petri Nets and Other Models of Concurrency},
    xvolume={7400},
    volume = 6,
    series={Lecture Notes in Computer Science},
    editor={Jensen, Kurt and Aalst, WilM. and Ajmone Marsan, Marco and Franceschinis, Giuliana and Kleijn, Jetty and Kristensen, Lars Michael},
    doi={10.1007/978-3-642-35179-2_7},
    title={Verifying Parallel Algorithms and Programs Using Coloured Petri Nets},
    url={http://dx.doi.org/10.1007/978-3-642-35179-2_7},
    publisher={Springer Berlin Heidelberg},
    author={Westergaard, Michael},
    pages={146-168}
    }
  • [PDF] [DOI] M. Westergaard and L. Kristensen, “A Graphical Approach to Component-Based and Extensible Model Checking Platforms,” Transactions on Petri Nets and Other Models of Concurrency, vol. 5, pp. 265-291, 2012.
    [Bibtex]
    @article{asaptopnoc,
    author = {Westergaard, Michael and Kristensen, Lars},
    affiliation = {Department of Mathematics and Computer Science, Eindhoven University of Technology, The Netherlands},
    title = {A Graphical Approach to Component-Based and Extensible Model Checking Platforms},
    journal = {Transactions on Petri Nets and Other Models of Concurrency},
    series = {Lecture Notes in Computer Science},
    editor = {Jensen, Kurt and Donatelli, Susanna and Kleijn, Jetty},
    publisher = {Springer Berlin / Heidelberg},
    isbn = {978-3-642-29071-8},
    keyword = {Computer Science},
    pages = {265-291},
    xvolume = {6900},
    volume = 5,
    url = {http://dx.doi.org/10.1007/978-3-642-29072-5_12},
    doi = {10.1007/978-3-642-29072-5_12},
    note = {10.1007/978-3-642-29072-5_12},
    abstract = {Model checking is applied for verification of concurrent systems by users having different skills and background. This ranges from researchers with detailed knowledge of the inner workings of the tools to engineers that are mostly interested in applying the technology as a black-box. This paper proposes JoSEL, a graphical language for specification of executable model checking jobs. JoSEL makes it possible to work at different levels of abstraction when interacting with the underlying components of a model checking tool and thereby supports the different kinds of users in a uniform manner. A verification job in JoSEL consists of tasks, ports, and connections describing the models to verify, the behavioural properties to checked, and the model checking techniques to apply. A job can then be mapped onto components of an underlying model checking tool for execution. We introduce the syntax of JoSEL, define its semantics, and show how JoSEL has been used as a basis for the user interface of the ASAP model checking platform.},
    year = {2012}
    }

2009

  • [PDF] [DOI] 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”
❗ These are all reviewed papers published at conferences.  ❗

2013

  • R. Müller, C. Stahl, W. M. P. van der Aalst, and M. Westergaard, “Service Discovery from Observed Behavior While Guaranteeing Deadlock Freedom in Collaborations,” 2013.
    [Bibtex]
    @techreport{service,
    author = {Müller, Richard and Stahl, Christian and van der Aalst, Wil M. P. and Westergaard, Michael},
    title = {Service Discovery from Observed Behavior While Guaranteeing Deadlock Freedom in Collaborations},
    booktitle = {Proc. of ICSOC},
    howpublished = {To appear},
    year = 2013,
    }
  • [DOI] M. Westergaard and T. Slaats, “Mixing Paradigms for More Comprehensible Models,” in Business Process Management, 2013, pp. 283-290.
    [Bibtex]
    @inproceedings{mixedparadigms,
    year={2013},
    isbn={978-3-642-40175-6},
    booktitle={Business Process Management},
    volume={8094},
    series={Lecture Notes in Computer Science},
    editor={Daniel, Florian and Wang, Jianmin and Weber, Barbara},
    doi={10.1007/978-3-642-40176-3_24},
    title={Mixing Paradigms for More Comprehensible Models},
    url={http://dx.doi.org/10.1007/978-3-642-40176-3_24},
    publisher={Springer Berlin Heidelberg},
    author={Westergaard, Michael and Slaats, Tijs},
    pages={283-290}
    }

2012

  • [PDF] [DOI] F. Maggi, M. Westergaard, M. Montali, and W. van der Aalst, “Runtime Verification of LTL-Based Declarative Process Models,” in Runtime Verification, 2012, pp. 131-146.
    [Bibtex]
    @inproceedings{conflicting,
    author = {Maggi, Fabrizio and Westergaard, Michael and Montali, Marco and van der Aalst, Wil},
    affiliation = {Eindhoven University of Technology, The Netherlands},
    title = {Runtime Verification of LTL-Based Declarative Process Models},
    booktitle = {Runtime Verification},
    series = {Lecture Notes in Computer Science},
    editor = {Khurshid, Sarfraz and Sen, Koushik},
    publisher = {Springer Berlin / Heidelberg},
    isbn = {978-3-642-29859-2},
    keyword = {Computer Science},
    pages = {131-146},
    volume = {7186},
    url = {http://dx.doi.org/10.1007/978-3-642-29860-8_11},
    doi = {10.1007/978-3-642-29860-8_11},
    note = {10.1007/978-3-642-29860-8_11},
    abstract = {Linear Temporal Logic (LTL) on finite traces has proven to be a good basis for the analysis and enactment of flexible constraint-based business processes. The Declare language and system benefit from this basis. Moreover, LTL-based languages like Declare can also be used for runtime verification. As there are often many interacting constraints, it is important to keep track of individual constraints and combinations of potentially conflicting constraints . In this paper, we operationalize the notion of conflicting constraints and demonstrate how innovative automata-based techniques can be applied to monitor running process instances. Conflicting constraints are detected immediately and our toolset (realized using Declare and ProM) provides meaningful diagnostics.},
    year = {2012}
       }
  • [PDF] [DOI] T. Mailund, A. Halager, and M. Westergaard, “Using Colored Petri Nets to Construct Coalescent Hidden Markov Models: Automatic Translation from Demographic Specifications to Efficient Inference Methods,” in Application and Theory of Petri Nets, 2012, pp. 32-50.
    [Bibtex]
    @inproceedings{biologyhmm,
    author = {Mailund, Thomas and Halager, Anders and Westergaard, Michael},
    affiliation = {Bioinformatics Research Center, Aarhus University, Denmark},
    title = {Using Colored Petri Nets to Construct Coalescent Hidden Markov Models: Automatic Translation from Demographic Specifications to Efficient Inference Methods},
    booktitle = {Application and Theory of Petri Nets},
    series = {Lecture Notes in Computer Science},
    editor = {Haddad, Serge and Pomello, Lucia},
    publisher = {Springer Berlin / Heidelberg},
    isbn = {978-3-642-31130-7},
    keyword = {Computer Science},
    pages = {32-50},
    volume = {7347},
    url = {http://dx.doi.org/10.1007/978-3-642-31131-4_3},
    doi = {10.1007/978-3-642-31131-4_3},
    note = {10.1007/978-3-642-31131-4_3},
    abstract = {Biotechnological improvements over the last decade has made it economically and technologically feasible to collect large DNA sequence data from many closely related species. This enables us to study the detailed evolutionary history of recent speciation and demographics. Sophisticated statistical methods are needed, however, to extract the information that DNA sequences hold, and a limiting factor in this is dealing with the large state space that the ancestry of large DNA sequences spans. Recently a new analysis method, CoalHMMs, has been developed, that makes it computationally feasible to scan full genome sequences – the complete genetic information of a species – and extract genetic histories from this. Applying this methodology, however, requires that the full state space of ancestral histories can be constructed. This is not feasible to do manually, but by applying formal methods such as Petri nets it is possible to build sophisticated evolutionary histories and automatically derive the analysis models needed. In this paper we describe how to use colored stochastic Petri nets to build CoalHMMs for complex demographic scenarios.},
    year = {2012}
    }
  • [PDF] [DOI] J. Nakatumba, M. Westergaard, and W. van der Aalst, “An Infrastructure for Cost-Effective Testing of Operational Support Algorithms Based on Colored Petri Nets,” in Application and Theory of Petri Nets, 2012, pp. 308-327.
    [Bibtex]
    @inproceedings{testsuite,
    author = {Nakatumba, Joyce and Westergaard, Michael and van der Aalst, Wil},
    affiliation = {Eindhoven University of Technology, The Netherlands},
    title = {An Infrastructure for Cost-Effective Testing of Operational Support Algorithms Based on Colored Petri Nets},
    booktitle = {Application and Theory of Petri Nets},
    series = {Lecture Notes in Computer Science},
    editor = {Haddad, Serge and Pomello, Lucia},
    publisher = {Springer Berlin / Heidelberg},
    isbn = {978-3-642-31130-7},
    keyword = {Computer Science},
    pages = {308-327},
    volume = {7347},
    url = {http://dx.doi.org/10.1007/978-3-642-31131-4_17},
    doi = {10.1007/978-3-642-31131-4_17},
    note = {10.1007/978-3-642-31131-4_17},
    abstract = {Operational support is a specific type of process mining that assists users while process instances are being executed. Examples are predicting the remaining processing time of a running insurance claim and recommending the action that minimizes the treatment costs of a particular patient. Whereas it is easy to evaluate prediction techniques using cross validation, the evaluation of recommendation techniques is challenging as the recommender influences the execution of the process. It is therefore impossible to simply use historic event data. Therefore, we present an approach where we use a colored Petri net model of user behavior to drive a real workflow system and real implementations of operational support, thereby providing a way of evaluating algorithms for operational support before implementation and a costly test using real users. In this paper, we evaluate algorithms for operational support using different user models. We have implemented our approach using Access/CPN 2.0.},
    year = {2012}
    }
  • [DOI] M. Westergaard and F. Maggi, “Looking into the Future: Using Timed Automata to Provide A Priori Advice about Timed Declarative Process Models,” in On the Move to Meaningful Internet Systems: OTM 2012, 2012, pp. 250-267.
    [Bibtex]
    @inproceedings{timeddeclare,
    year={2012},
    isbn={978-3-642-33605-8},
    booktitle={On the Move to Meaningful Internet Systems: OTM 2012},
    volume={7565},
    series={Lecture Notes in Computer Science},
    editor={Meersman, Robert and Panetto, Hervé and Dillon, Tharam and Rinderle-Ma, Stefanie and Dadam, Peter and Zhou, Xiaofang and Pearson, Siani and Ferscha, Alois and Bergamaschi, Sonia and Cruz, IsabelF.},
    doi={10.1007/978-3-642-33606-5_16},
    title={Looking into the Future: Using Timed Automata to Provide A Priori Advice about Timed Declarative Process Models},
    url={http://dx.doi.org/10.1007/978-3-642-33606-5_16},
    publisher={Springer Berlin Heidelberg},
    keywords={declarative process modeling; metric temporal logic; error detection; operational support; timed automata; Declare},
    author={Westergaard, Michael and Maggi, FabrizioMaria},
    pages={250-267}
    }

2011

  • [PDF] [DOI] F. Maggi, M. Montali, M. Westergaard, and W. van der Aalst, “Monitoring Business Constraints with Linear Temporal Logic: An Approach Based on Colored Automata,” in Business Process Management, 2011, pp. 132-147.
    [Bibtex]
    @inproceedings{colored-automata,
    author = {Maggi, Fabrizio and Montali, Marco and Westergaard, Michael and van der Aalst, Wil},
    affiliation = {Eindhoven University of Technology, The Netherlands},
    title = {Monitoring Business Constraints with Linear Temporal Logic: An Approach Based on Colored Automata},
    booktitle = {Business Process Management},
    series = {Lecture Notes in Computer Science},
    editor = {Rinderle-Ma, Stefanie and Toumani, Farouk and Wolf, Karsten},
    publisher = {Springer Berlin / Heidelberg},
    isbn = {978-3-642-23058-5},
    keyword = {Computer Science},
    pages = {132-147},
    volume = {6896},
    url = {http://dx.doi.org/10.1007/978-3-642-23059-2_13},
    doi = {10.1007/978-3-642-23059-2_13},
    note = {10.1007/978-3-642-23059-2_13},
    abstract = {Today’s information systems record real-time information about business processes. This enables the monitoring of business constraints at runtime. In this paper, we present a novel runtime verification framework based on linear temporal logic and colored automata. The framework continuously verifies compliance with respect to a predefined constraint model. Our approach is able to provide meaningful diagnostics even after a constraint is violated. This is important as in reality people and organizations will deviate and in many situations it is not desirable or even impossible to circumvent constraint violations. As demonstrated in this paper, there are several approaches to recover after the first constraint violation. Traditional approaches that simply check constraints are unable to recover after the first violation and still foresee (inevitable) future violations. The framework has been implemented in the process mining tool ProM.},
    year = {2011}
    }
  • [PDF] [DOI] M. Westergaard, “Better Algorithms for Analyzing and Enacting Declarative Workflow Languages Using LTL,” in Business Process Management, 2011, pp. 83-98.
    [Bibtex]
    @inproceedings{improved-translation,
    author = {Westergaard, Michael},
    affiliation = {Department of Mathematics and Computer Science, Eindhoven University of Technology, The Netherlands},
    title = {Better Algorithms for Analyzing and Enacting Declarative Workflow Languages Using LTL},
    booktitle = {Business Process Management},
    series = {Lecture Notes in Computer Science},
    editor = {Rinderle-Ma, Stefanie and Toumani, Farouk and Wolf, Karsten},
    publisher = {Springer Berlin / Heidelberg},
    isbn = {978-3-642-23058-5},
    keyword = {Computer Science},
    pages = {83-98},
    volume = {6896},
    url = {http://dx.doi.org/10.1007/978-3-642-23059-2_10},
    doi = {10.1007/978-3-642-23059-2_10},
    note = {10.1007/978-3-642-23059-2_10},
    abstract = {Declarative workflow languages are easy for humans to understand and use for specifications, but difficult for computers to check for consistency and use for enactment. Therefore, declarative languages need to be translated to something a computer can handle. One approach is to translate the declarative language to linear temporal logic (LTL), which can be translated to finite automata. While computers are very good at handling finite automata, the translation itself is often a road block as it may take time exponential in the size of the input. Here, we present algorithms for doing this translation much more efficiently (around a factor of 10,000 times faster and handling 10 times larger systems on a standard computer), making declarative specifications scale to realistic settings.},
    year = {2011}
    }
  • [PDF] [DOI] M. Westergaard and F. M. Maggi, “Modeling and Verification of a Protocol for Operational Support Using Coloured Petri Nets,” in Applications and Theory of Petri Nets, 2011, pp. 169-188.
    [Bibtex]
    @inproceedings{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

  • [PDF] [DOI] L. M. Kristensen and M. Westergaard, “Automatic Structure-Based Code Generation from Coloured Petri Nets: A Proof of Concept,” in Formal Methods for Industrial Critical Systems, 2010, pp. 215-230.
    [Bibtex]
    @inproceedings{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

  • [PDF] 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

  • [PDF] [DOI] M. Westergaard, L. M. Kristensen, G. S. Brodal, and L. Arge, “The ComBack Method – Extending Hash Compaction with Backtracking,” in Petri Nets and Other Models of Concurrency – ICATPN 2007, 2007, pp. 445-464.
    [Bibtex]
    @inproceedings{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

  • [PDF] [DOI] L. M. Kristensen, M. Westergaard, and P. C. Nørgaard, “Model-Based Prototyping of an Interoperability Protocol for Mobile Ad-Hoc Networks,” in Integrated Formal Methods, 2005, pp. 266-286.
    [Bibtex]
    @inproceedings{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

  • [PDF] [DOI] T. Mailund and M. Westergaard, “Obtaining Memory-Efficient Reachability Graph Representations Using the Sweep-Line Method,” in Tools and Algorithms for the Construction and Analysis of Systems, 2004, pp. 177-191.
    [Bibtex]
    @inproceedings{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}
    }
”Tools”
❗ These are all reviewed tool papers published at conferences. ❗

2013

  • [PDF] [DOI] M. Westergaard, “CPN Tools 4: Multi-formalism and Extensibility,” in Application and Theory of Petri Nets and Concurrency, J. Colom and J. Desel, Eds., Springer Berlin Heidelberg, 2013, vol. 7927, pp. 400-409.
    [Bibtex]
    @incollection{cpntools4,
    year={2013},
    isbn={978-3-642-38696-1},
    booktitle={Application and Theory of Petri Nets and Concurrency},
    volume={7927},
    series={Lecture Notes in Computer Science},
    editor={Colom, José-Manuel and Desel, Jörg},
    doi={10.1007/978-3-642-38697-8_22},
    title={CPN Tools 4: Multi-formalism and Extensibility},
    url={http://dx.doi.org/10.1007/978-3-642-38697-8_22},
    publisher={Springer Berlin Heidelberg},
    author={Westergaard, Michael},
    pages={400-409}
    }
  • [PDF] M. Westergaard and C. Stahl, “Leveraging Super-Scalarity and Parallelism to Provide Fast Declare Mining without Restrictions,” in Proceedings of the BPM Demo sessions, 2013.
    [Bibtex]
    @InProceedings{megaminer,
    author = {Westergaard, Michael and Stahl, Christian},
    title = {Leveraging Super-Scalarity and Parallelism to Provide Fast Declare Mining without Restrictions},
    year =   2013,
    booktitle =   {Proceedings of the BPM Demo sessions},
    editor =   {Fauvet, Marie-Christine and van Dongen, Boudewijn },
    volume =   1021,
    series =   {CEUR Workshop Proceedings},
    ISSN =   {1613-0073},
    publisher =   {CEUR-WS.org},
    url =     {http://CEUR-WS.org/Vol-1021},
    urn =     {urn:nbn:de:0074-1021-10}
    }
  • [PDF] M. Westergaard and T. Slaats, “CPN Tools 4: A Process Modeling Tool Combining Declarative and Imperative Paradigms,” in Proceedings of the BPM Demo sessions, 2013.
    [Bibtex]
    @InProceedings{cpntools4bpm,
    author = {Westergaard, Michael and Slaats, Tijs},
    title = {CPN Tools 4: A Process Modeling Tool Combining Declarative and Imperative Paradigms},
    year =   2013,
    booktitle =   {Proceedings of the BPM Demo sessions},
    editor =   {Fauvet, Marie-Christine and van Dongen, Boudewijn },
    volume =   1021,
    series =   {CEUR Workshop Proceedings},
    ISSN =   {1613-0073},
    publisher =   {CEUR-WS.org},
    url =     {http://CEUR-WS.org/Vol-1021},
    urn =     {urn:nbn:de:0074-1021-3}
    }

2011

  • [PDF] M. Westergaard and F. M. Maggi, “Declare: A Tool Suite for Declarative Workflow Modeling and Enactment,” in Proceedings of the Demo Track of the Nineth Conference on Business Process Management, 2011.
    [Bibtex]
    @InProceedings{declare,
    author = {Westergaard, Michael and Maggi, Fabrizio Maria},
    title = {Declare: A Tool Suite for Declarative Workflow Modeling and Enactment},
    year =   2011,
    booktitle =   {Proceedings of the Demo Track of the Nineth Conference on Business Process Management},
    editor =   {Ludwig, Heiko and Reijers, Hajo},
    volume =   820,
    series =   {CEUR Workshop Proceedings},
    ISSN =   {1613-0073},
    publisher =   {CEUR-WS.org},
    url =     {http://CEUR-WS.org/Vol-820},
    urn =     {urn:nbn:de:0074-820-4}
    }
  • [PDF] [DOI] M. Westergaard, “Access/CPN 2.0: A High-Level Interface to Coloured Petri Net Models,” in Applications and Theory of Petri Nets, L. M. Kristensen and L. Petrucci, Eds., 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

  • [PDF] [DOI] M. Westergaard and L. M. Kristensen, “The Access/CPN Framework: A Tool for Interacting with the CPN Tools Simulator,” in Applications and Theory of Petri Nets, G. Franceschinis and K. Wolf, Eds., 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}
    }
  • [PDF] [DOI] M. Westergaard, S. Evangelista, and L. M. Kristensen, “ASAP: An Extensible Platform for State Space Analysis,” in Applications and Theory of Petri Nets, G. Franceschinis and K. Wolf, Eds., 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

  • [PDF] [DOI] M. Westergaard and K. Lassen, “The BRITNeY Suite Animation Tool,” in Petri Nets and Other Models of Concurrency – ICATPN 2006, S. Donatelli and P. Thiagarajan, Eds., 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

  • [PDF] [DOI] 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,” in Applications and Theory of Petri Nets 2003, W. van der Aalst and E. Best, Eds., 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}
    }
”Workshops”
❗ These are all reviewed papers published at workshops. ❗

2013

  • [DOI] W. Aalst, M. Westergaard, and H. Reijers, “Beautiful Workflows: A Matter of Taste?,” in The Beauty of Functional Code, 2013, pp. 211-233.
    [Bibtex]
    @InProceedings{bpmconcepts,
    year={2013},
    isbn={978-3-642-40354-5},
    booktitle={The Beauty of Functional Code},
    volume={8106},
    series={Lecture Notes in Computer Science},
    editor={Achten, Peter and Koopman, Pieter},
    doi={10.1007/978-3-642-40355-2_15},
    title={Beautiful Workflows: A Matter of Taste?},
    url={http://dx.doi.org/10.1007/978-3-642-40355-2_15},
    publisher={Springer Berlin Heidelberg},
    keywords={Workflow Management; Business Process Management; Case Handling; Declarative Languages; Functional Programming},
    author={Aalst, WilM.P. and Westergaard, Michael and Reijers, HajoA.},
    pages={211-233}
    }

2012

  • [PDF] [DOI] J. Nakatumba, M. Westergaard, and W. M. P. Aalst, “Generating Event Logs with Workload-Dependent Speeds from Simulation Models,” in Advanced Information Systems Engineering Workshops, 2012, pp. 383-397.
    [Bibtex]
    @inproceedings{loggeneration,
    author = {Nakatumba, Joyce and Westergaard, Michael and Aalst, Wil M. P.},
    affiliation = {Eindhoven University of Technology, The Netherlands},
    title = {Generating Event Logs with Workload-Dependent Speeds from Simulation Models},
    booktitle = {Advanced Information Systems Engineering Workshops},
    series = {Lecture Notes in Business Information Processing},
    editor = {Bajec, Marko and Eder, Johann and Aalst, Wil and Mylopoulos, John and Rosemann, Michael and Shaw, Michael J. and Szyperski, Clemens and Aalst, Wil and Mylopoulos, John and Rosemann, Michael and Shaw, Michael J. and Szyperski, Clemens},
    publisher = {Springer Berlin Heidelberg},
    isbn = {978-3-642-31069-0},
    keyword = {Computer Science},
    pages = {383-397},
    volume = {112},
    url = {http://dx.doi.org/10.1007/978-3-642-31069-0_31},
    doi = {10.1007/978-3-642-31069-0_31},
    note = {10.1007/978-3-642-31069-0_31},
    abstract = {Both simulation and process mining can be used to analyze operational business processes. Simulation is model-driven and very useful because different scenarios can be explored by changing the model’s parameters. Process mining is driven by event data. This allows detailed analysis of the observed behavior showing actual bottlenecks, deviations, and other performance-related problems. Both techniques tend to focus on the control-flow and do not analyze resource behavior in a detailed manner. In this paper, we focus on workload-dependent processing speeds because of the well-known phenomenon that people perform best at a certain stress level. For example, the “Yerkes-Dodson Law of Arousal” states that people will take more time to execute an activity if there is little work to do. This paper shows how workload-dependent processing speeds can be incorporated in a simulation model and learned from event logs. We also show how event logs with workload-dependent behavior can be generated through simulation. Experiments show that it is crucial to incorporate such phenomena. Moreover, we advocate an amalgamation of simulation and process mining techniques to better understand, model, and improve real-life business processes.},
    year = {2012}
    }
  • [PDF] M. Westergaard, D. Fahland, and C. Stahl, “Grade/CPN: Semi-automatic Support for Teaching Petri Nets by Checking Many Petri Nets Against One Specification,” in Petri Nets and Software Engineering. International Workshop, PNSE’12, 2012, pp. 32-46.
    [Bibtex]
    @InProceedings{gradecpn,
    title =   {Grade/CPN: Semi-automatic Support for Teaching Petri Nets by Checking Many Petri Nets Against One Specification},
    pages =   {32-46},
    author =   {Westergaard, Michael and Fahland, Dirk and
    Stahl, Christian},
    year =   2012,
    booktitle =   {Petri Nets and Software Engineering.  International Workshop, PNSE'12},
    editor =   {Cabac, Lawrence and Duvigneau, Michael and Moldt, Daniel},
    volume =   851,
    series =   {CEUR Workshop Proceedings},
    ISSN =   {1613-0073},
    publisher =   {CEUR-WS.org},
    url =     {http://CEUR-WS.org/Vol-851},
    urn =     {urn:nbn:de:0074-851-7}
    }

2011

  • [PDF] M. Westergaard and H. M. W. Verbeek, “Efficient Implementation of Prioritized Transitions for High-level Petri Nets,” in Petri Nets and Software Engineering. International Workshop PNSE’11, 2011, pp. 27-41.
    [Bibtex]
    @InProceedings{priority,
    author =   {Westergaard, Michael and Verbeek, H. M. W.},
    title =   {Efficient Implementation of Prioritized Transitions for High-level {Petri} Nets},
    pages =   {27-41},
    booktitle =   {{Petri} Nets and Software Engineering. International Workshop PNSE'11},
    editor =   {Duvigneau, Michael and Moldt, Daniel and Hiraishi, Kunihiko},
    month =    jun,
    year =    2011,
    volume =    723,
    series =    {CEUR Workshop Proceedings},
    ISSN =    {1613-0073},
    publisher =    {CEUR-WS.org},
    url =    {http://CEUR-WS.org/Vol-723},
    urn =    {urn:nbn:de:0074-723-C}
    abstract =    {Transition priorities can be a useful mechanism when
    modeling using Petri nets.  For example, high-priority
    transitions can be used to model exception handling and
    low-priority transitions can be used to model background
    tasks that should only be executed when no other
    transition is enabled.  Transition priorities can be
    simulated in Petri nets using, e.\,g., inhibitor arcs,
    but such constructs tend to unnecessarily clutter models,
    making it useful to support priorities directly.
    
    Computing the enabling of transitions in high-level Petri
    nets is an expensive operation and should be avoided.  As
    transition priorities introduce a nonlocal enabling
    condition, at first sight this forces us to compute
    enabling for all transitions in a highest-priority-first
    order, but it is possible to do better.  Here we describe
    our implementation of transition priorities in CPN Tools
    3.0, where we minimize the number of enabling
    computations.  We describe algorithms for executing
    transitions at random, useful for automatic simulation
    without user interactions, and for maintaining a set of
    known enabled transitions, useful for interactive
    user-guided simulation.  Experiments show that using our
    algorithms we can execute $4-7$ million transitions a
    minute for real-life models and more than $20$ million
    transitions a minute for other models, a significant
    improvement over the $1-5$ million transitions a minute
    possible for simpler algorithms.}
    }
  • [PDF] M. Westergaard, “Towards Verifying Parallel Algorithms and Programs using Coloured Petri Nets,” in Petri Nets and Software Engineering. International Workshop PNSE’11, 2011, pp. 57-71.
    [Bibtex]
    @InProceedings{parallel-algorithms,
    author =   {Westergaard, Michael},
    title =   {Towards Verifying Parallel Algorithms and Programs using Coloured {Petri} Nets},
    pages =   {57-71},
    booktitle =   {{Petri} Nets and Software Engineering. International Workshop PNSE'11},
    editor =   {Duvigneau, Michael and Moldt, Daniel and Hiraishi, Kunihiko},
    month =    jun,
    year =    2011,
    volume =    723,
    series =    {CEUR Workshop Proceedings},
    ISSN =    {1613-0073},
    publisher =    {CEUR-WS.org},
    url =    {http://CEUR-WS.org/Vol-723},
    urn =    {urn:nbn:de:0074-723-C}
    abstract =    {Coloured Petri nets have proved to be a useful formalism
    for modeling distributed algorithms, i.e., algorithms
    where nodes communicate via message passing.  Here we
    describe an approach for modeling parallel algorithms and
    programs, i.e., algorithms and programs where processes
    communicate via shared memory.  The model is verified for
    correctness, here to prove absence of mutual exclusion
    violations and to find dead- and live-locks.  The
    approach can be used in a model-driven development
    approach, where code is generated from a model, in a
    model-extraction approach, where a model is extracted
    from running code, or using a combination of the two,
    supporting extracting a model from an abstract
    description and generation of correct implementation
    code.  We illustrate our idea by applying the technique
    to a parallel implementation of explicit state-space
    exploration.}
    }

2009

  • [PDF] K. L. Espensen, M. K. Kjeldsen, L. M. Kristensen, and M. Westergaard, “Towards Automatic Code-generation from Process-partitioned Coloured Petri Nets,” in Proc. of 10th CPN Workshop, 2009, pp. 41-60.
    [Bibtex]
    @InProceedings{codegenerationcpn,
    Author         = {Espensen, Kristian Leth and Kjeldsen, Mads Keblov and Kristensen, Lars Michael and Westergaard, Michael},
    Title          = {{Towards Automatic Code-generation from Process-partitioned Coloured Petri Nets}},
    BookTitle      = {{Proc. of 10th CPN Workshop}},
    Volume         = {590},
    Series         = {DAIMI-PB},
    Pages          = {41-60},
    year           = 2009,
    }
  • [PDF] M. Westergaard, L. M. Kristensen, and M. Kuusela, “A Prototype for Cosimulating SystemC and Coloured Petri Net Models,” in Proc. of 10th CPN Workshop, 2009, pp. 1-19.
    [Bibtex]
    @InProceedings{cosimulationcpn,
    Author         = {Westergaard, Michael and Kristensen, Lars Michael and Kuusela, Maija},
    Title          = {{A Prototype for Cosimulating SystemC and Coloured Petri Net Models}},
    BookTitle      = {{Proc. of 10th CPN Workshop}},
    Volume         = {590},
    Series         = {DAIMI-PB},
    Pages          = {1-19},
    year           = 2009,
    }

2008

  • [PDF] S. Evagelista, M. Westergaard, and L. M. Kristensen, “The ComBack Method Revisited: Caching Strategies and Extension with Delayed Duplicate Detection,” in Proc. of 9th CPN Workshop, 2008, pp. 63-82.
    [Bibtex]
    @InProceedings{combackrevisited,
    Author         = {Evagelista, Sami and Westergaard, Michael and Kristensen, Lars Michael},
    Title          = {{The ComBack Method Revisited: Caching Strategies and Extension with Delayed Duplicate Detection}},
    BookTitle      = {{Proc. of 9th CPN Workshop}},
    Volume         = {588},
    Series         = {DAIMI-PB},
    Pages          = {63-82},
    year           = 2008,
    }
  • [PDF] M. Westergaard and L. M. Kristensen, “JoSEL: A Job Specification and Execution Language for Model Checking,” in Proc. of 9th CPN Workshop, 2008, pp. 7-26.
    [Bibtex]
    @InProceedings{joselcpn,
    Author         = {Westergaard, Michael and Kristensen, Lars Michael},
    Title          = {{JoSEL: A Job Specification and Execution Language for Model Checking}},
    BookTitle      = {{Proc. of 9th CPN Workshop}},
    Volume         = {588},
    Series         = {DAIMI-PB},
    Pages          = {7-26},
    year           = 2008,
    }
  • [PDF] M. Westergaard and L. M. Kristensen, “Two Interfaces to the CPN Tools Simulator,” in Proc. of 9th CPN Workshop, 2008, pp. 83-102.
    [Bibtex]
    @InProceedings{siminterface,
    Author         = {Westergaard, Michael and Kristensen, Lars Michael},
    Title          = {{Two Interfaces to the CPN Tools Simulator}},
    BookTitle      = {{Proc. of 9th CPN Workshop}},
    Volume         = {588},
    Series         = {DAIMI-PB},
    Pages          = {83-102},
    year           = 2008,
    }

2007

  • [PDF] M. Westergaard, “A Game-theoretic View on Behavioural Visualisation,” in Proc. of 2nd International Workshop on Formal Methods for Interactive Systems, 2007.
    [Bibtex]
    @InProceedings{gameanimation,
    Author         = {Westergaard, Michael},
    Title          = {{A Game-theoretic View on Behavioural Visualisation}},
    BookTitle      = {{Proc. of 2nd International Workshop on Formal Methods for Interactive Systems}},
    year           = 2007,
    }

2006

  • [PDF] M. Westergaard, “The BRITNeY Suite: A Platform for Experiments,” in Proc. of 7th CPN Workshop, 2006, pp. 97-116.
    [Bibtex]
    @InProceedings{platform,
    Author         = {Westergaard, Michael},
    Title          = {{The BRITNeY Suite: A Platform for Experiments}},
    BookTitle      = {{Proc. of 7th CPN Workshop}},
    Volume         = {579},
    Series         = {DAIMI-PB},
    Pages          = {97-116},
    year           = 2006,
    }
  • [PDF] M. Westergaard, “Game Coloured Petri Nets,” in Proc. of 7th CPN Workshop, 2006, pp. 281-300.
    [Bibtex]
    @InProceedings{gcpn,
    Author         = {Westergaard, Michael},
    Title          = {{Game Coloured Petri Nets}},
    BookTitle      = {{Proc. of 7th CPN Workshop}},
    Volume         = {579},
    Series         = {DAIMI-PB},
    Pages          = {281-300},
    year           = 2006,
    }

2005

  • [PDF] M. Westergaard and K. B. Lassen, “Building and Deploying Visualizations of Coloured Petri Net Models Using BRITNeY animation and CPN Tools,” in Proc. of 6th CPN Workshop, 2005, pp. 119-136.
    [Bibtex]
    @InProceedings{techbritney,
    Author         = {Westergaard, Michael and Lassen, Kristian Bisgaard},
    Title          = {{Building and Deploying Visualizations of Coloured Petri Net Models Using BRITNeY animation and CPN Tools}},
    BookTitle      = {{Proc. of 6th CPN Workshop}},
    Volume         = {576},
    Series         = {DAIMI-PB},
    Pages          = {119-136},
    year           = 2005,
    }

2004

  • [PDF] M. Westergaard, “Towards a High-level Petri Net Type Definition,” in Proc. Workshop on the Definition, Implementation and Application of a Standard Interchange Format for Petri Nets, 2004.
    [Bibtex]
    @InProceedings{hlpn,
    Author         = {Westergaard, Michael},
    Title          = {{Towards a High-level Petri Net Type Definition}},
    BookTitle      = {{Proc. Workshop on the Definition, Implementation and Application of a Standard Interchange Format for Petri Nets}},
    year           = 2004,
    }

2002

  • [PDF] M. Westergaard, “Supporting Multiple Pointing Devices in Microsoft Windows,” in Proc. Microsoft Summer Workshop for Faculty and PhDs, 2002.
    [Bibtex]
    @InProceedings{mouse,
    Author         = {Westergaard, Michael},
    Title          = {{Supporting Multiple Pointing Devices in Microsoft Windows}},
    BookTitle      = {{Proc. Microsoft Summer Workshop for Faculty and PhDs}},
    year           = 2002,
    }
”Theses”
  • [PDF] M. Westergaard, “Looking Good, Behaving Well – Behavioural Verification and Visualisation of Formal Models of Concurrent Systems,” PhD Thesis, 2007.
    [Bibtex]
    @PhDThesis{thesis,
      author = {Westergaard, Michael},
      title = {Looking Good, Behaving Well – Behavioural Verification and Visualisation of Formal Models of Concurrent Systems},
      school = {Department of Computer Science, University of Aarhus, Denmark},
      year = 2007,
      pdf = {http://westergaard.eu/cv/thesis/},
      month = July,
    }
  • [PDF] M. Westergaard, “Building Verifiable Software Prototypes Using Coloured Petri Nets,” Master Thesis, 2005.
    [Bibtex]
    @MastersThesis{progress,
      author = {Westergaard, Michael},
      title = {Building Verifiable Software Prototypes Using Coloured Petri Nets},
      school = {Department of Computer Science, University of Aarhus, Denmark},
      year = 2005,
      month = June,
    }
”Technical

2013

  • [PDF] R. Müller, C. Stahl, W. M. P. van der Aalst, and M. Westergaard, “Service Discovery from Observed Behavior While Guaranteeing Deadlock Freedom in Collaborations,” BPM Center Report, BPM-13-05, 2013.
    [Bibtex]
    @techreport{servicetech,
    author = {Müller, Richard and Stahl, Christian and van der Aalst, Wil M. P. and Westergaard, Michael},
    title = {Service Discovery from Observed Behavior While Guaranteeing Deadlock Freedom in Collaborations},
    institution = {BPM Center Report},
    number = {BPM-13-05},
    year = 2013,
    }
  • [PDF] M. Westergaard, C. Stahl, and H. A. Reijers, “UnconstrainedMiner: Efficient Discovery of Generalized Declarative Process Models,” BPM Center Report, BPM-13-28, 2013.
    [Bibtex]
    @techreport{megaminertech,
    author =   {Westergaard, Michael and Stahl, Christian and Reijers, Hajo A.},
    title = {UnconstrainedMiner: Efficient Discovery of Generalized Declarative Process Models},
    institution = {BPM Center Report},
    number = {BPM-13-28},
    year = 2013,
    }
  • [PDF] M. Westergaard and B. F. van Dongen, “KeyValueSets: Event Logs Revisited,” BPM Center Report, BPM-13-25, 2013.
    [Bibtex]
    @techreport{keyvaluetech,
    author =   {Westergaard, Michael and van Dongen, Bioudewijn F.},
    title = {KeyValueSets: Event Logs Revisited},
    institution = {BPM Center Report},
    number = {BPM-13-25},
    year = 2013,
    }
  • [PDF] M. Westergaard and H. M. W. Verbeek, “Efficient Implementation of Simulation of Prioritized Transitions for High-level Petri Nets,” BPM Center Report, BPM-13-24, 2013.
    [Bibtex]
    @techreport{prioritytech,
    author =   {Westergaard, Michael and Verbeek, H. M. W.},
    title = {Efficient Implementation of Simulation of Prioritized Transitions for High-level Petri Nets},
    institution = {BPM Center Report},
    number = {BPM-13-24},
    year = 2013,
    }

2012

  • [PDF] [DOI] W. Aalst and et al., “Process Mining Manifesto,” in Business Process Management Workshops, 2012, pp. 169-194.
    [Bibtex]
    @inproceedings{manifesto,
    author = {Aalst, Wil and et al.},
    xauthor = {Aalst, Wil and Adriansyah, Arya and Medeiros, Ana Karla Alves and Arcieri, Franco and Baier, Thomas and Blickle, Tobias and Bose, Jagadeesh Chandra and Brand, Peter and Brandtjen, Ronald and Buijs, Joos and Burattin, Andrea and Carmona, Josep and Castellanos, Malu and Claes, Jan and Cook, Jonathan and Costantini, Nicola and Curbera, Francisco and Damiani, Ernesto and Leoni, Massimiliano and Delias, Pavlos and Dongen, Boudewijn F. and Dumas, Marlon and Dustdar, Schahram and Fahland, Dirk and Ferreira, Diogo R. and Gaaloul, Walid and Geffen, Frank and Goel, Sukriti and Günther, Christian and Guzzo, Antonella and Harmon, Paul and Hofstede, Arthur and Hoogland, John and Ingvaldsen, Jon Espen and Kato, Koki and Kuhn, Rudolf and Kumar, Akhil and Rosa, Marcello and Maggi, Fabrizio and Malerba, Donato and Mans, Ronny S. and Manuel, Alberto and McCreesh, Martin and Mello, Paola and Mendling, Jan and Montali, Marco and Motahari-Nezhad, Hamid R. and Muehlen, Michael and Munoz-Gama, Jorge and Pontieri, Luigi and Ribeiro, Joel and Rozinat, Anne and Seguel Pérez, Hugo and Seguel Pérez, Ricardo and Sepúlveda, Marcos and Sinur, Jim and Soffer, Pnina and Song, Minseok and Sperduti, Alessandro and Stilo, Giovanni and Stoel, Casper and Swenson, Keith and Talamo, Maurizio and Tan, Wei and Turner, Chris and Vanthienen, Jan and Varvaressos, George and Verbeek, Eric and Verdonk, Marc and Vigo, Roberto and Wang, Jianmin and Weber, Barbara and Weidlich, Matthias and Weijters, Ton and Wen, Lijie and Westergaard, Michael and Wynn, Moe},
    affiliation = {Eindhoven University of Technology, The Netherlands},
    title = {Process Mining Manifesto},
    booktitle = {Business Process Management Workshops},
    series = {Lecture Notes in Business Information Processing},
    editor = {Daniel, Florian and Barkaoui, Kamel and Dustdar, Schahram and Aalst, Wil and Mylopoulos, John and Rosemann, Michael and Shaw, Michael J. and Szyperski, Clemens},
    publisher = {Springer Berlin Heidelberg},
    isbn = {978-3-642-28108-2},
    keyword = {Computer Science},
    pages = {169-194},
    volume = {99},
    url = {http://dx.doi.org/10.1007/978-3-642-28108-2_19},
    doi = {10.1007/978-3-642-28108-2_19},
    note = {10.1007/978-3-642-28108-2_19},
    abstract = {Process mining techniques are able to extract knowledge from event logs commonly available in today’s information systems. These techniques provide new means to discover, monitor, and improve processes in a variety of application domains. There are two main drivers for the growing interest in process mining. On the one hand, more and more events are being recorded, thus, providing detailed information about the history of processes. On the other hand, there is a need to improve and support business processes in competitive and rapidly changing environments. This manifesto is created by the IEEE Task Force on Process Mining and aims to promote the topic of process mining. Moreover, by defining a set of guiding principles and listing important challenges, this manifesto hopes to serve as a guide for software developers , scientists , consultants , business managers , and end-users . The goal is to increase the maturity of process mining as a new tool to improve the (re)design, control, and support of operational business processes.},
    year = {2012}
                   }
  • [PDF] J. Nakatumba, M. Westergaard, and W. M. P. van der Aalst, “A Meta-model for Operational Support,” BPM Center Report, BPM-12-05, 2012.
    [Bibtex]
    @techreport{metamodeltech,
    author = {Nakatumba, Joyce and Westergaard, Michael and van der Aalst, Wil M. P.},
    title = {A Meta-model for Operational Support},
    institution = {BPM Center Report},
    number = {BPM-12-05},
    year = 2012,
    }

2008

  • [PDF] M. Westergaard and S. Evagelista, “The ASAP Platform: Next Generation Tool Support for State Space Analysis of CPN Models,” in Proc. of 9th CPN Workshop, 2008, pp. 1-2.
    [Bibtex]
    @InProceedings{asaptutorial,
    Author         = {Westergaard, Michael and Evagelista, Sami},
    Title          = {{The ASAP Platform: Next Generation Tool Support for State Space Analysis of CPN Models}},
    BookTitle      = {{Proc. of 9th CPN Workshop}},
    Volume         = {588},
    Series         = {DAIMI-PB},
    Pages          = {1-2},
    year           = 2008,
    }

2007

  • [PDF] L. M. Kristensen and M. Westergaard, “The ASCoVeCo State Space Analysis Platform: Next Generation Tool Support for State Space Analysis,” in Proc. of 8th CPN Workshop, 2007, pp. 1-6.
    [Bibtex]
    @InProceedings{asapcpn,
    Author         = {Kristensen, Lars Michael and Westergaard, Michael},
    Title          = {{The ASCoVeCo State Space Analysis Platform: Next Generation Tool Support for State Space Analysis}},
    BookTitle      = {{Proc. of 8th CPN Workshop}},
    Volume         = {584},
    Series         = {DAIMI-PB},
    Pages          = {1-6},
    year           = 2007,
    }

2006

  • [PDF] K. B. Lassen and M. Westergaard, “Embedding Java Types in CPN Tools,” Department of Computer Science, University of Aarhus, Denmark 2006.
    [Bibtex]
    @techreport{types,
      author = {Lassen, Kristian Bisgaard and Westergaard, Michael},
      title = {Embedding Java Types in CPN Tools},
      year = 2006,
      institution = {Department of Computer Science, University of Aarhus, Denmark},
    }
”Slides”

L.M. Kristensen and M. Westergaard

State space exploration of Coloured Petri Nets and the ASAP model checking platform

  • Part 1: Introduction [PDF]
  • Part 2: User perspective [PDF, MOV]
  • Part 3: Advanced methods [PDF]
  • Part 4: Research perspective [PDF, MOV]

Slides from tutorial at the Petri net confenrence. Braga, Portugal, June 2010.

M. Westergaard

Stuff About CPN Tools [PDF with builds, PDF]

Slides from presentation of the structure of CPN Tools. Eindhoven, Holland, April 2010.

M. Westergaard

Routing Protocols in Mobile Ad-hoc Networks [Keynote, PDF]

Slides from University of Aarhus course “Advanced Behaviour Modelling”. Aarhus, Denmark, November 2006.

M. Westergaard

Routing Protocols in Mobile Ad-hoc Networks [Keynote, PDF]

Slides from IT University of Copenhagen PhD School “Verification of Protocols for Security and Mobility”. Copenhagen, Denmark, October 2006.

M. Westergaard

Routing Protocols in Mobile Ad-hoc Networks [PDF]

Slides from University of Aarhus undergraduate course “Computer Science – in perspective”. Århus, Denmark, September 2006.

M. Westergaard

Looking good, behaving well [Keynote, PDF]

Slides from Brics Seminar. Aalborg, Denmark, February 2006.

M. Westergaard

Routing Protocols in Mobile Ad-hoc Networks [PDF]

Slides from University of Aarhus undergraduate course “Computer Science – in perspective”. Århus, Denmark, September 2005.

M. Westergaard

Petri-net Based Animation with CPN Tools and BRITNeY animation [PDF]

Slides from Tutorial on CPN Tools at Fifth Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools. Århus, Denmark, October 2004.