Presentations

This page contains complete listings of Prof. Lüttgen's presentations at conferences and workshops, as well as of invited presentations.

Paper Presentations

Richer Interface Automata with Optimistic and Pessimistic Compatibility. 13th Intl. Workshop on Automated Verification of Critical Systems (AVoCS 2013), Guildford, England, September 2013. Slides.
Heterogeneous Specification Using State Machines and Temporal Logic. 16. Kolloquium Programmiersprachen und Grundlagen der Programmierung (KPS 2011), Schloss Raesfeld, Germany, September 2011. Slides.
Safe reasoning with Logic LTS. 24th British Colloquium for Theoretical Computer Science (BCTCS 2008), Durham, England, April 2008. Slides.
Introducing the CoSta project: Contractual Statecharts. 14th Intl. Open Workshop on Synchronous Programming (SYNCHRON 2007), Bamberg, Germany, November 2007. Slides.
Ready simulation for concurrency: It's Logical! 34th Intl. Colloquium on Automata, Languages and Programming (ICALP 2007), Wroclaw, Poland, July 2007. Slides.
Conjunction on processes: Full-abstraction via ready-tree semantics. 9th Intl. Conf. on Foundations of Software Science and Computation Structures (FOSSACS 2006), Vienna, Austria, March 2006. Slides.
Bisimulation on speed: A unified approach. 8th Intl. Conf. on Foundations of Software Science and Computation Structures (FOSSACS 2005), Edinburgh, Scotland, April 2005. Slides.
Bisimulation on speed: Lower time bounds. 7th Intl. Conf. on Foundations of Software Science and Computation Structures (FOSSACS 2004), Barcelona, Spain, April 2004. Slides.
Axiomatizing an algebra of step reactions for synchronous languages. 13th Intl. Conf. on Concurrency Theory (CONCUR 2002), Brno, Czech Republic, August 2002. Slides.
A logical process calculus. 9th Intl. Workshop on Expressiveness in Concurrency (EXPRESS 2002), Brno, Czech Republic, August 2002. Slides.
Fully-abstract Statecharts semantics via intuitionistic Kripke models. 27th Intl. Colloquium on Automata, Languages and Programming (ICALP 2000), Geneva, Switzerland, July 2000. Slides.
Analyzing mode confusion via model checking. Intl. Workshop on Theoretical and Practical Aspects of SPIN Model Checking (SPIN '99), Toulouse, France, September 1999.
An algebraic theory of multiple clocks. 8th Intl. Conf. on Concurrency Theory (CONCUR '97), Warsaw, Poland, July 1997. Slides.
A process algebra with distributed priorities. 7th Intl. Conf. on Concurrency Theory (CONCUR '96), Pisa, Italy, August 1996. Slides.
Priorities for modeling and verifying distributed systems. 2nd Intl. Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '96), Passau, Germany, March 1996. Slides.

^ Top

Invited Presentations

DSI: Automated detection of dynamic data structures in C programs and binary code. NII Sohnan Meeting 100 on Analysis and Verification of Pointer Programs, Shonan, Japan, October 2017. Abstract / Slides.

This talk presents the key results of the DFG-funded research project "e;Learning Data Structure Behaviour from Executions of Pointer Programs"e; (DSI), in which dynamic analysis techniques have been developed to identify dynamic data structures in C programs and x86 binary code. DSI's analysis utilizes a novel memory abstraction that allows for a compact description of pointer-based data structures such as linked lists and binary trees, and their interconnections such as parent-child nesting. On top of this abstraction, an evidence-collecting approach calculates a natural language description of the observed data structures with the help of a systematic taxonomy. The inferred data structure information is not only helpful for program comprehension but can also be utilized in the contexts of software verification and visualization.
Modal Interface Automata. Institute of Software Engineering and Theoretical Computer Science, TU Berlin, Germany, July 2016. Abstract / Slides.

Interface theories are employed in the component-based design of concurrent systems. In this talk, I present the novel interface theory Modal Interface Automata (MIA), which has been developed in the context of a joint DFG-project with Walter Vogler at the University of Augsburg. MIA addresses several limitations of related work; in particular, MIA resolves the longstanding conflict between unspecified input events being allowed in IA but forbidden in MTS.
Modal Interface Automata. iMinds-DistriNet Research Group, Department of Computer Science, KU Leuven, Belgium, May 2016. Abstract / Slides.

Interface theories are employed in the component-based design of concurrent systems. Several modern theories have been built at the crossroads of de Alfaro and Henzinger's Interface Automata (IA) and Larsen's Modal Transition Systems (MTS), such as Nyman et al.'s IOMTS, Raclet et al.'s MI and Bauer et al.'s MIO. Unfortunately, all of them have shortcomings or restrictions regarding the (non-)monotonicity of interface refinement, the (non-)determinacy of interfaces and the employed notion of component compatibility, respectively, which limit their practical use for incremental system design.

In this talk, I present the novel interface theory Modal Interface Automata (MIA), which has been developed in the context of a joint DFG-project with Walter Vogler at the University of Augsburg. MIA addresses the above mentioned limitations of related work and, in particular, resolves the longstanding conflict between unspecified input events being allowed in IA but forbidden in MTS.
Heterogene Modellierungstechniken in der Softwareentwicklung. Talk at a leading technology company, Germany, April 2016. Abstract / Slides.

Bei der Spezifikation und dem Entwurf komplexer Software werden in zunehmenden Maße heterogene Notationen eingesetzt, die deklarativ-logische und operationelle Paradigmen miteinander verbinden, um eine prägnante Beschreibung von Entwurfsspielräumen und Produktvariabilitäten zu ermöglichen. Ein Beispiel hierfür ist die Unified Modeling Language (UML), die dem Modellierer u.a. Klassendiagramme, Zustandsmaschinen und die Object Constraint Language zur Verfügung stellt. Auch bei der modellgetriebenen Entwicklung eingebetteter Software werden ähnliche Ansätze verfolgt, um etwa Statecharts mit logischen Zusicherungen zu annotieren.

In diesem Vortrag werde ich über Ideen, Lösungsansätze und Ergebnisse berichten, die im Rahmen eines aktuellen DFG-Forschungsprojekts zu derartig heterogenen Modellierungstechniken an meinem Lehrstuhl entstanden sind. Im Zentrum unserer Untersuchungen stehen dabei sog. Interface-Theorien, welche ein schrittweises, kompositionelles Verfeinern - ausgehend von einer groben, deklarativen Spezifikation bis hin zum detaillierten, operationellen Entwurf - ermöglichen und im Rahmen von Behavioural Types auch eine Schnittstelle zur parallelen Programmierung bieten. Darüber hinaus möchte ich kurz ein weiteres Forschungsthema des Lehrstuhls zur Identifikation von dynamischen Datenstrukturen in C-Programmen vorstellen.
Modal Interface Automata. Departmental seminar, Department of Computer Science, Technical University of Dortmund, Germany, February 2014. Abstract / Slides.

Several modern interface theories for formally modelling and reasoning about component-based, concurrent systems have been built at the crossroads of de Alfaro and Henzinger's Interface Automata (IA) and Larsen's Modal Transition Systems (MTS). Two established examples are Nyman et al.'s IOMTS and Bauer et al.'s MIO, which differ in their view of component compatibility: IOMTS adopts an optimistic view leading to a more permissive parallel composition operator than MIO's, but has technical shortcomings regarding (non-)monotonicity of refinement and the treatment of internal computation. In addition, both approaches neither consider conjunction on interfaces nor do they allow extending alphabets when refining system components, which are practically desired properties that enable one to specify and design systems incrementally.

In this talk I present the novel interface theory Modal Interface Automata (MIA), which addresses the above shortcomings, and discuss MIA's design decisions, trade-offs and limitations. The reported research is joint work with Walter Vogler, Universität Augsburg.
Modal Interface Automata. Seminar on Synchronous Programming. Schloss Dagstuhl, Germany, November 2013. Abstract / Slides.

Several modern interface theories for formally modelling and reasoning about component-based, concurrent systems have been built at the crossroads of de Alfaro and Henzinger's Interface Automata (IA) and Larsen's Modal Transition Systems (MTS). Two established examples are Nyman et al.'s IOMTS and Bauer et al.'s MIO, which differ in their view of component compatibility: IOMTS adopts an optimistic view leading to a more permissive parallel composition operator than MIO's, but has technical shortcomings regarding (non-)monotonicity of refinement and the treatment of internal computation. In addition, both approaches neither consider conjunction on interfaces nor do they allow extending alphabets when refining system components, which are practically desired properties that enable one to specify and design systems incrementally.

This talk presents the novel interface theory Modal Interface Automata (MIA), which addresses the above shortcomings, and discusses MIA's design decisions, trade-offs and limitations. The reported research is joint work with Walter Vogler of the University of Augsburg, Germany.
Modal Interface Automata. Departmental seminar, Department of Information and Computer Science, Aalto University, Finland, August 2013. Abstract / Slides.

Several modern interface theories for formally modelling and reasoning about component-based, concurrent systems have been built at the crossroads of de Alfaro and Henzinger's Interface Automata (IA) and Larsen's Modal Transition Systems (MTS). Two established examples are Nyman et al.'s IOMTS and Bauer et al.'s MIO, which differ in their view of component compatibility: IOMTS adopts an optimistic view leading to a more permissive parallel composition operator than MIO's, but has technical shortcomings regarding (non-)monotonicity of refinement and the treatment of internal computation. In addition, both approaches neither consider conjunction on interfaces nor do they allow extending alphabets when refining system components, which are practically desired properties that enable one to specify and design systems incrementally.

In this talk I present the novel interface theory Modal Interface Automata (MIA), which addresses the above shortcomings, and discuss MIA's design decisions, trade-offs and limitations. The reported research is joint work with Walter Vogler of the University of Augsburg, Germany.
MIA 2.0: Richer Interface Automata with Optimistic and Pessimistic Compatibility. 25 Years of Combining Compositionality and Concurrency, Königswinter, Germany, August 2013. Abstract / Slides.

Several modern interface theories for formally modelling and reasoning about component-based, concurrent systems have been built at the crossroads of de Alfaro and Henzinger's Interface Automata (IA) and Larsen's Modal Transition Systems (MTS). Two established examples are Nyman et al.'s IOMTS and Bauer et al.'s MIO, which differ in their view of component compatibility: IOMTS adopts an optimistic view leading to a more permissive parallel composition operator than MIO's, but has technical shortcomings regarding (non-)monotonicity of refinement and the treatment of internal computation. In addition, both approaches neither consider conjunction on interfaces nor do they allow extending alphabets when refining system components, which are practically desired properties that enable one to specify and design systems incrementally.

In this talk we will present our novel interface theory Modal Interface Automata (MIA), which addresses these shortcomings in an optimistic and also in a pessimistic setting, and discuss MIA's design decisions, trade-offs and limitations. (This talk was held jointly with Walter Vogler of the University of Augsburg, Germany. The online slides here are those of Prof. Lüttgen's part.)
Modellieren, Programmieren, Verifizieren: Dreiklang der Softwaretechnik und Programmiersprachen. Inaugural lecture, Faculty of Information Systems and Applied Computer Sciences, University of Bamberg, Germany, January 2013. Abstract / Slides.

Modellieren, Programmieren, Verifizieren - Der Informatiker Gerald Lüttgen beschäftigte sich in seiner Antrittsvorlesung mit den Hintergründen der Softwareentwicklung. Dabei ging er bis zu den Anfängen der Programmierung zurück und schlug den Bogen bis in die Gegenwart zu aktuellen Forschungsprojekten am Lehrstuhl.
Software für die Raumfahrt: Lernen aus Unglücksfällen und Erfolgen. Talk at a software development company, Germany, November 2012. Abstract / Slides.

Dieser Vortrag berichtet über Anstrengungen zur Qualitätssicherung bei der Entwicklung von Software für die Raumfahrt.
Heterogene Modellierungsformalismen für komplexe Systeme. Department of Informatics and Mathematics, University of Passau, Germany, June 2012.
Agile Methoden: Leichtgewichte der Softwareentwicklung. IT Cluster Oberfranken, Bamberg, Germany, July 2011. Abstract / Slides.

Dieser Vortrag berichtet über den fortwährenden Trend hin zu agileren Methoden der Softwareentwicklung.
Parallelising symbolic state-space generators: Frustration and hope. Seminar on Distributed Verification and Grid Computing. Schloss Dagstuhl, Germany, August 2008. Abstract / Slides.

Due to the irregular nature of the task, efficient algorithms for symbolic state-space generation are notoriously hard to parallelise. This talk explores two different strategies for parallelising and implementing one such algorithm, Saturation, on multi-core PCs: one strategy employs the parallel language Cilk, while the other uses a thread pool implemented in Pthreads.

I will analyse the underlying parallel overheads, present experimental results and argue their relevance. The conclusions will give room for both frustration and hope regarding the parallelisability of symbolic model checkers on shared-memory architectures.
Neue Wege der Softwareentwicklung mit Contractual Statecharts. Faculty of Information Systems and Applied Computer Sciences, University of Bamberg, Germany, May 2008.
Ready simulation for concurrency: It's Logical! Department of Computer Science. University of Leicester, England, November 2007. Abstract / Slides.

This talk presents a concurrency-theoretic framework that allows one to truly mix operational and logic styles of specification. Heterogeneous methodologies supporting multi-paradigm specifications have strong practical motivations, and design notations such as the UML already provide superficial support for them.

Our framework adds a conjunction operator to the standard setting of labelled transition systems with CSP-style parallel composition. We show that the well-known behavioural relation of ready simulation is fully abstract with respect to failures inclusion. Ready simulation also satisfies standard logic properties, and thus lends itself to studying mixed operational and logic languages.
Ready simulation for concurrency: It's Logical! School of Informatics. University of Edinburgh, Scotland, September 2007. Abstract / Slides.

This talk presents a concurrency-theoretic framework that allows one to truly mix operational and logic styles of specification. Heterogeneous methodologies supporting multi-paradigm specifications have strong practical motivations, and design notations such as the UML already provide superficial support for them.

Our framework adds a conjunction operator to the standard setting of labelled transition systems with CSP-style parallel composition. We show that the well-known behavioural relation of ready simulation is fully abstract with respect to failures inclusion. Ready simulation also satisfies standard logic properties, and thus lends itself to studying mixed operational and logic languages.
Parallelising symbolic state-space generators: Frustration and hope. Verification and Testing Group. University of Sheffield, England, June 2007. Abstract / Slides.

Due to the irregular nature of the task, efficient algorithms for symbolic state-space generation are notoriously hard to parallelise. This talk explores two different strategies for parallelising and implementing one such algorithm, Saturation, on multi-core PCs: one strategy employs the parallel language Cilk, while the other uses a thread pool implemented in Pthreads.

I will analyse the underlying parallel overheads, present experimental results and argue their relevance. The conclusions will give room for both frustration and hope regarding the parallelisability of symbolic model checkers on shared-memory architectures.

The research on which this talk is based is funded by the EPSRC under grant no. GR/S86211/01: "New-Generation Symbolic Model Checkers for Verifying Asynchronous Systems".
Embedded Systems Design with Statecharts. National Institute of Aerospace, Hampton, Virginia, May 2006. Abstract / Slides.

Statecharts is a popular language for designing the control flow of embedded systems. Various dialects of the language are integrated in many commercial design tools, such as Simulink/Stateflow and SCADE, which are gaining popularity within the avionics industry.

This talk gives an introduction to the concepts underlying the syntax and semantics of Statecharts, with a particular focus on SCADE's Safe State Machines. It also highlights the current limitations of Statecharts and concludes with an outlook regarding future improvements.
Conjunction on processes: Full-abstraction via ready-tree semantics. Department of Computer Science, Theory Special Interest Group, University of Sheffield, England, March 2006. Abstract / Slides.

A key problem in mixing operational (e.g., process-algebraic) and declarative (e.g., logical) styles of specification is how to deal with inconsistencies arising when composing processes under conjunction. This talk introduces a conjunction operator on labelled transition systems which captures the basic intuition of "a and b = false", and considers a naive preorder which demands that an inconsistent specification can only be refined by an inconsistent implementation.

The main result is a characterisation of the largest precongruence contained in the naive preorder. This characterisation is based on a novel semantics called ready-tree semantics, which refines ready traces but is coarser than ready simulation. It is proved that the induced ready-tree preorder is compositional and fully-abstract, and that the conjunction operator indeed reflects conjunction.

The obtained results provide a foundation for, and an important step towards a unified framework that allows one to freely mix operators from process algebras and linear-time temporal logics. A small but typical example will be presented which illustrates this point.
Structured Symbolic Model Checking of Asynchronous Systems. Department of Computer Science, Aachen University of Technology, Germany, December 2005. Abstract / Slides.

Model checking is a popular technology for assessing the correctness of discrete-state systems. Its success, particularly in the hardware industry, has been made possible by the discovery of Binary Decision Diagrams (BDDs) as a suitable data structure for compactly storing the huge state spaces described by synchronous digital circuits. However, BDD-based model checking does not scale when analysing asynchronous systems, such as Petri nets, protocols and concurrent software.

This talk presents a novel algorithm for generating and analysing the state spaces of asynchronous systems, which employs Multi-valued Decision Diagrams and Kronecker-based data structures. These permit the systematic exploitation of structural information of asynchronous system models, such as taking into account the locality of effect for an event, and the use of a new strategy for computing fixed points. Experimental studies show huge improvements in both memory and time efficiency when compared to state-of-the-art model checkers.
Teaching the British Way: My Daily Cup of Tea. Faculty of Information Systems and Applied Computer Sciences, University of Bamberg, Germany, October 2005. Abstract / Slides.

UK Universities are internationally known for their high quality education and their service-oriented approach to teaching. York is in the premier league, or Top Ten, according to most league tables published annually in quality British newspapers. It is 1st for teaching in most of these tables.

This informal talk will give a first-hand report of what teaching quality means at York, how it is achieved, and what impact it has on students and lecturers alike.

The speaker is teaching in the UK for the past five years and is currently a Senior Lecturer at the University of York. He is or has been actively involved in various administrative roles ranging from Principal Admissions Tutor, to Staff Handbook Editor, to Coordinator of York's Advanced MSc in Software Engineering degree course.
When 1 Clock Is Not Enough. Intl. Workshop on Algebraic Process Calculi: The First Twenty Five Years and Beyond. Bertinoro, Italy, August 2005. Slides.
Structured Symbolic Model Checking of Asynchronous Systems. Department of Computer Science, University of Saarbrücken, Germany, June 2005. Videocast simultaneously to the Universities of Freiburg and Oldenburg, Germany. Abstract / Slides.

Model checking is a popular technology for assessing the correctness of discrete-state systems. Its success, particularly in the hardware industry, has been made possible by the discovery of Binary Decision Diagrams (BDDs) as a suitable data structure for compactly storing the huge state spaces described by synchronous digital circuits. However, BDD-based model checking does not scale when analysing asynchronous systems, such as Petri nets, protocols and concurrent software.

This talk presents a novel algorithm for generating and analysing the state spaces of asynchronous systems, which employs Multi-valued Decision Diagrams and Kronecker-based data structures. These permit the systematic exploitation of structural information of asynchronous system models, such as taking into account the locality of effect for an event, and the use of a new strategy for computing fixed points. Experimental studies show huge improvements in both memory and time efficiency when compared to state-of-the-art model checkers. The talk concludes by briefly describing recent efforts in parallelising this particular algorithm and in benchmarking model-checking algorithms in general.
Structured Symbolic Model Checking of Asynchronous Systems. Informatics Theory Group, University of Bamberg, Germany, November 2004. Abstract / Slides.

Model checking is a popular technology for assessing the correctness of discrete-state systems. Its success, particularly in the hardware industry, has been made possible by the discovery of Binary Decision Diagrams (BDDs) as a suitable data structure for compactly storing the huge state spaces described by synchronous digital circuits. However, BDD-based model checking does not scale when analysing asynchronous systems, such as Petri nets, protocols and concurrent software.

This talk presents a novel algorithm for generating and analysing the state spaces of asynchronous systems, which employs Multi-valued Decision Diagrams and Kronecker-based data structures. These permit the systematic exploitation of structural information of asynchronous system models, such as taking into account the locality of effect for an event, and the use of a new strategy for computing fixed points. Experimental studies show huge improvements in both memory and time efficiency when compared to state-of-the-art symbolic tools. The talk concludes by briefly describing an application to an embedded software system being developed at NASA for use in civil aviation.
Statecharts: From Visual Syntax to Model-Theoretic Semantics. Formal Methods Group, Department of Computer Science, University of Manchester, England, May 2004. Abstract / Slides.

Statecharts is a popular visual notation for modelling synchronous reactive systems, which extends finite state automata by concepts of hierarchy and concurrency. The language's semantics has been made precise in a seminal paper by Pnueli and Shalev in the early Nineties, which offers both an operational and a declarative account.

This talk proposes an alternative approach to defining the semantics of Statecharts: the visual syntax of a Statechart is read, directly and structurally, as a formula in propositional logic whose models are expected to encode its step semantics. A closer look, however, reveals that the correct semantics (in the sense of Pnueli and Shalev) is only obtained when interpreting the propositional formula not classically but intuitionistically.

The suggested model-theoretic approach offers several benefits. On the one hand, it permits the integration of Statecharts in automated verification tools (such as theorem provers). On the other hand, it paves the road for solving some open problems related to Statecharts semantics (such as compositionality and full abstraction) and for clarifying its relation to other popular synchronous languages (such as Esterel).
Structured Symbolic Model Checking of Asynchronous Systems. Department of Computer Science, University of Manchester, England, May 2004. Abstract / Slides.

Model checking is a popular technology for assessing the correctness of discrete-state systems. Its success, particularly in the hardware industry, has been made possible by the discovery of Binary Decision Diagrams (BDDs) as a suitable data structure for compactly storing the huge state spaces described by synchronous digital circuits. However, BDD-based model checking does not scale when analysing asynchronous systems, such as Petri nets, protocols and concurrent software.

This talk presents a novel algorithm for generating and analysing the state spaces of asynchronous systems, which employs Multi-valued Decision Diagrams and Kronecker-based data structures. These permit the systematic exploitation of structural information of asynchronous system models, such as taking into account the locality of effect for an event, and the use of a new strategy for computing fixed points. Experimental studies show huge improvements in both memory and time efficiency when compared to state-of-the-art symbolic tools. The talk concludes by briefly describing an application to an embedded software system being developed at NASA for use in civil aviation.
A Compositional Semantic Theory for Synchronous Component-based Design. Department of Informatics, University of Sussex, England, June 2003. Abstract / Slides.

Digital signal processing (DSP) tools, such as National Instruments' LabView and Micro-Epsilon's iConnect, allow application developers to assemble systems by connecting predefined components in signal-flow graphs and by hierarchically building new components via encapsulating sub-graphs. Run-time environments then dynamically schedule components for execution on some embedded processor, typically in a synchronous cycle-based fashion, and check whether one component jams another by producing outputs faster than can be consumed.

This talk will report on a recent EPSRC-funded project that aimed at providing a foundation for enhancing existing DSP tools by conducting behavioural validations, such as jam-freeness, automatically at compile-time. A process-algebraic coordination model for synchronous component-based design will be presented, which lends itself to compositionally formalising the monolithic semantics of DSP tools. In particular, it will be discussed how the DSP principles of dynamic synchronous scheduling, isochrony and encapsulation may be captured faithfully and compositionally in a process algebra combining the well-known concepts of abstract clocks, maximal progress and clock-hiding. Finally, it will be shown how observation equivalence may facilitate static jam checks.
Statecharts: From Visual Syntax to Model-Theoretic Semantics. Formal Methods & Tools Group, Faculty of Computer Science, University of Twente, The Netherlands, November 2002. Abstract / Slides.

Statecharts is a popular visual specification language for modelling synchronous reactive systems, which extends finite state automata by concepts of hierarchy and concurrency. The language's semantics has been made precise by Pnueli and Shalev in the early Nineties; their seminal paper offers both an operational and a declarative account.

This talk proposes an alternative approach to defining the semantics of Statecharts: the visual syntax of a Statechart is read, directly and structurally, as a formula in propositional logic whose models are expected to encode its desired step semantics. A closer look, however, reveals that the correct semantics (in the sense of Pnueli and Shalev) is obtained when interpreting the propositional formula not classically but intuitionistically.

The suggested model-theoretic approach offers several benefits. On the one hand, it permits the integration of Statecharts in automated verification tools (such as theorem provers). On the other hand, it paves the road for solving some open problems related to Statecharts semantics (such as compositionality and full abstraction).
Towards a Model-Theory for Esterel. Department of Computer Science, University of York, England, July 2002. Slides.
Die intuitionistische Natur von Statecharts. Department of Mathematics and Computer Science, University of Augsburg, Germany, October 2001. Abstract / Slides.

Statecharts ist eine unter Ingenieuren beliebte synchrone, graphische Sprache zur Spezifikation reaktiver Systeme (z.B. Tempomaten in PKW), welche die Notation endlicher Automaten um ein Hierarchiekonzept und um einen Mechanismus zur parallelen Komposition erweitert. Die Semantik von Statecharts wurde Anfang der 90er Jahre in einem wegweisenden Papier von Pnueli & Shalev auf deklarative und operationelle Weise mathematisch praezisiert.

Dieser Vortrag stellt einen alternativen Weg zur Semantikdefinition vor, bei dem die graphische Syntax eines Statecharts in natuerlicher Weise als eine aussagenlogische Formel gelesen wird, dessen Modelle die gewuenschte Semantik beschreiben sollen. Eine genauere Betrachtung offenbart, dass die korrekte Semantik im Sinne von Pnueli und Shalev nicht wie gelegentlich angenommen einer klassichen sondern einer intuitionistischen Interpretation der aussagenlogischen Formel entspricht.

Der vorgeschlagene modelltheoretische Ansatz hat im Vergleich zu dem von Pnueli und Shalev mehrere Vorteile: zum einen erlaubt er die Integration von Statecharts mit Verifikationswerkzeugen (z.B. Theorembeweisern), zum anderen zeigt er einen Weg zur Loesung offener Probleme innerhalb der Semantik von Statecharts (z.B. Kompositionalitaet und volle Abstraktheit) auf.
Priority in Process Algebra. 1st Intl. School on Formal Methods for the Design of Computer, Communication and Software Systems: Process Algebras (SFM-01:PA), Bertinoro, Italy, July 2001. Slides.
The Intuitionism Behind Statecharts Steps. Department of Computer Science, University of York, England, May 2001. Slides.
A Faster-than Relation for Asynchronous Processes. 17th British Colloquium for Theoretical Computer Science (BCTCS 17), Glasgow, Scotland, April 2001. Abstract / Slides.

This talk introduces a novel (bi)simulation-based faster-than preorder which relates asynchronous processes with respect to their worst-case timing behavior. The underlying studies were conducted for a conservative extension of the process algebra CCS, called TACS (Timed Asynchronous Communicating Systems), which permits the specification of maximal time bounds of actions. TACS complements work in plain process algebras which compares asynchronous processes with respect to their functional reactive behavior only, and in timed process algebras which focus on analyzing synchronous processes.

The most unusual contribution of the reported work are results showing that the proposed faster-than preorder coincides with two other and at least equally appealing preorders, one of which considers the absolute times at which actions occur in system runs. The talk also presents the semantic theory of TACS, including a characterization of the largest precongruence contained in the faster-than preorder and its axiomatization in a fragment of the algebra. A small example relating two implementations of a simple storage system testifies to the practical utility of the new theory.

The research, on which this talk is based, has been jointly conducted with Walter Vogler, The University of Augsburg, Germany.
The Intuitionism Behind Statecharts Steps. NASA Ames Research Center, Moffett Field, California, August 2000. Abstract / Slides.

Statecharts is a popular synchronous visual language for specifying reactive systems, which extends finite-state machines by concepts of hierarchy, parallel composition, and priority. In a seminal paper published in the early nineties, Pnueli and Shalev formalized Statecharts step semantics. Unfortunately, their semantics is not compositional, which is a prerequisite for structurally analyzing Statecharts and for modularly compiling Statecharts into program fragments. The lack of compositionality resulted in the development of several Statecharts dialects as well as in the definition of new synchronous languages, such as Esterel.

This talk analyzes and repairs the compositionality defect of Pnueli and Shalev's semantics by borrowing ideas from intuitionistic logic. The motivation for employing this logic is rooted in the observation that the logic underlying Statecharts step semantics violates the Law of the Excluded Middle. Within a novel theoretic framework which is based on intuitionistic linear Kripke structures, I first characterize Pnueli and Shalev's semantics and then derive a new compositional and fully-abstract step semantics. The obtained results not only give insights into the semantic subtleties of Statecharts and enable their efficient implementation, but also support a formal comparison among different Statecharts variants.
Analyzing Mode Confusion via Model Checking. Jet Propulsion Laboratory, Pasadena, California, August 2000. Abstract / Slides.

Mode confusion is a serious problem in aviation safety. Today's complex avionics systems make it difficult for pilots to maintain awareness of the actual states, or modes, of the flight deck automation. Recently, NASA Langley has explored how Formal Methods can be used to discover mode confusion.

This talk reports on the application of state-exploration techniques, such as model checking, to the abovementioned problem domain. It also compares the verification tools Murphi, SMV, and Spin for the specific application.
Efficient Symbolic State-space Construction for Asynchronous Systems. Department of Computer Science, University of Sheffield, England, May 2000. Abstract / Slides.

Many state-of-the-art techniques for the verification of today's complex embedded systems rely on the analysis of their reachable state spaces. In this talk I present a new algorithm, developed by Gianfranco Ciardo and Radu Siminiceanu of the College of William & Mary and myself, for the symbolic generation of the state spaces of asynchronous system models, such as Petri nets. The algorithm is based on previous work that employs Multi-valued Decision Diagrams (MDDs) for efficiently storing sets of reachable states. In contrast to related approaches, however, it fully exploits event locality which is a fundamental semantic property of asynchronous systems. Additionally, it supports intelligent cache management and achieves faster convergence via advanced iteration control. The algorithm is implemented in the Petri net tool SMART, and run-time results show that it often performs significantly faster than existing state-space generators.
Pre-emptive Modeling of Distributed Systems. Department of Computer Science, University of Sheffield, England, January 2000. Slides.
Formal Methods: Objectives, Techniques, & Perspectives. Department of Computer Science, Old Dominion University, Virginia, December 1999. Abstract / Slides.

This talk gives an introduction to the field of Formal Methods.

Formal Methods aims at the precise modeling of and the rigorous mathematical reasoning about digital systems. This is of particular importance for the growing number of embedded systems used in safety-critical applications, such as those employed in automotive and avionics systems.

The rationale behind Formal Methods is closely related to that in other engineering disciplines, e.g., fluid dynamics. However, rather than using numerical mathematics, Formal Methods techniques are based on discrete mathematics, i.e., logics and deduction, as well as automata and formal language theory. Formal methods complement well-established quality assurance techniques, in particular, reviews and system tests. Calculations carried out by Formal Methods tools support system designers in checking for inconsistencies in requirements, revealing errors in system designs, and verifying critical portions of the implemented system.
A Semantic Foundation for Heterogeneous Specification Formalisms. Department of Computer Science, Aachen University of Technology, Germany, October 1999. Abstract / Slides.

Research in the specification and verification of concurrent systems falls into two general categories, the assertional approach and the operational approach. The temporal logic school advocates the assertional approach which employs temporal-logic formulas for system specification, with the semantics of the logic being used as the basis for determining whether or not a system is correct. In contrast, a large part of the process algebra school favors the operational approach. This approach focuses on using a state-machine semantics of process terms as the basis for relating system specifications and implementations via behavioral equivalences and preorders.

In this talk, I present ongoing research by Rance Cleaveland, SUNY at Stony Brook, and myself on the development of a semantic foundation for a heterogeneous specification formalism permitting mixtures of assertional and operational specification styles. The benefits of such a mixed specification formalism are manifold, since it supports the following:

(1) capture of system correctness via refinement, i.e., it enables a sound, gradual transition from abstract, assertional system requirements to concrete, operational system designs;

(2) definition of systems in which some components are or remain only specified as temporal-logic formulas, e.g., when dealing with off-the-shelf components;

(3) consideration of constraints, including fairness constraints, which are imposed by a system's environment or which are known to be true of specific system components.

Technically, we are concerned with assertional specifications using linear-time logics (LTL) and operational specifications using labeled transition systems. Our semantic framework is founded on Buechi automata, which we equip with a behavioral relation based on DeNicola/Hennessy must-testing preorder. We show that this preorder is a conservative extension of the classical must-preorder and that it is "compatible" to the LTL satisfaction relation, i.e., LTL model checking becomes a special case of preorder checking.
A Semantic Foundation for Heterogeneous Specification Formalisms. Verification and Testing Group. University of Sheffield, England, October 1999. Abstract / Slides.

Research in the specification and verification of concurrent systems falls into two general categories, the assertional approach and the operational approach. The temporal logic school advocates the assertional approach which employs temporal-logic formulas for system specification, with the semantics of the logic being used as the basis for determining whether or not a system is correct. In contrast, a large part of the process algebra school favors the operational approach. This approach focuses on using a state-machine semantics of process terms as the basis for relating system specifications and implementations via behavioral equivalences and preorders.

In this talk, I present ongoing research by Rance Cleaveland, SUNY at Stony Brook, and myself on the development of a semantic foundation for a heterogeneous specification formalism permitting mixtures of assertional and operational specification styles. The benefits of such a mixed specification formalism are manifold, since it supports the following:

(1) capture of system correctness via refinement, i.e., it enables a sound, gradual transition from abstract, assertional system requirements to concrete, operational system designs;

(2) definition of systems in which some components are or remain only specified as temporal-logic formulas, e.g., when dealing with off-the-shelf components;

(3) consideration of constraints, including fairness constraints, which are imposed by a system's environment or which are known to be true of specific system components.

Technically, we are concerned with assertional specifications using linear-time logics (LTL) and operational specifications using labeled transition systems. Our semantic framework is founded on Buechi automata, which we equip with a behavioral relation based on DeNicola/Hennessy must-testing preorder. We show that this preorder is a conservative extension of the classical must-preorder and that it is "compatible" to the LTL satisfaction relation, i.e., LTL model checking becomes a special case of preorder checking.
Modellieren Nebenläufiger und Verteilter Systeme mit Präemption. 1998 Dissertation Award Colloquium of the German Society of Computer Science (Gesellschaft für Informatik), Schloss Dagstuhl, Germany, April 1999. Slides.
Statecharts via Process Algebra. Department of Computer Science, State University of New York at Stony Brook, New York, March 1999.
Approaches to State-space Reduction. Institute for Computer Applications in Science and Engineering (ICASE), NASA Langley Research Center, Hampton, Virginia, March 1998. Slides.
Formal Analysis and Verification. Daimler-Benz, Research Department for Electronics, Technology, and Tools, Stuttgart, Germany, February 1998. Slides.
Pre-emptive Modeling of Concurrent and Distributed Systems. Department of Mathematics and Computer Science, University of Augsburg, Germany, January 1998. Abstract.

Prozeßalgebren sind ein formalen Rahmen zur Modellierung und Verifikation nebenläufiger Systeme. Sie bestehen typischerweise aus einer einfachen Sprache zusammen mit einer wohldefinierten operationellen Semantik basierend auf beschrifteten Transitionssystemen. Mittels einer Äquivalenzrelation werden dann Implementationen und Spezifikationen von Systemen in Relation gesetzt. Um ein kompositionelles Vorgehen zu ermöglichen, bei dem Systeme auf der Grundlage des Verhaltens ihrer Teilkomponenten verifiziert werden, sollte die betrachtete Äquivalenzrelation auch eine Kongruenz sein.

Traditionelle Prozeßalgebren, z.B. Milners CCS (Calculus of Communicating Systems) mit Bisimulationsäquivalenz, beschränken sich auf die Modellierung des potentiellen Nichtdeterminismus, welcher durch Parallelismus hervorgerufen wird. Insbesondere wird von den wichtigen Aspekten Prioritäten und Zeit abstrahiert, was ein exaktes Modellieren erschwert. Um diese Schwäche zu beheben, wurde in der Literatur das semantische Konzept der globalen Präemption eingeführt, so daß einigen Transitionen Präzedenz über anderen Transitionen gegeben werden kann. Existierende Erweiterungen eignen sich jedoch vorwiegend zur Behandlung von zentralisierten und nicht von verteilten Systemen; beispielsweise berücksichtigen Realzeit-Prozeßalgebren in der Regel nur eine globale Uhr.

In diesem Vortrag stellen wir Erweiterungen von CCS um Prioritäten und Zeit fuer verteilte Systeme vor, indem wir ein lokales Präemptionskonzept entwickeln und anhand von elementaren Beispielen motivieren. Dies hat weitreichende semantische Implikationen, insbesondere auf die Kongruenzeigenschaft der Bisimulation, auf welche wir im Vortrag näher eingehen werden.
Dynamic Priorities for Modeling Real-Time. Real-Time Systems Group, University of Pennsylvania, Pennsylvania, September 1997.
Kompositionelle Minimierung Endlicher Verteilter Systeme. Department of Computer Science, University of Erlangen, Germany, June 1996. Abstract.

Viele formale Analyse- und Verifikationsmethoden arbeiten auf Transitionssystemen, welche das Verhalten von (verteilten) Systemen repräsentieren.

Oftmals reicht es fuer die Verifikation eines Systems aus, eine Abstraktion des zugehörigen Transitionssystems zu betrachten, weil zahlreiche Berechnungen des Systems aus der Sicht eines Beobachters irrelevant sind. Daher kann in der Regel ein Transitionssystem durch eine Zusammenfassung semantisch äquivalenter Zustände drastisch kollabiert werden. Beispielsweise kann das Ergebnis einer solchen Minimierung eines komplexen Kommunikationsprotokolls ein einfacher Buffer sein.

In dem Vortrag wird eine Methode zur kompositionellen Konstruktion eines im Sinne einer Bisimulationssemantik minimalen Transitionssystems für verteilte Systeme vorgestellt. Ziel der Methode ist es, die durch das Interleaving von Aktionen kommunizierender Parallelkomponenten verursachte Zustandsexplosion zu kontrollieren.

Die Besonderheit der Methode ist, dass neben Minimierungsschritten auch Reduktionsschritte durchgeführt werden. Dabei steht der Begriff eines Reduktionsoperators im Vordergrund, welcher im Kontext unerreichbare Zustände und Transitionen eliminiert. Dies geschieht mit Hilfe von Interfacespezifikationen, die die möglichen Kommunikationssequenzen zwischen Parallelkomponenten eines Systems beschreiben.

Die Effizienz dieser Methode hängt von der Exaktheit der vom Programmentwickler bereitgestellten Interfacespezifikationen ab. Die Korrektheit der Methode ist jedoch von der Korrektheit der Interfacespezifikationen unabhängig.
An Algebraic Approach to Distributed Priorities. Seminar on Semantics of Concurrent Systems - Foundations and Applications, Schloss Dagstuhl, Germany, May 1996.
Unvergleichbare Prioritäten mit Prozessalgebren. Department of Mathematics and Computer Science, University of Passau, Germany, December 1995. Abstract.

Im Mittelpunkt des Vortrags steht eine CCS-basierte Prozessalgebra mit Prioritaeten. Die Notwendigkeit von Prioritaeten zur Modellierung und Verifikation verteilter Systeme wird unmittelbar deutlich, wenn man an Interruptmechanismen und verschiedene Konstrukte von Programmiersprachen - etwa das PRIALT Konstrukt in occam - denkt. Im Gegensatz zu anderen Ansaetzen auf diesem Gebiet haengt die von uns definierte operationelle Semantik von einer Vergleichbarkeitsrelation ab, welche Prioritaeten auf verschiedenen Seiten des Paralleloperators als unvergleichbar betrachtet. Der Nutzen dieses Designs - sowohl fuer die Modellierung als auch fuer die Verifikation verteilter Systeme - wird anhand eines einfachen Beispiels demonstriert. Innerhalb unseres prozessalgebraischen Rahmens charakterisieren wir die groesste, in der ueblichen starken Bisimulation enthaltene Kongruenz und stellen deren Axiomatisierung vor. Ausserdem entwickeln wir eine Beobachtungskongruenz und zeigen, dass dies die groesste Kongruenz innerhalb einer naiv definierten Beobachtungsaequivalenz ist.