Stephan Merz — recent talks

Refinement of events with permissions and obligations

Proposal of an extension of event systems by fairness conditions, obligations, interdictions, and permissions. The latter "deontic" properties are relevant in connection with work on information security (more specifically, access control). Whereas there are frameworks to represent such concepts, few formal development methods reflect them in their notions of correctness and refinement.

Modeling and Developing Systems Using TLA+

Material for a course on the TLA+ specification language, including the TLC model checker, given at a summer school in Rio Cuarto, Argentina.

Automata and temporal logics - a biased overview

Contains a tutorial presentation of the classical automata-theoretic framework for model checking, targeted towards a public familiar with modal logic. Also presents alternating automata for linear and (very briefly) for branching time. The talk was given at the M4M 2003 workshop at LORIA in Nancy.

Model Checking UML Statecharts and Collaborations

An overview of the state of the Hugo project as of december, 2002. The talk was given at a UML theme day organized in Turku, Finland, following a similar talk given in October 2002 at the CSDUML workshop at Dresden, Germany.

Towards Specification and Refinement of Mobile Systems

Describes ongoing joint work with Martin Wirsing and Júlia Zappe to extend Lamport's TLA for the specification of mobile agent systems. This talk was given at a theme day on temporal logic within the QSL project at LORIA.

Model Checking

with Javier Esparza

A 6-hour tutorial covering basic model checking techniques as well as some more advanced topics (abstraction, infinite-state model checking). The talk was given at the Petri Net Conference 2001.

Here comes the time warp:  Javier gave the same tutorial at the same conference a year later (though at the other end of the world)!