List of Publications

Below is a complete listing of all publications of Prof. Lüttgen.

Important Copyright Notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders, such as publishers. All persons copying this information are expected to adhere to the terms and constraints invoked by each copyright holder. In most cases, these works may not be reposted without explicit permission of the copyright holder.

Books

Lüttgen, G. Pre-emptive modeling of concurrent and distributed systems. Shaker Verlag, 1998. ISBN 3-8265-3932-X. (Dissertation.) Abstract / Article / BibTeX.

Process algebras constitute a widely studied framework for modeling and verifying concurrent systems. Such theories typically consist of a simple language with a well-defined operational semantics given in terms of labeled transition systems; a behavioral equivalence is then used to relate implementations and specifications, which are both given as terms in the language. In order to facilitate compositional reasoning, in which systems are verified on the basis of the behavior of their components, researchers have devoted great attention to the definition of behavioral congruences, which permit the substitution of "equals for equals" inside larger systems.

Traditional process algebras focus on modeling the potential nondeterminism that concurrent processes may exhibit. They abstract away the details such as time, priority and data from implementation. However, many of these abstractions lose too much information and, thus, complicate the accurate modeling of important system behavior. Consequently, approaches have been suggested for re-introducing sensitivity to some of the mentioned aspects of system behavior, especially to priority and time. Both of these phenomena deal with pre-emption since some transitions may have precedence over others. In temporal process algebras this is due to the maximal progress assumption which prevents clock ticks whenever the system under consideration can engage in internal computation. Most of these extensions, however, have been devoted to modeling centralized, as opposed to distributed systems; the real-time work, in particular, has focused on systems with a single clock. The centralized character of these approaches is reflected by the choice of a global notion of pre-emption in the underlying semantic theories. Whereas this interpretation of pre-emption is adequate for modeling concurrent systems in uni-processor environments, it is too restrictive for achieving an intuitive semantics for distributed systems.

The contribution of this dissertation is to shed some light on the semantic concept of pre-emption for priority and time. The first part re-investigates and advances classical approaches dealing with priority and time in process algebras based on global pre-emption. Two medium-scale case studies dealing with a safety-critical railway signaling system and the SCSI-2 bus-protocol testify to the importance of incorporating these aspects in process algebra for system modeling and verification. Moreover, it is formally shown that time can conceptually be understood as a dynamic variant of priority. In the second part of the thesis the shortcomings for reasoning about existing theories with respect to distributed systems are pointed out and, subsequently, are eliminated without sacrificing the simplicity and the elegance that have led to their success. Therefore, process algebras with priority and time are developed incorporating a localized notion of pre-emption which allows one to keep the abstract view of process algebras as far as possible but has far-reaching consequences for the semantic theories. Technically, the considered and developed calculi extend the well-studied process algebra CCS by priority and time. The presented semantic theories are based on the notion of bisimulation and include abstractness results as well as axiomatic and logical characterizations of the behavioral relations. Generic examples illustrate the practical utility of the approaches to distributed system modeling and verification.

^ Top

Chapters in Books

Cleaveland, R., Lüttgen, G. and Natarajan, V. Priority in process algebra. In J.A. Bergstra, A. Ponse, and S.A. Smolka, eds., Handbook of Process Algebra, ch. 12, pp. 711-765. Elsevier Science Publishers, 2001. ISBN 0-444-82830-3. Abstract / Article / BibTeX.

This chapter surveys the semantic ramifications of extending traditional process algebras with notions of priority that allow for some transitions to be given precedence over others. The need for these enriched formalisms arises when one wishes to model system features such as interrupts, prioritized choice, or real-time behavior.

Approaches to priority in process algebras can be classified according to whether the induced notion of pre-emption on transitions is global or local and whether priorities are static or dynamic. Early work in the area concentrated on global pre-emption and static priorities and led to formalisms for modeling interrupts and aspects of real-time, such as maximal progress, in centralized computing environments. More recent research has investigated localized notions of pre-emption in which the distribution of systems is taken into account, as well as dynamic priority approaches, i.e., those where priority values may change as systems evolve. The latter allows one to model behavioral phenomena such as scheduling algorithms and also enables the efficient encoding of real-time semantics.

Technically, this chapter studies the different models of priorities by presenting extensions of Milner's Calculus of Communicating Systems (CCS) with static and dynamic priority as well as with notions of global and local pre-emption. In each case the operational semantics of CCS is modified appropriately, behavioral theories based on strong and weak bisimulation are given, and related approaches for different process-algebraic settings are discussed.
Lüttgen, G. Modellieren nebenläufiger und verteilter Systeme mit Präemption. Ausgezeichnete Informatikdissertationen 1998 (Distinguished Dissertations in Computer Science 1998), pp. 102-111. B.G. Teubner, 1999. ISBN 3-519-02648-1. Abstract / Article / BibTeX.

Aus unserem modernen Leben sind computerunterstützte Systeme nicht mehr wegzudenken. Wir müssen uns vor allem auf sicherheitskritische Systeme, wie sie z.B. in der Medizin oder in der Luftfahrt eingesetzt werden, verlassen können. Um deren Korrektheit hinreichend genau nachzuweisen, genügen ausgiebige Systemtests alleine nicht. Vielmehr wird ein mathematisch präziser Rahmen zur Systemmodellierung und Systemverifikation benötigt, wie ihn etwa Prozeßalgebren für die besonders diffizilen nebenläufigen und verteilten Systeme bieten.

Traditionelle Prozeßalgebren, z.B. Milners Calculus of Communicating Systems (CCS), beschränken sich auf die Modellierung des potentiellen Nichtdeterminismus, welcher durch die verzahnte Ausführung der Aktionen paralleler Prozesse hervorgerufen wird. Dabei wird meist von wichtigen Aspekten, wie z.B. Prioritäten und Zeit, abstrahiert, was ein exaktes Modellieren realer Systeme erschwert. Um diese Schwäche zu beheben, wurde in der Literatur das semantische Konzept der Präemption eingeführt, welches es ermöglicht, einigen Aktionen Präzedenz über anderen Aktionen zu geben. Existierende Erweiterungen klassischer Prozeßalgebren eignen sich vorwiegend zur Behandlung zentraler, aber nicht verteilter Systeme. In diesem Artikel skizzieren wir eine Erweiterung von CCS um Prioritäten, welche auch die Verteilung von Systemen berücksichtigt. Die dabei auftretenden semantischen Konzepte werden anhand eines einfachen Beispiels veranschaulicht.

^ Top

Articles in Journals

Vogler, W. and Lüttgen, G. A linear-time branching-time perspective on Interface Automata. Acta Informatica, 57(3):513-550, 2020. Abstract / Article / BibTeX / DOI.

Over the past two decades, de Alfaro and Henzinger's interface automata (IA) have become a popular formal framework for the component-based specification of concurrent systems. IA's parallel composition assumes that a component may wait on inputs but never on outputs, implying that an output must be consumed immediately or a communication error occurs. By now, the literature contains a number of semantics for IA: linear-time semantics based on traces observing communication errors, quiescence and/or divergence, as well as branching-time semantics based on alternating simulation.

This article surveys these semantics from Rob van Glabbeek's linear-time branching-time perspective, which does not consider settings with communication errors. We shed light onto the subtleties implied by IA's pruning of all behaviour that might lead a component to autonomously enter an error state, and investigate when exactly de Alfaro and Henzinger's restriction of input-determinism is needed. In addition, we introduce several new semantics for IA, in particular the linear-time ready semantics and the branching-time ready simulation.
Fendrich, S. and Lüttgen, G. A generalised theory of Interface Automata, component compatibility and error. Acta Informatica, 56(4):287-319, 2019. Abstract / Article / BibTeX / DOI.

Interface theories allow system designers to reason about the composability and compatibility of concurrent system components. Such theories often extend both de Alfaro and Henzinger's Interface Automata and Larsen's Modal Transition Systems, which leads, however, to several issues that are undesirable in practice: an unintuitive treatment of specified unwanted behaviour, a binary compatibility concept that does not scale to multi-component assemblies, and compatibility guarantees that are insufficient for software product lines. In this article we show that communication mismatches are central to all these problems and, thus, the ability to represent such errors semantically is an important feature of an interface theory. Accordingly, we present the error-aware interface theory EMIA, where the above shortcomings are remedied by introducing explicit fatal error states. In addition, we prove via a Galois insertion that EMIA is a conservative generalisation of the established Modal Interface Automata theory.
Bujtor, F., Fendrich, S., Lüttgen, G. and Vogler, W. Nondeterministic Modal Interfaces. Theoretical Computer Science, 642:24-53, 2016. Abstract / Article / BibTeX / DOI.

Interface theories are employed in the component-based design of concurrent systems. They often emerge as combinations of Interface Automata (IA) and Modal Transition Systems (MTS), e.g., Nyman et al.'s IOMTS, Bauer et al.'s MIO, Raclet et al.'s MI or our MIA. In this paper, we generalise MI to interfaces, for which we properly resolve the longstanding conflict between unspecified inputs being allowed in IA but forbidden in MTS. With this solution we achieve, in contrast to related work, an associative parallel composition, a compositional preorder, a conjunction on interfaces with dissimilar alphabets supporting perspective-based specifications, and a quotienting operator for decomposing nondeterministic specifications in a single theory. In addition, we define a hiding and a restriction operator, complement conjunction with a disjunction operator and illustrate our interface theory by means of a simple example.
Lüttgen, G., Vogler, W. and Fendrich, S. Richer interface automata with optimistic and pessimistic compatibility. Acta Informatica, 52(4-5): 305-336, 2015. Abstract / Article / BibTeX / DOI.

Modal transition systems are a popular semantic underpinning of interface theories, such as Nyman et al.'s IOMTS and Bauer et al.'s MIO, which facilitate component-based reasoning for concurrent systems. Our interface theory MIA repaired a compositional flaw of IOMTS-refinement and introduced a conjunction operator. In this paper, we first modify MIA to properly deal with internal computations including internal must-transitions, which were largely ignored already in IOMTS. We then study a MIA variant that adopts MIO's pessimistic - rather than IOMTS' optimistic - view on component compatibility and define, for the first-time in a pessimistic, non-deterministic setting, conjunction and disjunction on interfaces. For both the optimistic and pessimistic MIA variant, we also discuss mechanisms for extending alphabets when refining interfaces, which is a desired feature for perspective-based specification. We illustrate our advancements via a small example.
Mühlberg, J. T. and Lüttgen, G. Symbolic object code analysis. Software Tools for Technology Transfer, 16(1):81-102, 2014. Abstract / Article / BibTeX / DOI.

Software model checkers quickly reach their limits when being applied to verifying pointer safety properties in source code that includes function pointers and inlined assembly. This article introduces a novel technique for checking pointer safety violations, called Symbolic Object Code Analysis (SOCA), which is based on bounded symbolic execution, incorporates path-sensitive slicing, and employs the SMT solver Yices as its execution and verification engine. Extensive experimental results of a prototypic SOCA Verifier, using the Verisec suite and almost 10,000 Linux device driver functions as benchmarks, show that SOCA performs competitively to modern source-code model checkers, scales well when applied to real operating systems code and pointer safety issues, and effectively explores niches of pointer-complex software that current software verifiers do not reach.
Lüttgen, G. and Vogler, W. Modal Interface Automata. Logical Methods in Computer Science, 9(3:4), 2013. Abstract / Article / BibTeX / DOI.

De Alfaro and Henzinger's Interface Automata (IA) and Nyman et al.'s recent combination IOMTS of IA and Larsen's Modal Transition Systems (MTS) are established frameworks for specifying interfaces of system components. However, neither IA nor IOMTS consider conjunction that is needed in practice when a component shall satisfy multiple interfaces, while Larsen's MTS-conjunction is not closed and Benes et al.'s conjunction on disjunctive MTS does not treat internal transitions. In addition, IOMTS-parallel composition exhibits a compositionality defect.

This article defines conjunction (and also disjunction) on IA and disjunctive MTS and proves the operators to be 'correct', i.e., the greatest lower bounds (least upper bounds) wrt. IA- and resp. MTS-refinement. As its main contribution, a novel interface theory called Modal Interface Automata (MIA) is introduced: MIA is a rich subset of IOMTS featuring explicit output-must-transitions while input-transitions are always allowed implicitly, is equipped with compositional parallel, conjunction and disjunction operators, and allows a simpler embedding of IA than Nyman's. Thus, it fixes the shortcomings of related work, without restricting designers to deterministic interfaces as Raclet et al.'s modal interface theory does.
Mühlberg, J. T. and Lüttgen, G. Verifying compiled file system code. Formal Aspects of Computing, 24(3):375-391, 2012. Special issue on the Brazilian Symposium on Formal Methods (SBMF 2009). Abstract / Article / BibTeX / DOI.

This article presents a case study on retrospective verification of the Linux Virtual File System (VFS), which is aimed at checking violations of API usage rules and memory properties. Since VFS maintains dynamic data structures and is written in a mixture of C and inlined assembly, modern software model checkers cannot be applied. Our case study centres around our novel automated software verification tool, the SOCA Verifier, which symbolically executes and analyses compiled code. We describe how this verifier deals with complex features such as memory access, pointer aliasing and computed jumps in the VFS implementation, while reducing manual modelling to a minimum. Our results show that the SOCA Verifier is capable of analysing the complex Linux VFS implementation reliably and efficiently, thereby going beyond traditional testing tools and into niches that current software model checkers do not reach. This testifies to the SOCA Verifier's suitability as an effective and efficient bug-finding tool during the development of operating system components.
Lüttgen, G. and Vogler, W. Safe reasoning with Logic LTS. Theoretical Computer Science, 412(28):3337-3357, 2011. Bergstra Festschrift. Abstract / Article / BibTeX / DOI.

Previous work has introduced the setting of Logic Labelled Transition Systems, called Logic LTS or LLTS for short, together with a variant of ready simulation as fully-abstract refinement preorder, which allows one to compose operational specifications using a CSP-style parallel operator and the propositional connectives conjunction and disjunction.

In this article, we show how a temporal logic for specifying safety properties may be embedded into LLTS so that (a) the temporal operators are compositional for ready simulation; (b) ready simulation, when restricted to pairs of processes and formulas, coincides with the logic's satisfaction relation; (c) ready simulation, when restricted to formulas, is entailment.

The utility of this setting as a semantic foundation for mixed operational and temporal-logic specification languages is demonstrated by means of a simple example. We also adopt the concept of may- and must-transitions from modal transition systems for notational convenience, and investigate the relation between modal refinement on modal transition systems and ready simulation on LLTS.
Lüttgen, G. and Vogler, W. Ready simulation for concurrency: It's logical! Information and Computation, 208:845-867, 2010. Abstract / Article / BibTeX / DOI.

This article provides new insight into the connection between the trace-based lower part of van Glabbeek's linear-time, branching-time spectrum and its simulation-based upper part. We establish that ready simulation is fully abstract with respect to failure inclusion, when adding the conjunction operator that was proposed by the authors in [TCS 373(1-2):19-40] to the standard setting of labelled transition systems with (CSP-style) parallel composition. More precisely, we actually prove a stronger result by considering a coarser relation than failure inclusion, namely a preorder that relates processes with respect to inconsistencies that may arise under conjunctive composition.

Ready simulation is also shown to satisfy standard logic properties. In addition, our semantic formalism proves itself robust when adding disjunction, external choice and hiding operators, and is thus suited for studying mixed operational and logic languages. Finally, the utility of our formalism is demonstrated by means of a small example that deals with specifying and reasoning about mode logics within aircraft control systems.
Mendler, M. and Lüttgen, G. Is observational congruence on mu-expressions axiomatisable in equational Horn logic? Information and Computation, 208:634-651, 2010. Special Issue on Concurrency Theory (CONCUR 2007). Abstract / Article / BibTeX / DOI.

It is well known that bisimulation on mu-expressions cannot be finitely axiomatised in equational logic. Complete axiomatisations such as those of Milner and Bloom/Esik necessarily involve implicational rules. However, both systems rely on features beyond pure equational Horn logic: either rules that are impure by involving non-equational side-conditions, or rules that are schematically infinitary like the congruence rule which is not Horn. It is an open question whether these complications cannot be avoided in the proof-theoretically and computationally clean and powerful setting of second-order equational Horn logic.

This article presents a positive and a negative result regarding the axiomatisability of observational congruence in equational Horn logic. Firstly, we show how Milner's impure rule system can be reworked into a pure Horn axiomatisation that is complete for guarded processes. Secondly, we prove that for unguarded processes, both Milner's unique fixed point rule and Bloom/Esik's GA rule are incomplete without the congruence rule, and neither system has a complete extension in rank 1 equational axioms. It remains open whether there are higher-rank equational axioms or other Horn rules which would render Milner's or Bloom/Esik's axiomatisations complete.
Ezekiel, J., Lüttgen, G., and Siminiceanu, R. To parallelise or to optimise? Journal of Logic and Computation, 21(1):85-120, 2011. Special Issue on Parallel and Distributed Methods of verifiCation (PDMC). Abstract / Article / BibTeX / DOI.

Model checking is a popular and successful technique for verifying complex digital systems. Carrying this technique - and its underlying state-space generation algorithms - beyond its current limitations presents itself with a number of alternatives. Our focus is on parallelisation which is made attractive by the current trend in hardware architectures towards multi-core, multi-processor systems. The main obstacle in this endeavour is that, in particular, symbolic state-space generation algorithms are notoriously hard to parallelise.

In this article, we describe the process of taking a sequential symbolic state-space generation algorithm, namely a generic, symbolic BFS algorithm, through a sequence of optimisations that leads up to the Saturation algorithm, and follow the impact these sequential algorithms have on their parallel counterparts. In particular, we develop a parallel version of Saturation, discuss the challenges faced in its design, and conduct extensive experimental studies of its implementation. We employ rigorous analysis tools and techniques for measuring and evaluating parallel overheads and the quality of the parallelisation.

The outcome of these studies is that the performance of a parallel symbolic state-space generation algorithm is almost impossible to predict and highly dependent on the model to which it is applied. In most situations, perceivable speed-ups are hard to achieve, but real-world applications where our technique produces significant improvements do exist. Nevertheless, it appears that time is better invested in optimising sequential symbolic model checking algorithms rather than parallelising them.
Yu, A. J., Ciardo, G. and Lüttgen, G. Decision-diagram-based techniques for bounded reachability checking of asynchronous systems. Software Tools for Technology Transfer, 11(2):117-131, 2009. Abstract / Article / BibTeX / DOI.

Bounded reachability analysis and bounded model checking are widely believed to perform poorly when using decision diagrams instead of SAT procedures. Recent research suggests this to be untrue with regards to synchronous systems and, in particular, digital circuits. This article shows that the belief is also a myth for asynchronous systems, such as models specified by Petri nets. We propose several Bounded Saturation approaches to compute bounded state spaces using decision diagrams. These approaches are based on the established Saturation algorithm, which benefits from a non-standard search strategy that is very different from breadth-first search, but employ different flavors of decision diagrams: Multi-valued Decision Diagrams, Edge-valued Decision Diagrams, and Algebraic Decision Diagrams. We apply our approaches to studying deadlock as a safety property. Our extensive benchmarking shows that our algorithms often, but not always, compare favorably against two SAT-based approaches that are advocated in the literature.
Hierons, R. M., Bogdanov, K., Bowen, J. P., Cleaveland, R., Derrick, J., Dick, J., Gheorghe, M., Harman, M., Kapoor, K., Krause, P., Lüttgen, G., Simons, A. J. H. Simons, Vilkomir, S., Woodward, M. R. and Zedan, H. Using formal specifications to support testing. ACM Computing Surveys, 41(2):1--76, 2009. Abstract / BibTeX / DOI.

Formal methods and testing are two important approaches that assist in the development of high quality software. While traditionally these approaches have been seen as rivals, in recent years a new consensus has developed in which they are seen as complementary. This article reviews the state of the art regarding ways in which the presence of a formal specification can be used to assist testing.
White, D. and Lüttgen, G. Embedded systems programming: Accessing databases from Esterel. EURASIP Journal of Embedded Systems, Vol. 2008, Article ID 961036, 17pp., 2008. Abstract / Article / BibTeX / DOI.

A current limitation in embedded controller design and programming is the lack of database support in development tools such as Esterel Studio. This article proposes a way of integrating databases and Esterel by providing two Application Programming Interfaces (APIs) which enable the use of relational databases inside Esterel programs. As databases and Esterel programs are often executed on different machines, result sets returned as responses to database queries may be processed either locally and according to Esterel's synchrony hypothesis, or remotely along several of Esterel's execution cycles. These different scenarios are reflected in the design and usage rules of the two APIs presented in this article, which rely on Esterel's facilities for extending the language by external data types, external functions and procedures, as well as tasks.

The APIs' utility is demonstrated by means of a case study modelling an automated warehouse storage system, which is constructed using Lego Mindstorms robotics kits. The robot's controller is programmed in Esterel in a way that takes dynamic ordering information and the warehouse's floor layout into account, both of which are stored in a MySQL database.
Cleaveland, R., Lüttgen, G. and Natarajan, V. Priority and abstraction in process algebra. Information and Computation 205(9):1426-1458, 2007. Abstract / Article / BibTeX / DOI.

More than 15 years ago, Cleaveland and Hennessy proposed an extension of the process algebra CCS in which some actions may take priority over others. The theory was equipped with a behavioral congruence based on strong bisimulation.

This article gives a full account of the challenges in, and the solutions employed for, defining a semantic theory of observation congruence for this process algebra. A full-abstraction result is presented whose proof relies on a novel approach based on successive approximations for identifying the largest congruence contained in an intuitive but naive equivalence. Prioritized observation congruence is also characterized equationally for the class of finite processes, while its utility for system verification is demonstrated by an illustrative example.
Ciardo, G., Lüttgen, G. and Miner, A. S. Exploiting interleaving semantics in symbolic state-space generation. Formal Methods in System Design 31(1):63-100, 2007. Abstract / Article / BibTeX / DOI.

Symbolic techniques based on Binary Decision Diagrams (BDDs) are widely employed for reasoning about temporal properties of hardware circuits and synchronous controllers. However, they often perform poorly when dealing with the huge state spaces underlying systems based on interleaving semantics, such as communications protocols and distributed software, which are composed of independently acting subsystems that communicate via shared events.

This article shows that the efficiency of state-space exploration techniques using decision diagrams can be drastically improved by exploiting the interleaving semantics underlying many event-based and component-based system models. A new algorithm for symbolically generating state spaces is presented that (i) encodes a model's state vectors with Multi-valued Decision Diagrams (MDDs) rather than flattening them into BDDs and (ii) partitions the model's Kronecker-consistent next-state function by event and subsystem, thus enabling multiple lightweight next-state transformations rather than a single heavyweight one. Together, this paves the way for a novel iteration order, called Saturation, which replaces the breadth-first search order of traditional algorithms. The resulting Saturation algorithm is implemented in the tool SMART, and experimental studies show that it is often several orders of magnitude better in terms of time efficiency, final memory consumption, and peak memory consumption than existing symbolic algorithms.
Lüttgen, G. and Vogler, W. Conjunction on processes: Full-abstraction via ready-tree semantics. Theoretical Computer Science, 373(1-2):19-40, 2007. Abstract / Article / BibTeX / DOI.

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 article introduces a conjunction operator on labelled transition systems capturing the basic intuition of "a and b = false", and considers a naive preorder that demands that an inconsistent specification can only be refined by an inconsistent implementation.

The main body of the article is concerned with characterising the largest precongruence contained in the naive preorder. This characterisation will be based on what we call ready-tree semantics, which is a variant of path-based possible-worlds semantics. We prove that the induced ready-tree preorder is compositional and fully-abstract, and that the conjunction operator indeed reflects conjunction.

The article's 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.
Lüttgen, G. and Vogler, W. Bisimulation on speed: A unified approach. Theoretical Computer Science, 360(1-3):209-227, 2006. Abstract / Article / BibTeX / DOI.

Two process-algebraic approaches have been developed for comparing two bisimulation-equivalent processes with respect to speed: the one of Moller-Tofts equips actions with lower time bounds, while the other by Lüttgen-Vogler considers upper time bounds instead.

This article sheds new light on both approaches by testifying to their close relationship. We introduce a general, intuitive concept of "faster-than", which is formalised by a notion of amortised faster-than preorder. When closing this preorder under all contexts, exactly the two faster-than preorders investigated by Moller/Tofts and Lüttgen/Vogler arise. For processes incorporating both lower and upper time bounds we also show that the largest precongruence contained in the amortised faster-than preorder is not a proper preorder but a timed bisimulation. In the light of this result we systematically investigate under which circumstances the amortised faster-than preorder degrades to an equivalence.
Lüttgen, G. and Vogler, W. Bisimulation on speed: Lower time bounds. RAIRO - Theoretical Informatics and Applications, 39:587-618, 2005. Special Issue on Foundations of Software Science and Computation Structures (FOSSACS 2004). Abstract / Article / BibTeX.

More than a decade ago, Moller and Tofts published their seminal work on relating processes, which are annotated with lower time bounds, with respect to speed. Their paper has left open many questions regarding the semantic theory for the suggested bisimulation-based faster-than preorder, the MT-preorder, which have not been addressed since. The encountered difficulties concern a general compositionality result, a complete axiom system for finite processes, a convincing intuitive justification of the MT-preorder, and the abstraction from internal computation.

This article solves these difficulties by developing and employing a novel commutation lemma relating the sequencing of action and clock transitions in discrete-time process algebra. Most importantly, it is proved that the MT-preorder is fully-abstract with respect to a natural amortized preorder that uses a simple bookkeeping mechanism for deciding whether one process is faster than another. Together these results reveal the intuitive roots of the MT-preorder as a faster-than relation, while testifying to its semantic elegance. This lifts some of the barriers that have so far hampered progress in semantic theories for comparing the speed of processes.
Lüttgen, G. and Vogler, W. Bisimulation on speed: Worst-case efficiency. Information and Computation, 191(2):105-144, 2004. Abstract / Article / BibTeX / DOI.

This paper introduces a novel (bi)simulation-based faster-than preorder which relates asynchronous processes, where the relative speeds of system components are indeterminate, with respect to their worst-case timing behavior. The study is conducted for a conservative extension of the process algebra CCS, called TACS, which permits the specification of upper time bounds on action occurrences. 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 is in showing that the proposed faster-than preorder coincides with several other preorders, two of which consider the absolute times at which actions occur in system runs. The paper also develops the semantic theory of TACS by studying congruence properties, equational laws, and abstractions from internal actions. Two examples, one dealing with mail delivery and one relating two implementations of a simple storage system, testify to the practical utility of the new theory.
Lüttgen, G. and Mendler, M. The intuitionism behind Statecharts steps. ACM Transactions on Computational Logic, 3(1):1-41, 2002. Abstract / Article / BibTeX / DOI.

The semantics of Statecharts macro steps, as introduced by Pnueli and Shalev, lacks compositionality. This paper first analyzes the compositionality problem and traces it back to the invalidity of the Law of the Excluded Middle. It then characterizes the semantics via a particular class of linear intuitionistic Kripke models. This yields, for the first time in the literature, a simple fully-abstract semantics which interprets Pnueli and Shalev's concept of failure naturally. The results not only give insight into the semantic subtleties of Statecharts, but also provide a basis for an implementation, for developing algebraic theories for macro steps, and for comparing different Statecharts variants.
Bhat, G., Cleaveland, R. and Lüttgen, G. A practical approach to implementing real-time semantics. Annals of Software Engineering, 7:127-155, 1999. Special issue on Real-time Software Engineering. Abstract / Article / BibTeX.

This paper investigates implementations of process algebras which are suitable for modeling concurrent real-time systems. It suggests an approach for efficiently implementing real-time semantics using dynamic priorities. For this purpose a process algebra with dynamic priority is defined, whose semantics corresponds one-to-one to traditional real-time semantics. The advantage of the dynamic-priority approach is that it drastically reduces the state-space sizes of the systems in question while preserving all properties of their functional and real-time behavior. The utility of the technique is demonstrated by a case study which deals with the formal modeling and verification of several aspects of the widely-used SCSI-2 bus-protocol. The case study is carried out in the Concurrency Workbench of North Carolina, an automated verification tool in which the process algebra with dynamic priority is implemented. It turns out that the state space of the bus-protocol model is about an order of magnitude smaller than the one resulting from real-time semantics. The accuracy of the model is proved by applying model checking for verifying several mandatory properties of the bus protocol.
Cleaveland, R., Lüttgen, G. and Natarajan, V. A process algebra with distributed priorities. Theoretical Computer Science, 195(2):227-258, 1998. Special issue on Concurrency Theory (CONCUR '96). Abstract / Article / BibTeX / DOI.

This paper presents a process algebra for distributed systems in which some actions may take precedence over others. The algebra is distinguished by the design decision that it only allows actions to pre-empt others at the same "location" and therefore captures a notion of localized precedence. Using Park's and Milner's notion of strong bisimulation as a basis, we develop a behavioral congruence and axiomatize it for finite processes; we also derive an associated observational congruence and present logical characterizations of our behavioral relations. Simple examples highlight the utility of the theory.
Cleaveland, R., Lüttgen, G., Natarajan, V. and Sims, S. Modeling and verifying distributed systems using priorities: A case study. Software - Concepts and Tools, 17(2):50-62, 1996. Abstract / Article / BibTeX.

This paper illustrates the use of priorities in process algebras by a real-world example dealing with the design of a safety-critical network which is part of a railway signaling system. Priorities in process algebras support an intuitive modeling of distributed systems since undesired interleavings can be suppressed. This fact also leads to a substantial reduction of the sizes of the models. We have implemented a CCS-based process algebra with priorities as a new front-end for the NCSU Concurrency Workbench, and we used model checking for verifying properties of the signaling system.
Graf, S., Steffen, B. and Lüttgen, G. Compositional minimisation of finite state systems using interface specifications. Formal Aspects of Computing, 8(5):607-616, 1996. Abstract / Article / Long Version / BibTeX.

We present a method for the compositional construction of the minimal transition system that represents the semantics of a given distributed system. Our aim is to control the state explosion caused by the interleavings of actions of communicating parallel components by reduction steps that exploit global communication constraints given in terms of interface specifications. The effect of the method, which is developed for bisimulation semantics here, depends on the structure of the distributed system under consideration, and the accuracy of the interface specifications. However, its correctness is independent of the correctness of the interface specifications provided by the program designer.

^ Top

Papers Published in Refereed Proceedings

Boockmann, J. H. and Lüttgen, G. Learning data structure shapes from memory graphs. In 23rd Intl. Conf. on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-23), vol. 73 of EPiC Series in Computing, pp. 151-168, 2020. EasyChair. Abstract / Article / BibTeX / DOI.

This paper presents a novel algorithm for automatically learning recursive shape pred- icates from memory graphs, so as to formally describe the pointer-based data structures contained in a program. These predicates are expressed in separation logic and can be used, e.g., to construct efficient secure wrappers that validate the shape of data structures exchanged between trust boundaries at runtime. Our approach first decomposes memory graph(s) into sub-graphs, each of which exhibits a single data structure, and generates candidate shape predicates of increasing complexity, which are expressed as rule sets in Prolog. Under separation logic semantics, a meta-interpreter then performs a systematic search for a subset of rules that form a shape predicate that non-trivially and concisely captures the data structure. Our algorithm is implemented in the prototype tool ShaPE and evaluated on examples from the real-world and the literature. It is shown that our approach indeed learns concise predicates for many standard data structures and their implementation variations, and thus alleviates software engineers from what has been a time-consuming manual task.
Lüttgen, G. A note on refinement in hierarchical transition systems. In 23rd Intl. Conf. on Formal Methods for Industrial Critical Systems (FMICS 2018), vol. 11119 of Lecture Notes in Computer Science, pp. 211-222, Maynooth, Ireland, September 2018. Springer-Verlag. Abstract / Article / BibTeX / DOI.

Software engineers frequently employ notations and tools based on transition systems, such as UML state machines and Statecharts, for specifying and reasoning about reactive behaviour. While these notations are typically supported by an operational semantics, they lack a formal underpinning of the incremental refinement practices of engineers who, e.g., place state machines inside states or add outer transitions to states during design. This note sketches how modal transition systems may be applied to formally capture such refinements along state hierarchies, using a hierarchical extension of labelled transition systems that permits engineers to explicitly allow or disallow state refinement and transition extension at each state. A small example testifies to the utility of this framework for hierarchically refining reactive systems.
Sailer, A., Deubzer, M., Lüttgen, G. and Mottok, J. Comparing trace recordings of automotive real-time software. In 25th Intl. Conf. on Real-Time Networks and Systems (RTNS 2017), pp. 118-127, Grenoble, France, October 2017. ACM. Abstract / Article / BibTeX / DOI.

The process of engineering models of existing real-time system components is often difficult and time consuming, especially when legacy code has to be re-used or information about the exact timing behaviour is needed. In order to tackle this reverse engineering problem, we have developed a tool called CoreTAna. CoreTAna derives an AUTOSAR compliant model of a real-time system by conducting dynamic analysis using trace recordings.

Motivated by the challenge of assessing the quality of reverse engineered models of real-time software, we present a novel mathematical measurement for comparing trace recordings from embedded real-time systems regarding their temporal behaviour. We also introduce a benchmark framework based on this measure, for evaluating reverse engineering tools such as CoreTAna. For an evaluation, trace recordings of the benchmark, of randomly generated systems, and of three exemplary industrial projects in the automotive domain are applied to CoreTAna. Finally, an industrial case study demonstrates other use cases of the measure such as impact analysis.
Rupprecht, T., Chen, X., White, D. H., Boockmann, J. H., Lüttgen, G. and Bos, H. DSIbin: Identifying dynamic data structures in C/C++ binaries. In 32nd IEEE/ACM Intl. Conf. on Automated Software Engineering (ASE 2017), pp. 331-341, Urbana-Champaign, Illinois, USA, October/November 2017. IEEE/ACM. Abstract / Article / BibTeX / DOI.

Reverse engineering binary code is notoriously difficult and, especially, understanding a binary's dynamic data structures. Existing data structure analyzers are limited wrt. program comprehension: they do not detect complex structures such as skip lists, or lists running through nodes of different types such as in the Linux kernel's cyclic doubly-linked list. They also do not reveal complex parent-child relationships between structures. The tool DSI remedies these shortcomings but requires source code, where type information on heap nodes is available.

We present DSIbin, a combination of DSI and the type excavator Howard for the inspection of C/C++ binaries. While a naive combination already improves upon related work, its precision is limited because Howard's inferred types are often too coarse. To address this we auto-generate candidates of refined types based on speculative nested-struct detection and type merging; the plausibility of these hypotheses is then validated by DSI. We demonstrate via benchmarking, that DSIbin detects data structures with high precision.
Rupprecht, T., Chen, X., White, D. H., Mühlberg, J. T., Bos, H. and Lüttgen, G. POSTER: Identifying dynamic data structures in malware. In ACM SIGSAC Conf. on Computer and Communications Security (CCS 2016), pp. 1772-1774, Vienna, Austria, October 2016. ACM. Abstract / Article / BibTeX / DOI.

As the complexity of malware grows, so does the necessity of employing program structuring mechanisms during de velopment. While control flow structuring is often obfuscated, the dynamic data structures employed by the program are typically untouched. We report on work in progress that exploits this weakness to identify dynamic data structures present in malware samples for the purposes of aiding reverse engineering and constructing malware signatures, which may be employed for malware classification.

Using a prototype implementation, which combines the type recovery tool Howard and the identification tool Data Structure Investigator (DSI), we analyze data structures from Carberp and AgoBot malware. Identifying their data structures illustrates a challenging problem. To tackle this, we propose a new type recovery for binaries based on machine learning, which uses Howard's types to guide the search and DSI's memory abstraction for hypothesis evaluation.
Sailer, A., Deubzer, M., Lüttgen, G. and Mottok, J. CoreTAna: A trace analyzer for reverse engineering real-time software. In 23rd Intl. Conf. on Software Analysis, Evolution, and Reengineering (SANER 2016), pp. 657-660, Osaka, Japan, March 2016. IEEE Computer Society. Abstract / Article / BibTeX / DOI.

With the availability of the AUTOSAR standard, model-driven methodologies are becoming established in the automotive domain. However, the process of creating models of existing system components is often difficult and time consuming, especially when legacy code has to be re-used or information about the exact timing behaviour is needed. In order to tackle this reverse engineering problem, we present CoreTAna, a novel tool that derives an AUTOSAR compliant model of a real-time system from a dynamic analysis of its trace recordings. This paper gives an overview of CoreTAna's current features and discusses its benefits for reverse engineering.
White, D. H., Rupprecht, T. and Lüttgen, G. DSI: An evidence-based approach to identify dynamic data structures in C programs. In A. Roychoudhury, ed., 2016 Intl. Symp. on Software Testing and Analysis (ISSTA 2016), pp. 259-269, Saarbrücken, Germany, July 2016. ACM. Abstract / Article / BibTeX / DOI.

Comprehension of C programs containing pointer-based dynamic data structures can be a challenging task. To tackle this challenge we present Data Structure Investigator (DSI), a new dynamic analysis for automated data structure identification that targets C source code. Our technique first applies a novel abstraction on the evolving memory structures observed at runtime to discover data structure building blocks. By analyzing the interconnections between building blocks we are then able to identify, e.g., binary trees, doubly-linked lists, skip lists, and relationships between these such as nesting. Since the true shape of a data structure may be temporarily obscured by manipulation operations, we ensure robustness by first discovering and then reinforcing evidence for data structure observations. We show the utility of our DSI prototype implementation by applying it to both synthetic and real world examples. DSI outputs summarizations of the identified data structures, which will benefit software developers when maintaining (legacy) code.
Fendrich, S. and Lüttgen, G. A generalised theory of Interface Automata, component compatibility and error. In E. Abraham and M. Huisman, eds., 12th Intl. Conf. on Integrated Formal Methods (IFM 2016), vol. 9681 of Lecture Notes in Computer Science, pp. 160-175, Reykjavik, Iceland, June 2016. Springer-Verlag. Abstract / Article / BibTeX / DOI.

Interface theories allow systems designers to reason about the composability and compatibility of concurrent system components. Such theories often extend both de Alfaro and Henzinger's Interface Automata and Larsen's Modal Transition Systems, which leads, however, to several issues that are undesirable in practice: an unintuitive treatment of specified unwanted behaviour, a binary compatibility concept that does not scale to multi-component assemblies, and compatibility guarantees that are insufficient for software product lines.

In this paper we show that communication mismatches are central to all these problems and, thus, the ability to represent such errors semantically is an important feature of an interface theory. Accordingly, we present the error-aware interface theory EMIA, where the above shortcomings are remedied by introducing explicit fatal error states. In addition, we prove via a Galois insertion that EMIA is a conservative generalisation of the established MIA (Modal Interface Automata) theory.
Mühlberg, J. T., White, D. H., Dodds, M., Lüttgen, G. and Piessens, F. Learning assertions to verify linked-list programs. In R. Calinsecu and B. Rumpe, eds., 13th Intl. Conf. on Software Engineering and Formal Methods (SEFM 2015), vol. 9276 of Lecture Notes in Computer Science, pp. 37-52, York, UK, September 2015. Springer-Verlag. Abstract / Article / BibTeX / DOI.

C programs that manipulate list-based dynamic data structures remain a challenging target for static verification. In this paper we employ the dynamic analysis of dsOli to locate and identify data structure operations in a program, and then use this information to automatically annotate that program with assertions in separation logic. These annotations comprise candidate pre/post-conditions and loop invariants suitable to statically verify memory safety with the verification tool VeriFast. By using both textbook and real-world examples on our prototype implementation, we show that the generated assertions are often discharged automatically. Even when this is not the case, candidate invariants are of great help to the verification engineer, significantly reducing the manual verification effort.
Bujtor, F., Fendrich, S., Lüttgen, G. and Vogler, W. Nondeterministic Modal Interfaces. In G. F. Italiano, T. Margaria-Steffen, J. Pokorny, J.-J. Quisquater and R. Wattenhofer, eds., 41st Intl. Conf. on Current Trends in Theory and Practice of Computer Science (SOFSEM 2015), vol. 8939 of Lecture Notes in Computer Science, pp. 152-163, Pec pod Snezkou, Czech Republic, January 2015. Springer-Verlag. Abstract / Article / BibTeX / DOI.

Interface theories are employed in the component-based design of concurrent systems. They often emerge as combinations of Interface Automata (IA) and Modal Transition Systems (MTS), e.g., Nyman et al.'s IOMTS, Bauer et al.'s MIO, Raclet et al.'s MI or our MIA. In this paper, we generalise MI to nondeterministic interfaces, for which we resolve the longstanding conflict between unspecified inputs being allowed in IA but forbidden in MTS. With this solution we achieve, in contrast to related work, an associative parallel composition, a compositional preorder, a conjunction on interfaces with dissimilar alphabets supporting perspective-based specifications, and a quotienting operator for decomposing nondeterministic specifications in a single theory.
Lüttgen, G. and Vogler, W. Richer Interface Automata with optimistic and pessimistic compatibility. In H. Treharne and S. Schneider, eds., 13th Intl. Workshop on Automated Verification of Critical Systems (AVoCS 2013), vol. 66 of Electronic Communications of the EASST, Guildford, England, September 2013. European Association of Software Science and Technology. Abstract / Article / BibTeX / Open Access.

Modal transition systems are a popular semantic underpinning of interface theories, such as Nyman et al.'s IOMTS and Bauer et al.'s MIO, which facilitate component-based reasoning of concurrent systems. Our interface theory MIA repaired a compositional flaw of IOMTS-refinement and introduced a conjunction operator. In this paper, we first modify MIA to properly deal with internal computations including internal must-transitions, which were largely ignored already in IOMTS. We then study a MIA variant that adopts MIO's pessimistic - rather than IOMTS' optimistic - view on component compatibility and define, for the first-time in a pessimistic, non-deterministic setting, conjunction and disjunction on interfaces. For both the optimistic and pessimistic MIA variants, we also provide a mechanism for extending alphabets when refining interfaces, which is a desired feature in practice. We illustrate our advancements via a small example.
White, D. H. and Lüttgen, G. Identifying dynamic data structures by learning evolving patterns in memory. In N. Piterman and S. A. Smolka, eds., 19th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2013), vol. 7795 of Lecture Notes in Computer Science, pp. 354-369, Rome, Italy, March 2013. Springer-Verlag. Abstract / Article / BibTeX / DOI.

We investigate whether dynamic data structures in pointer programs can be identified by analysing program executions only. This paper describes a first step towards solving this problem by applying machine learning and pattern recognition techniques to analyse executions of C programs. By searching for repeating temporal patterns in memory caused by multiple invocations of data-structure operations, we are able to first locate and then identify these operations. Applying a prototypic tool implementing our approach to pointer programs that employ, e.g., lists, queues and stacks, we show that the identified operations can accurately determine the data structures used.
Lüttgen, G. and Vogler, W. Modal Interface Automata. In J.C.M. Baeten, T. Ball and F.S. de Boer, eds., 7th IFIP Intl. Conf. on Theoretical Computer Science (TCS 2012), vol. 7604 of Lecture Notes in Computer Science, pp. 265-279, Amsterdam, The Netherlands, September 2012, Springer-Verlag. Abstract / Article / BibTeX / DOI.

De Alfaro and Henzinger's Interface Automata (IA) and Nyman et al.'s recent combination IOMTS of IA and Larsen's Modal Transition Systems (MTS) are established frameworks for specifying interfaces of system components. However, neither IA nor IOMTS consider conjunction that is needed in practice when a component satisfies multiple interfaces, while Larsen's MTS-conjunction is not closed. In addition, IOMTS-parallel composition exhibits a compositionality defect. This paper defines conjunction on IA and MTS and proves the operators to be `correct', i.e., the greatest lower bounds wrt. IA- and resp. MTS-refinement. As its main contribution, a novel interface theory called Modal Interface Automata (MIA) is introduced: MIA is a rich subset of IOMTS, is equipped with compositional parallel and conjunction operators, and allows a simpler embedding of IA than Nyman's. Thus, it fixes the shortcomings of related work, without restricting designers to deterministic interfaces as Raclet et al.'s modal interface theory does.
Ditter, A., Ceska, M. and Lüttgen, G. On Parallel software verification using Boolean equation systems. In A. Donaldson and D. Parker, eds., 19th Intl. SPIN Workshop on Model Checking Software (SPIN 2012), vol. 7385 of Lecture Notes in Computer Science, pp. 80-97, Oxford, England, July 2012, Springer-Verlag. Abstract / Article / BibTeX / DOI.

Multi- and many-core hardware platforms are today widely accessible and used to significantly accelerate many computationally demanding tasks. In this paper we describe a parallel approach to solve Boolean Equation Systems (BESs) in the context of model checking. We focus on the applicability of state-of-the-art, shared-memory parallel hardware - multi-core CPUs and many-core GPUs - to speed up the resolution procedure for BESs. In this setting, we experimentally show the scalability and competitiveness of our approach, compared to an optimized sequential implementation, based on a large benchmark suite containing models of software systems and protocols from industry and academia.
Siirtola, A., Puhakka, A. und Lüttgen, G. Introducing fairness into compositional verification via unidirectional counters. In 12th Intl. Conf. on Application of Concurrency to System Design (ACSD 2012), pp. 32-41, Hamburg, Germany, June 2012, IEEE Computer Society. Abstract / Article / BibTeX / DOI.

We equip labelled transition systems (LTSs) with unidirectional counters (UCs) which can be initialised to an arbitrary positive value and decremented but not incremented. This formalism, called UCLTSs, enables one to express fairness properties of concurrent systems in a finite form and reason about them in a compositional, refinement-based fashion. Technically, we first show how to apply CSP-style parallel composition and hiding directly on UCLTSs while maintaining compositionality. As our main result, we prove that the refinement checking of UCLTSs under the chaos-free failures-divergences semantics can be reduced to two decidable tasks that can be solved by the popular FDR2 and NuSMV model checkers, respectively.
Mühlberg, J. T. and Lüttgen, G. Symbolic object code analysis. In J. van de Pol and M. Weber, eds., 17th Intl. SPIN Workshop - Model Checking Software (SPIN 2010), vol. 6349 of Lecture Notes in Computer Science, pp. 4-21, Enschede, The Netherlands, September 2010, Springer-Verlag. Abstract / Article / BibTeX / DOI.

Current software model checkers quickly reach their limits when being applied to verifying pointer safety properties in source code that includes function pointers and inlined assembly. This paper introduces an alternative technique for checking pointer safety violations, called Symbolic Object Code Analysis (SOCA), which is based on bounded symbolic execution, incorporates path-sensitive slicing, and employs the SMT solver Yices as its execution and verification engine. Experimental results of a prototypic SOCA Verifier, using the Verisec suite and almost 10,000 Linux device driver functions as benchmarks, show that SOCA performs competitively to source-code model checkers and scales well when applied to real operating systems code and pointer safety issues.
De Roever, W.-P., Lüttgen, G. and Mendler, M. What is in a step: New Perspectives on a classical question. In Z. Manna and D. Peled, eds., Pnueli Festschrift, vol. 6200 of Lecture Notes in Computer Science, pp. 370-399, July 2010, Springer-Verlag. Abstract / Article / BibTeX / DOI.

In their seminal 1991 paper "What is in a Step: On the Semantics of Statecharts", Pnueli and Shalev showed how, in the presence of global consistency and while observing causality, the synchronous language Statecharts can be given coinciding operational and declarative step semantics. Over the past decade, this semantics has been supplemented with order-theoretic, denotational, axiomatic and game-theoretic characterisations, thus revealing itself as a rather canonical interpretation of the synchrony hypothesis.

In this paper, we survey these characterisations and use them to emphasise the close but not widely known relations of Statecharts to the synchronous language Esterel and to the field of logic programming. Additionally, we highlight some early reminiscences on Amir Pnueli's contributions to characterise the semantics of Statecharts.
Mühlberg, J. T. and Lüttgen, G. Verifying compiled file system code. In M. Vinicius, M. Oliveira and J. Woodcock, eds., 12th Brazilian Symposium on Formal Methods (SBMF 2009), vol. 5902 of Lecture Notes in Computer Science, pp. 306-320, Gramado, Brazil, August 2009, Springer-Verlag. Abstract / Article / BibTeX / DOI.

This paper presents a case study on retrospective verification of the Linux Virtual File System (VFS), which is aimed at checking for violations of API usage rules and memory properties. Since VFS maintains dynamic data structures and is written in a mixture of C and inlined assembly, modern software model checkers cannot be applied. Our case study centres around our novel, verification tool, the SOCA Verifier, which symbolically executes and analyses compiled code. We describe how this verifier deals with complex program features such as memory access, pointer aliasing and computed jumps, while reducing manual modelling to the bare minimum. Our results show that the SOCA Verifier is capable of reliably analysing complex operating system components such as the Linux VFS, thereby going beyond traditional testing tools and into niches that current software model checkers do not reach.
Fecher, H., de Frutos-Escrig, D., Lüttgen, G. and Schmidt, H. On the expressiveness of refinement settings. In F. Arbab and M. Sirjani, eds., 3rd Intl. Conf. on Fundamentals of Software Engineering (FSEN 2009), vol. 5961 of Lecture Notes in Computer Science, pp. 276-291, Kish Island, Iran, April 2009. Springer-Verlag. Abstract / Article / BibTeX / DOI.

Embedded-systems designers often use transition-system-based notations for specifying, with respect to some refinement preorder, sets of deterministic implementations. This paper compares popular such refinement settings - ranging from transition systems equipped with failure-pair inclusion to disjunctive modal transition systems - regarding the sets of implementations they are able to express. The paper's main result is an expressiveness hierarchy, as well as language-preserving transformations between various settings. In addition to system designers, the main beneficiaries of this work are tool builders who wish to reuse refinement checkers or model checkers across different settings.
Lüttgen, G. and Vogler, W. Safe reasoning with Logic LTS. In M. Nielsen, A. Kucera, P. Bro Miltersen, C. Palamidessi, P. Tuma and F. Valencia, eds., 35th Conf. on Current Trends in Theory and Practice of Computer Science (SOFSEM 2009), vol. 5404 of Lecture Notes in Computer Science, pp. 376-387, Spindleruv Mlyn, Czech Republic, January 2009. Springer-Verlag. Abstract / Article / BibTeX / DOI.

Previous work has introduced the setting of Logic LTS, together with a variant of ready simulation as fully-abstract refinement preorder, which allows one to compose operational specifications using a CSP-style parallel operator as well as the propositional connectives conjunction and disjunction. In this paper, we show how a temporal logic for specifying safety properties may be embedded into Logic LTS so that (a) the temporal operators are compositional for ready simulation and (b) ready simulation, when restricted to pairs of processes and formulas, coincides with the logic's satisfaction relation. The utility of this setting as a semantic foundation for mixed operational and temporal-logic specification languages is demonstrated via a simple example.
Galloway, A., Lüttgen, G., Mühlberg, J. T. and Siminiceanu, R. I. Model-checking the Linux Virtual File System. In N. Jones and M. Müller-Olm, eds., 10th Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI 2009), vol. 5403 of Lecture Notes in Computer Science, pp. 74-88, Savannah, Georgia, USA, January 2009. Springer-Verlag. Abstract / Article / BibTeX / DOI.

This paper presents a case study in modelling and verifying the Linux Virtual File System (VFS). Our work is set in the context of Hoare's verification grand challenge and, in particular, Joshi and Holzmann's mini-challenge to build a verifiable file system. The aim of the study is to assess the viability of retrospective verification of a VFS implementation using model-checking technology. We show how to extract an executable model of the Linux VFS implementation, validate the model by employing the simulation capabilities of SPIN, and analyse it for adherence to data integrity constraints and deadlock freedom using the SMART model checker.
Mendler, M. and Lüttgen, G. Is observational congruence axiomatisable in equational Horn logic? In L. Caires and V.T. Vasconcelos, eds., 18th Intl. Conf. on Concurrency Theory (CONCUR 2007), vol. 4703 of Lecture Notes in Computer Science, pp. 197-211, Lisbon, Portugal, September 2007. Springer-Verlag. Abstract / Article / BibTeX / DOI.

It is well known that bisimulation on mu-expressions cannot be finitely axiomatised in equational logic. Complete axiomatisations such as those of Milner and Bloom/Esik necessarily involve implicational rules. However, both systems rely on features which go beyond pure equational Horn logic: either the rules are impure by involving non-equational side-conditions, or they are schematically infinitary like the congruence rule which is not Horn. It is an open question whether these complications cannot be avoided in the proof-theoretically and computationally clean and powerful setting of second-order equational Horn logic.

This paper presents a positive and a negative result regarding axiomatisability of observational congruence in equational Horn logic. Firstly, we show how Milner's impure rule system can be reworked into a pure Horn axiomatisation that is complete for guarded processes. Secondly, we prove that for unguarded processes, both Milner's and Bloom/Esik's axiomatisations are incomplete without the congruence rule, and neither system has a complete extension in rank 1 equational axioms. It remains open whether there are higher-rank equational axioms or Horn rules which would render Milner's or Bloom/Esik's axiomatisations complete for unguarded processes.
Lüttgen, G. and Vogler, W. Ready simulation for concurrency: It's logical! In C. Cachin, T. Jurdzinski and A. Tarlecki, eds., 34th Intl. Colloquium on Automata, Languages and Programming (ICALP 2007), vol. 4596 of Lecture Notes in Computer Science, pp. 752-763, Wroclaw, Poland, July 2007. Springer-Verlag. Abstract / Article / BibTeX / DOI.

This paper provides new insight into the connection between the trace-based lower part of van Glabbeek's linear-time, branching-time spectrum and its simulation-based upper part. We establish that ready simulation is fully abstract with respect to failures inclusion, when adding the conjunction operator that was proposed by the authors in [TCS 373(1-2):19-40] to the standard setting of labelled transition systems with (CSP-style) parallel composition. More precisely, we actually prove a stronger result by considering a coarser relation than failures inclusion, namely a preorder that relates processes with respect to inconsistencies that may arise under conjunctive composition. Ready simulation is also shown to satisfy standard logic properties and thus commends itself for studying mixed operational and logic languages.
Ezekiel, J. and Lüttgen, G. Measuring and evaluating parallel state-space exploration algorithms. In I. Cerna and B. Haverkort, eds., 6th Intl. Workshop on Parallel and Distributed Methods in verifiCation (PDMC 2007), vol. 198(1) of Electronic Notes in Theoretical Computer Science, pp. 47-61, Berlin, Germany, July 2007. Elsevier Science. In press. Abstract / Article / BibTeX / DOI.

We argue in this paper that benchmarking should be complemented by direct measurement of parallelisation overheads when evaluating parallel state-space exploration algorithms. This poses several challenges that so far have not been addressed in the literature: what exactly are those overheads, how can and cannot they be measured, and how should system models be selected in order to expose the causes of parallelisation (in)efficiencies? We discuss and answer these questions based on our experience with parallelising Saturation - a symbolic algorithm for generating state-spaces of asynchronous system models - on a shared-memory architecture. Doing so will hopefully spare newcomers to the growing PDMC community from having to learn these lessons the hard way, as we did over a painful period of almost three years.
Ezekiel, J., Lüttgen, G. and Ciardo, G. Parallelising symbolic state-space generators. In W. Damm and H. Hermanns, eds., 19th Intl. Conf. on Computer Aided Verification (CAV 2007), vol. 4590 of Lecture Notes in Computer Science, pp. 268-280, Berlin, Germany, July 2007. Springer-Verlag. Abstract / Article / BibTeX / DOI.

Symbolic state-space generators are notoriously hard to parallelise, largely due to the irregular nature of the task. Parallel languages such as Cilk, tailored to irregular problems, have been shown to offer efficient scheduling and load balancing. This paper explores whether Cilk can be used to efficiently parallelise a symbolic state-space generator on a shared-memory architecture. We parallelise the Saturation algorithm implemented in the SMART verification tool using Cilk, and compare it to a parallel implementation of the algorithm using a thread pool. Our experimental studies on a dual-processor, dual-core PC show that Cilk can improve the run-time efficiency of our parallel algorithm due to its load balancing and scheduling efficiency. We also demonstrate that this incurs a significant memory overhead due to Cilk's inability to support pipelining, and conclude by pointing to a possible future direction for parallel irregular languages to include pipelining.
Ciardo, G., Lüttgen, G. and Yu, A. J. Improving static variable orders via invariants. In J. Kleijn and A. Yakovlev, eds., 28th Intl. Conf. on Application and Theory of Petri Nets and Other Models of Concurrency (ICATPN 2007), vol. 4546 of Lecture Notes in Computer Science, pp. 83-103, Siedlce, Poland, June 2007. Springer-Verlag. Abstract / Article / BibTeX / DOI.

Choosing a good variable order is crucial for making symbolic state-space generation algorithms truly efficient. One such algorithm is the MDD-based Saturation algorithm for Petri nets implemented in SMART, whose efficiency relies on exploiting event locality.

This paper presents a novel, static ordering heuristic that considers place invariants of Petri nets. In contrast to related work, we use the functional dependencies encoded by invariants to merge decision-diagram variables, rather than to eliminate them. We prove that merging variables always yields smaller MDDs and improves event locality, while eliminating variables may increase MDD sizes and break locality. Combining this idea of merging with heuristics for maximizing event locality, we obtain an algorithm for static variable order which outperforms competing approaches regarding both time-efficiency and memory-efficiency, as we demonstrate by extensive benchmarking.
Yu, A. J., Ciardo, G. and Lüttgen, G. Bounded reachability checking of asynchronous systems using decision diagrams. In O. Grumberg and M. Huth, eds., 13th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2007), vol. 4424 of Lecture Notes in Computer Science, pp. 648-663, Braga, Portugal, March 2007. Springer-Verlag. Abstract / Article / BibTeX / DOI.

Bounded reachability or model checking is widely believed to work poorly when using decision diagrams instead of SAT procedures. Recent research suggests this to be untrue with regards to synchronous systems, particularly digital circuits. This paper shows that the belief is also a myth for asynchronous systems, such as models specified by Petri nets. We propose Bounded Saturation, a new algorithm to compute bounded state spaces using Multi-way Decision Diagrams (MDDs). This is based on the established Saturation algorithm which benefits from a non-standard search strategy that is very different from breadth-first search. To bound Saturation, we employ Edge-Valued MDDs and rework its search strategy. Experimental results show that our algorithm often, but not always, compares favorably against two SAT-based approaches advocated in the literature for deadlock checking in Petri nets.
Ezekiel, J., Lüttgen, G. and Siminiceanu, R. Can Saturation be parallelised? On the parallelisation of a symbolic state-space generator. In L. Brim, B. Haverkort, M. Leucker and J. van de Pol, eds., 5th Intl. Workshop on Parallel and Distributed Methods in verifiCation (PDMC 2006), vol. 4346 of Lecture Notes in Computer Science, pp. 331-346, Bonn, Germany, August 2006. Springer-Verlag. Abstract / Article / BibTeX / DOI.

Symbolic state-space generators are notoriously hard to parallelise. However, the Saturation algorithm implemented in the SMART verification tool differs from other sequential symbolic state-space generators in that it exploits the locality of firing events in asynchronous system models.

This paper explores whether event locality can be utilised to efficiently parallelise Saturation on shared-memory architectures. Conceptually, we propose to parallelise the firing of events within a decision diagram node, which is technically realised via a thread pool. We discuss the challenges involved in our parallel design and conduct experimental studies on its prototypical implementation. On a dual-processor dual-core PC, our studies show speed-ups for several example models, e.g., of up to 50% for a Kanban model, when compared to running our algorithm only on a single core.
Mühlberg, J. T. and Lüttgen, G. BLASTing Linux code. In L. Brim, B. Haverkort, M. Leucker and J. van de Pol, eds., 11th Intl. Workshop on Formal Methods for Industrial Critical Systems (FMICS 2006), vol. 4346 of Lecture Notes in Computer Science, pp. 211-226, Bonn, Germany, August 2006. Springer-Verlag. Abstract / Article / BibTeX / DOI.

Computer programs can only run reliably if the underlying operating system is free of errors. In this paper we evaluate, from a practitioner's point of view, the utility of the popular software model checker BLAST for revealing errors in Linux kernel code. The emphasis is on important errors related to memory safety in and locking behaviour of device drivers. Our conducted case studies show that, while BLAST's abstraction and refinement techniques are efficient and powerful, the tool has deficiencies regarding usability and support for analysing pointers, which are likely to prevent kernel developers from using it.
Lüttgen, G. and Vogler, W. Conjunction on processes: Full-abstraction via ready-tree semantics. In L. Aceto and A. Ingólfsdóttir, eds., 9th Intl. Conf. on Foundations of Software Science and Computation Structures (FOSSACS 2006), vol. 3921 of Lecture Notes in Computer Science, pp. 261-276, Vienna, Austria, April 2006. Springer-Verlag. Abstract / Article / BibTeX / DOI.

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 paper introduces a conjunction operator on labelled transition systems capturing the basic intuition of "a and b = false", and considers a naive preorder that demands that an inconsistent specification can only be refined by an inconsistent implementation.

The main body of the paper is concerned with characterising the largest precongruence contained in the naive preorder. This characterisation will be 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 paper's results provide a foundation for, and an important step towards a unified framework that allows one to freely mix operators from process algebras and temporal logics.
Lüttgen, G. and Vogler, W. Bisimulation on speed: A unified approach. In V. Sassone, ed., 8th Intl. Conf. on Foundations of Software Science and Computation Structures (FOSSACS 2005), vol. 3441 of Lecture Notes in Computer Science, pp. 79-94, Edinburgh, Scotland, April 2005. Springer-Verlag. Abstract / Article / BibTeX / DOI.

Two process-algebraic approaches have been developed for comparing two bisimulation-equivalent processes with respect to speed: the one of Moller-Tofts equips actions with lower time bounds, while the one by Lüttgen-Vogler considers upper time bounds instead.

This paper sheds new light on both approaches by testifying to their close relationship. We introduce a general, intuitive concept of "faster-than", which is formalised by a notion of amortised faster-than preorder. When closing this preorder under all contexts, exactly the two faster-than preorders investigated by Moller/Tofts and Lüttgen/Vogler arise. For processes incorporating both lower and upper time bounds we also show that the largest precongruence contained in the amortised faster-than preorder is not a proper preorder but a timed bisimulation. In the light of this result we systematically investigate under which circumstances the amortised faster-than preorder degrades to an equivalence.
Lüttgen, G. and Vogler, W. Bisimulation on speed: Lower time bounds. In I. Walukiewicz, ed., 7th Intl. Conf. on Foundations of Software Science and Computation Structures (FOSSACS 2004), vol. 2987 of Lecture Notes in Computer Science, pp. 333-347, Barcelona, Spain, April 2004. Springer-Verlag. Abstract / Article / BibTeX / DOI.

More than a decade ago, Moller and Tofts published their seminal work on relating processes that are annotated with lower time bounds, with respect to speed. Their paper has left open many questions concerning the semantic theory for their suggested bisimulation-based faster-than preorder, the MT-preorder, which have not been addressed since. The encountered difficulties concern a general compositionality result, a complete axiom system for finite processes, and a convincing intuitive justification of the MT-preorder.

This paper solves these difficulties by developing and employing novel tools for reasoning in discrete-time process algebra, in particular a general commutation lemma relating the sequencing of action and clock transitions. Most importantly, it is proved that the MT-preorder is fully-abstract with respect to a natural amortized preorder that uses a simple bookkeeping mechanism for deciding whether one process is faster than another. Together these results reveal the intuitive roots of the MT-preorder as a faster-than relation, while testifying to its semantic elegance. This lifts some of the barriers that have so far hampered progress in semantic theories for comparing the speed of processes.
Norton, B., Lüttgen, G. and Mendler, M. A Compositional semantic theory for synchronous component-based design. In R. Amadio and D. Lugiez, eds., 14th Intl. Conf. on Concurrency Theory (CONCUR 2003), vol. 2761 of Lecture Notes in Computer Science, pp. 461-476, Marseille, France, September 2003. Springer-Verlag. Abstract / Article / BibTeX / DOI.

Digital signal processing and control (DSPC) tools 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 paper develops a process-algebraic model of coordination for synchronous component-based design, which directly lends itself to compositionally formalising the monolithic semantics of DSPC tools. By uniformly combining the well-known concepts of abstract clocks, maximal progress and clock-hiding, it is shown how the DSPC principles of dynamic synchronous scheduling, isochrony and encapsulation may be captured faithfully and compositionally in process algebra, and how observation equivalence may facilitate jam checks at compile-time.
Aguado, J., Lüttgen, G. and Mendler, M. A-maze-ing Esterel. In A. Girault, F. Maraninchi and E. Rutten, eds., Intl. Workshop on Synchronous Languages, Applications, and Programming (SLAP 2003), vol. 88 of Electronic Notes in Theoretical Computer Science, Porto, Portugal, July 2003. Elsevier Science. Abstract / Article / BibTeX.

This paper shows that the kernel fragment of Esterel corresponding to combinational circuits admits a natural game-theoretic interpretation. Technically, combinational Esterel programs are mapped into finite two-player games in such a way that the standard must- and cannot-analysis of signal statuses is reflected in the computation of winning strategies. The novel game-theoretic approach complements the existing behavioral, operational, circuit-based, and model-theoretic accounts of Esterel's semantics and offers a new didactic perspective for familiarizing students and engineers with this intricate constructive semantics.
Lüttgen, G. and Mendler, M. Axiomatizing an algebra of step reactions for synchronous languages. In L. Brim, P. Jancar, M. Kretinsky and A. Kucera, eds., 13th Intl. Conf. on Concurrency Theory (CONCUR 2002), vol. 2421 of Lecture Notes in Computer Science, pp. 386-401, Brno, Czech Republic, August 2002. Springer-Verlag. Abstract / Article / BibTeX / DOI.

This paper introduces a novel algebra for reasoning about step reactions in synchronous languages, such as macro steps in Harel, Pnueli and Shalev's Statecharts and instantaneous reactions in Berry's Esterel. The algebra describes step reactions in terms of configurations which can both be read in a standard operational as well as in a model-theoretic fashion. The latter arises by viewing configurations as propositional formulas, interpreted intuitionistically over finite linear Kripke structures. Previous work by the authors showed the adequacy of this approach by establishing compositionality and full-abstraction results for Statecharts and Esterel. The present paper generalizes this work in an algebraic setting and, as its main result, provides a sound and complete equational axiomatization of step reactions. This yields, for the first time in the literature, a complete axiomatization of Statecharts macro steps, which can also be applied, modulo encoding, to Esterel reactions.
Cleaveland, R. and Lüttgen, G. A logical process calculus. In U. Nestmann and P. Panangaden, eds., 9th Intl. Workshop on Expressiveness in Concurrency (EXPRESS 2002), vol. 68, no. 2 of Electronic Notes in Theoretical Computer Science, Brno, Czech Republic, August 2002. Elsevier Science. Abstract / Article / BibTeX.

This paper presents the Logical Process Calculus (LPC), a formalism that supports heterogeneous system specifications containing both operational and declarative subspecifications. Syntactically, LPC extends Milner's Calculus of Communicating Systems with operators from the alternation-free linear-time mu-calculus (LTmu). Semantically, LPC is equipped with a behavioral preorder that generalizes Hennessy's and De Nicola's must-testing preorder as well as LTmu's satisfaction relation, while being compositional for all LPC operators.

From a technical point of view, the new calculus is distinguished by the inclusion of (i) both minimal and maximal fixed-point operators and (ii) an unimplementability predicate on process terms which tags inconsistent specifications. The utility of LPC is demonstrated by means of an example highlighting the benefits of heterogeneous system specification.
Lüttgen, G. and Mendler, M. Towards a model-theory for Esterel. In F. Maraninchi, A. Girault and E. Rutten, eds., Intl. Workshop on Synchronous Languages, Applications, and Programming (SLAP 2002), vol. 65, no. 5 of Electronic Notes in Theoretical Computer Science, Grenoble, France, April 2002. Elsevier Science. Abstract / Article / BibTeX.

Esterel is a synchronous language for reactive-systems design and builds the core of the commercial tool Esterel Studio. This paper shows how the constructive semantics of a combinational fragment of Esterel, as presented by Berry, can be derived in a model-theoretic fashion, thus complementing the existing behavioral, operational, and circuit-based approaches to Esterel semantics. Technically, Esterel programs are read as formulas in propositional intuitionistic logic, which are interpreted over simple linear Kripke structures, referred to as Gödel valuations. Esterel reactions are then characterized as specific Gödel valuations, called response models, and it is shown that the approach is compositional in the structure of Esterel programs.

The obtained results are an important step towards explaining the logic behind Esterel semantics. In addition, the intuitionistic setting advocated in this paper nicely links to Pnueli and Shalev's semantics of Harel's Statecharts, another synchronous language for reactive-system design. This offers interesting insights into the similarities of and the differences between Esterel and Statecharts semantics.
Lüttgen, G. and Mendler, M. Statecharts: From visual syntax to model-theoretic semantics. In K. Bauknecht, W. Brauer and Th. Mück, eds., GI Workshop on Integrating Diagrammatic and Formal Specification Techniques, pp. 615-621, Vienna, Austria, September 2001. Austrian Computer Society. Abstract / Article / BibTeX.

This paper presents a novel model-theoretic account of Harel, Pnueli and Shalev's original step semantics of the visual specification language Statecharts. The graphical syntax of a Statechart is read, directly and structurally, as a formula in propositional logic. This proposition captures all the logical constraints imposed by the diagram on the Statechart's semantics, i.e., the possible sets of transitions that can be taken together to perform a valid Statecharts step, and their effects on Statecharts configurations. The paper's main result shows that the correct semantics is uniquely described by the intuitionistic interpretation of Statecharts formulas, whereas the naive classical interpretation is insufficient.

The advocated intuitionistic approach not only gives a correct, clear and direct logical account of Statecharts' semantics, but also permits the integration of Statecharts with formal validation tools, such as theorem provers.
Lüttgen, G. and Vogler, W. A faster-than relation for asynchronous processes. In K. G. Larsen and M. Nielsen, eds., 12th Intl. Conf. on Concurrency Theory (CONCUR 2001), vol. 2154 of Lecture Notes in Computer Science, pp. 262-276, Aalborg, Denmark, August 2001. Springer-Verlag. Abstract / Article / BibTeX / DOI.

This paper introduces a novel (bi)simulation-based faster-than preorder which relates asynchronous processes with respect to their worst-case timing behavior. The studies are conducted for a conservative extension of the process algebra CCS, called TACS, which permits the specification of maximal time bounds of actions. The most unusual contribution is in showing that the proposed faster-than preorder coincides with two other preorders, one of which considers the absolute times at which actions occur in system runs. The paper also develops the semantic theory of TACS, addressing congruence properties, equational laws, and abstractions from internal actions.
Ciardo, G., Lüttgen, G. and Siminiceanu, R. Saturation: An efficient iteration strategy for symbolic state-space generation. In T. Margaria and W. Yi, eds., 7th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2001), vol. 2031 of Lecture Notes in Computer Science, pp. 328-342, Genova, Italy, April 2001. Springer-Verlag. Abstract / Article / BibTeX / DOI.

We present a novel algorithm for generating state spaces of asynchronous systems using Multi-valued Decision Diagrams. In contrast to related work, we encode the next-state function of a system not as a single Boolean function, but as cross-products of integer functions. This permits the application of various iteration strategies to build a system's state space. In particular, we introduce a new elegant strategy, called saturation, and implement it in the tool SMART. On top of usually performing several orders of magnitude faster than existing BDD-based state-space generators, our algorithm's required peak memory is often close to the final memory needed for storing the overall state space.
Cleaveland, R. and Lüttgen, G. A semantic theory for heterogeneous system design. In S. Kapoor and S. Prasad, eds., 20th Conf. on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2000), vol. 1974 of Lecture Notes in Computer Science, pp. 312-324, New Delhi, India, December 2000. Springer-Verlag. Abstract / Article / BibTeX / DOI.

This paper extends De Nicola and Hennessy's testing theory from labeled transition system to Büchi processes and establishes a tight connection between the resulting Büchi must-preorder and satisfaction of linear-time temporal logic (LTL) formulas. An example dealing with the design of a communications protocol testifies to the utility of the theory for heterogeneous system design, in which some components are specified as labeled transition systems and others are given as LTL formulas.
Lüttgen, G., von der Beeck, M. and Cleaveland, R. A compositional approach to Statecharts semantics. In ACM/SIGSOFT 8th Intl. Symposium on Foundations of Software Engineering (FSE 2000), vol. 25, no. 6 of ACM Software Engineering Notes, pp. 120-129, San Diego, California, November 2000. ACM Press. Abstract / Article / BibTeX/ DOI.

Statecharts is a visual language for specifying reactive system behavior. The formalism extends traditional finite-state machines with notions of hierarchy and concurrency, and it is used in many popular software design notations. A large part of the appeal of Statecharts derives from its basis in state machines, with their intuitive operational interpretation. The classical semantics of Statecharts, however, suffers from a serious defect: it is not compositional, meaning that the behavior of system descriptions cannot be inferred from the behavior of their subsystems. Compositionality is a prerequisite for exploiting the modular structure of Statecharts for simulation, verification, and code generation, and it also provides the necessary foundation for reusability.

This paper suggests a new compositional approach to formalizing Statecharts semantics as flattened labeled transition systems in which transitions represent system steps. The approach builds on ideas developed for timed process calculi and employs structural operational rules to define the transitions of a Statecharts expression in terms of the transitions of its subexpressions. It is first presented for a simple dialect of Statecharts, with respect to a variant of Pnueli and Shalev's semantics, and is illustrated by means of a small example. To demonstrate its flexibility, the proposed approach is then extended to deal with practically useful features available in many Statecharts variants, namely state references, history states, and priority concepts along state hierarchies.
Lüttgen, G. and Mendler, M. Fully-abstract Statecharts semantics via intuitionistic Kripke models. In U. Montanari, J. Rolim and E. Welzl, eds., 27th Intl. Colloquium on Automata, Languages and Programming (ICALP 2000), vol. 1853 of Lecture Notes in Computer Science, pp. 163-174, Geneva, Switzerland, July 2000. Springer-Verlag. Abstract / Article / BibTeX / DOI.

The semantics of Statecharts macro steps, as introduced by Pnueli and Shalev, lacks compositionality. This paper first analyzes the compositionality problem and traces it back to the invalidity of the Law of the Excluded Middle. It then characterizes the semantics via a particular class of linear, intuitionistic Kripke models, namely stabilization sequences. This yields, for the first time in the literature, a simple fully-abstract semantics which interprets Pnueli and Shalev's concept of failure naturally. The results not only give insights into the semantic subtleties of Statecharts, but also provide a basis for developing algebraic theories for macro steps and for comparing different Statecharts variants.
Ciardo, G., Lüttgen, G. and Siminiceanu, R. Efficient symbolic state-space construction for asynchronous systems. In M. Nielsen and D. Simpson, eds., 21st Intl. Conf. on Application and Theory of Petri Nets (ICATPN 2000), vol. 1839 of Lecture Notes in Computer Science, pp. 103-122, Aarhus, Denmark, June 2000. Springer-Verlag. Abstract / Article / BibTeX / DOI.

Many techniques for the verification of reactive systems rely on the analysis of their reachable state spaces. In this paper, a new algorithm for the symbolic generation of the state spaces of asynchronous system models, such as Petri nets, is developed. The algorithm is based on previous work that employs Multi-valued Decision Diagrams for efficiently storing sets of reachable states. In contrast to related approaches, however, it fully exploits event locality, 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.
Lüttgen, G. and Carreño, V. Analyzing mode confusion via model checking. In D. Dams, R. Gerth, S. Leue and M. Massink, eds., Intl. Workshop on Theoretical and Practical Aspects of SPIN Model Checking (SPIN '99), vol. 1680 of Lecture Notes in Computer Science, pp. 120-135, Toulouse, France, September 1999. Springer-Verlag. Abstract / Article / BibTeX / DOI.

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. NASA explores how formal methods, especially theorem proving, can be used to discover mode confusion. The present paper investigates whether state-exploration techniques, e.g., model checking, are better able to achieve this task than theorem proving and also to compare the verification tools Murphi, SMV, and Spin for the specific application. While all tools can handle the task well, their strengths are complementary.
Lüttgen, G., von der Beeck, M. and Cleaveland, R. Statecharts via process algebra. In J. C. M. Baeten and S. Mauw, eds., 10th Intl. Conf. on Concurrency Theory (CONCUR '99), vol. 1664 of Lecture Notes in Computer Science, pp. 399-414, Eindhoven, The Netherlands, August 1999. Springer-Verlag. Abstract / Article / BibTeX / DOI.

Statecharts is a visual language for specifying the behavior of reactive systems. The language extends finite-state machines with concepts of hierarchy, concurrency, and priority. Despite its popularity as a design notation for embedded systems, precisely defining its semantics has proved extremely challenging. In this paper, we present a simple process algebra, called Statecharts Process Language (SPL), which is expressive enough for encoding Statecharts in a structure-preserving and semantics-preserving manner. We also establish that the behavioral equivalence bisimulation, when applied to SPL, preserves Statecharts semantics.
Bhat, G., Cleaveland, R. and Lüttgen, G. Dynamic priorities for modeling real-time. In T. Mizuno, N. Shiratori, T. Higashino and A. Togashi, eds., Intl. Conf. on Formal Description Techniques and Protocol Specification, Testing and Verification (FORTE X/PSTV XVII), pp. 321-336, Osaka, Japan, November 1997. Chapman & Hall. Abstract / Article / BibTeX.

This paper describes an approach for modeling real-time systems using dynamic priorities. The advantage of the technique is that it drastically reduces the state space sizes of the systems in question while preserving properties of their functional behavior. We demonstrate the utility of our approach by formally modeling and verifying aspects of the widely-used SCSI-2 bus-protocol. It turns out that the state space of this model is about an order of magnitude smaller than the one resulting from traditional real-time semantics.
Cleaveland, R., Lüttgen, G. and Mendler, M. An algebraic theory of multiple clocks. In A. Mazurkiewicz and J. Winkowski, eds., 8th Intl. Conf. on Concurrency Theory (CONCUR '97), vol. 1243 of Lecture Notes in Computer Science, pp. 166-180, Warsaw, Poland, July 1997. Springer-Verlag. Abstract / Article / BibTeX.

This paper develops a temporal process algebra, CSA, for reasoning about distributed systems that involve qualitative timing constraints. It is a conservative extension of Milner's CCS that combines the idea of multiple clocks from the algebra PMC with the assumption of maximal progress familiar from timed process algebras such as TPL. Using a typical class of examples drawn from hardware design, we motivate why these features are useful and in some cases necessary for modeling and verifying distributed systems. We also present fully-abstract behavioral congruences based on the notion of strong bisimulation and observational equivalence, respectively. For temporal strong bisimulation we give sound and complete axiomatizations for classes of processes.
Cleaveland, R., Lüttgen, G. and Natarajan, V. A process algebra with distributed priorities. In U. Montanari and V. Sassone, eds., 7th Intl. Conf. on Concurrency Theory (CONCUR '96), vol. 1119 of Lecture Notes in Computer Science, pp. 34-49, Pisa, Italy, August 1996. Springer-Verlag. Abstract / Article / BibTeX.

This paper presents a process algebra for distributed systems in which some actions may take precedence over others. In contrast with existing approaches to priorities, our algebra only allows actions to pre-empt others at the same "location" and therefore captures a notion of localized precedence. Using Park's and Milner's notion of strong bisimulation as a basis, we develop a behavioral congruence and axiomatize it for finite processes; we also derive an associated observational congruence. Simple examples highlight the utility of the theory.
Geser, A., Lüttgen, G., Knoop, J., Rüthing, O. and Steffen, B. Non-monotone fixpoint iterations to resolve second order effects. In T. Gyimóthy, ed., 6th Intl. Symp. on Compiler Construction (CC '96), vol. 1060 of Lecture Notes in Computer Science, pp. 106-120, Linköping, Sweden, April 1996. Springer-Verlag. Abstract / Article / BibTeX.

We present a new fixpoint theorem which guarantees the existence and the finite computability of the least common solution of a countable system of recursive equations over a wellfounded domain. The functions are only required to be increasing and delay-monotone, the latter being a property much weaker than monotonicity. We hold that wellfoundedness is a natural condition as it guarantees termination of every fixpoint computation algorithm. Our fixpoint theorem covers, under the wellfoundedness condition, all the known "synchronous" versions of fixpoint theorems. To demonstrate its power and versatility we contrast an application in data flow analysis, where known versions are applicable as well, to a practically relevant application in program optimization, which due to its second order effects, requires the full strength of our new theorem. In fact, the new theorem is central for establishing the optimality of the partial dead code elimination algorithm considered, which is implemented in the new release of the Sun SPARCompiler language systems.
Cleaveland, R., Lüttgen, G., Natarajan, V. and Sims, S. Priorities for modeling and verifying distributed systems. In T. Margaria and B. Steffen, eds., 2nd Intl. Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '96), vol. 1055 of Lecture Notes in Computer Science, pp. 278-297, Passau, Germany, March 1996. Springer-Verlag. Abstract / Article / BibTeX.

This paper illustrates the use of priorities in process algebras by a real-world example dealing with the design of a safety-critical network which is part of a railway signaling scheme. Priorities in process algebras support an intuitive modeling of distributed systems since undesired interleavings can be suppressed. This fact also leads to a substantial reduction in the sizes of models. We have implemented a CCS-based process algebra with priorities as a new front-end for the NCSU Concurrency Workbench, and we use model checking for verifying properties of the signaling system.

^ Top

Editorial Duties

Lüttgen, G. and Corradini, F., eds. Comprehending Asynchrony in Specification and Analysis (Festschrift Walter Vogler). Special issue of Acta Informatica, 52(2-3):107-108, April 2015. Preface / BibTeX / DOI.
Lüttgen, G. and Merz, S., eds. Automated Verification of Critical Systems (AVOCS'12). Special issue of Science of Computer Programming, 96(3):277-278, December 2014. Preface / BibTeX / DOI.
Lüttgen, G. and Merz, S., eds. 12th Intl. Workshop on Automated Verification of Critical Systems (AVoCS 2012). Electronic Communications of the EASST, vol. 53, December 2012. Preface / BibTeX / Open Access.
Černá, I. and Lüttgen, G., eds. 7th Intl. Workshop on Parallel and Distributed Methods in verifiCation (PDMC 2008). Electronic Notes in Theoretical Computer Science, vol. 120, issue 2, pp. 1-2, December 2008. Preface / BibTeX / DOI.
Lüttgen, G., Martinez-Madrid, N. and Mendler, M., eds. 2nd Intl. Workshop on Semantic Foundations of Engineering Design Languages (SFEDL 2004). Electronic Notes in Theoretical Computer Science, vol. 115, January 2005. Editorial / BibTeX / DOI.
Broy, M., Lüttgen, G. and Mendler, M., eds. Semantic Foundations of Engineering Design Languages (Part II). Special issue of Formal Aspects of Computing 16(3):165-312, August 2004. Editorial / BibTeX / DOI.
Broy, M., Lüttgen, G. and Mendler, M., eds. Semantic Foundations of Engineering Design Languages (Part I). Special issue of Formal Aspects of Computing 15(4):297-422, December 2003. Editorial / BibTeX / DOI
Lüttgen, G., Maraninchi, F. and Mendler, M., eds. 1st Intl. Workshop on Semantic Foundations of Engineering Design Languages (SFEDL 2002). VERIMAG Workshop Proceedings Series, Grenoble, France, April 2002. Editorial / BibTeX.

^ Top

Technical Reports & Contractor Reports

Yip, E., Lalo, E., Lüttgen, G., Deubzer, M. and Sailer, A. Optimized buffering of time-triggered automotive software. Technical Report No. 103/2018, Faculty of Information Systems and Applied Computer Sciences, University of Bamberg, Germany, September 2018. Abstract / Article / BibTeX.

The development of an automotive system involves the integration of many real-time software functionalities, and it is of utmost importance to guarantee strict timing requirements. However, the recent trend towards multi-core architectures poses significant challenges for the timely transfer of signals between processor cores so as to not violate data consistency.

We have studied and adapted an existing buffering mechanism to work specifically for statically scheduled time-triggered systems, called static buffering protocol. We developed further buffering optimisation algorithms and heuristics, to reduce the memory consumption, processor utilisation, and end-to-end response times of time-triggered AUTOSAR designs on multi-core platforms. Our contributions are important because they enable deterministic time-triggered implementations to become competitive alternatives to their inherently non-deterministic event-triggered counterparts. We have prototyped a selection of optimisations in an industrial tool and evaluated them on realistic industrial automotive benchmarks.
Fendrich, S. and Lüttgen, G. A generalised theory of Interface Automata, component compatibility and error. Technical Report No. 98/2016, Faculty of Information Systems and Applied Computer Sciences, University of Bamberg, Germany, March 2016. Abstract / Article / BibTeX.

Interface theories allow systems designers to reason about the composability and compatibility of concurrent system components. Such theories often extend both de Alfaro and Henzinger's Interface Automata and Larsen's Modal Transition Systems, which leads, however, to several issues that are undesirable in practice: an unintuitive treatment of specied unwanted behaviour, a binary compatibility concept that does not scale to multi-component assemblies, and compatibility guarantees that are insufficient for software product lines.

In this paper we show that communication mismatches are central to all these problems and, thus, the ability to represent such errors semantically is an important feature of an interface theory. Accordingly, we present the error-aware interface theory EMIA, where the above shortcomings are remedied by introducing explicit fatal error states. In addition, we prove via a Galois insertion that EMIA is a conservative generalisation of the established MIA (Modal Interface Automata) theory.
Bujtor, F., Fendrich, S., Lüttgen, G. and Vogler, W. Nondeterministic Modal Interfaces. Technical Report No. 2014-06, Computer Science Institute, University of Augsburg, Germany, October 2014. Abstract / Article / BibTeX.

Interface theories are employed in the component-based design of concurrent systems. They often emerge as combinations of Interface Automata (IA) and Modal Transition Systems (MTS), e.g., Nyman et al.'s IOMTS, Bauer et al.'s MIO, Raclet et al.'s MI or our MIA. In this paper, we generalise MI to nondeterministic interfaces, for which we resolve the longstanding conflict between unspecified inputs being allowed in IA but forbidden in MTS. With this solution we achieve, in contrast to related work, an associative parallel composition, a compositional preorder, a conjunction on interfaces with dissimilar alphabets supporting perspective-based specifications, and a quotienting operator for decomposing nondeterministic specifications in a single theory.
Mühlberg, J. T. and Lüttgen, G. Symbolic Object Code Analysis. Technical Report No. 85/2010, Faculty of Information Systems and Applied Computer Sciences, University of Bamberg, Germany, February 2010. Abstract / Article / BibTeX.

Current software model checkers quickly reach their limit when being applied to verifying pointer safety properties in source code that includes function pointers and inlined assembly. This paper introduces an alternative technique for checking pointer safety violations, called Symbolic Object Code Analysis (SOCA), which is based on bounded symbolic execution, incorporates path-sensitive slicing, and employs the SMT solver Yices as its execution and verification engine. Extensive experimental results of a prototypic SOCA Verifier, using the Verisec suite and almost 10,000 Linux device driver functions as benchmarks, show that SOCA performs competitively to current source-code model checkers and that it also scales well when applied to real operating systems code and pointer safety issues. SOCA effectively explores semantic niches of software that current software verifiers do not reach.
Lüttgen, G. and Vogler, W. Safe reasoning with Logic LTS. Technical Report No. 2008-18, Computer Science Institute, University of Augsburg, Germany, November 2008. Abstract / Article / BibTeX.

Previous work has introduced the setting of Logic LTS, together with a variant of ready simulation as fully-abstract refinement preorder, which allows one to compose operational specifications using a CSP-style parallel operator as well as the propositional connectives conjunction and disjunction. In this paper, we show how a temporal logic for specifying safety properties may be embedded into Logic LTS so that (a) the temporal operators are compositional for ready simulation and (b) ready simulation, when restricted to pairs of processes and formulas, coincides with the logic's satisfaction relation. The utility of this setting as a semantic foundation for mixed operational and temporal-logic specification languages is demonstrated via a simple example.
Galloway, A., Mühlberg, J. T., Siminiceanu, R. and Lüttgen, G. Model-checking part of a Linux file system. Technical Report YCS-2007-423, Department of Computer Science, University of York, England, November 2007. Abstract / Article / BibTeX.

We present our experiences with model checking part of a Linux file system. The work is set in the context of Hoare's verification grand challenge, and, in particular, Joshi and Holzmann's mini-challenge to build a verifiable file system. The primary aim of the work was to construct a larger scale case study upon which to measure our own research into model-checking technology. However, the choice of case study material was influenced by the aforementioned mini-challenge. The secondary aim of the work was to add to the existing confidence in the Linux code, for example by "testing" improbable situations through exhaustive model checking. Two models were produced: a Promela model, which was analysed using SPIN, and a Petri-Net-based model, which was analysed using versions of the SMART model-checker. The approach adopted was incremental, initially focussing on the basic functions of Linux's Virtual File Systems layer. The report presents intermediate results.
Ezekiel, J., Lüttgen, G. and Siminiceanu, R. I. An anticipated firing Saturation algorithm for shared-memory architectures. Technical Report YCS-2007-422, Department of Computer Science, University of York, England, November 2007. Abstract / Article / BibTeX.

Parallelising symbolic state-space generation algorithms, such as Saturation, is known to be difficult as it often incurs high parallel overheads. To improve efficiency, related work on a distributed-memory implementation of Saturation proposed using idle processors for speculatively firing events and caching the obtained results, in the hope that these results will be needed lateron.

This paper investigates a variant of this anticipated firing approach for shared-memory architectures, such as multi-core PCs. Rather than parallelising Saturation, the idea is to run the sequential Saturation algorithm on one core, while the others are given speculative work. Since computing the optimal strategy for selecting useful work is likely to be an NP-complete problem, the paper devises and implements various heuristics. The obtained experimental results show that moderate speed-ups can be achieved as a result of using anticipated firing. However, the proposed heuristics require further work in order to be truly useful in practice.
Mühlberg, J. T. and Lüttgen, G. BLASTing Linux code. Technical Report YCS-2007-417, Department of Computer Science, University of York, England, June 2007. Abstract / Article / BibTeX.

Computer programs can only run reliably if the underlying operating system is free of errors. In this paper we evaluate, from a practitioner's point of view, the utility of the popular software model checker BLAST for revealing errors in Linux kernel code. The emphasis is on important errors related to memory safety in and locking behaviour of device drivers. Our conducted case studies show that, while BLAST's abstraction and refinement techniques are efficient and powerful, the tool has deficiencies regarding usability and support for analysing pointers, which are likely to prevent kernel developers from using it.
Mendler, M. and Lüttgen, G. Is observational congruence on mu-expressions axiomatisable in equational Horn logic? Technical Report No. 72/2007, Faculty of Information Systems and Applied Computer Sciences, University of Bamberg, Germany, June 2007. Abstract / Article / BibTeX.

It is well known that bisimulation on mu-expressions cannot be finitely axiomatised in equational logic. Complete axiomatisations such as those of Milner and Bloom/Esik necessarily involve implicational rules. However, both systems rely on features which go beyond pure equational Horn logic: either the rules are impure by involving non-equational side-conditions, or they are schematically infinitary like the congruence rule which is not Horn. It is an open question whether these complications cannot be avoided in the proof-theoretically and computationally clean and powerful setting of second-order equational Horn logic.

This paper presents a positive and a negative result regarding axiomatisability of observational congruence in equational Horn logic. Firstly, we show how Milner's impure rule system can be reworked into a pure Horn axiomatisation that is complete for guarded processes. Secondly, we prove that for unguarded processes, both Milner's and Bloom/Esik's axiomatisations are incomplete without the congruence rule, and neither system has a complete extension in rank 1 equational axioms. It remains open whether there are higher-rank equational axioms or Horn rules which would render Milner's or Bloom/Esik's axiomatisations complete for unguarded processes.
Lüttgen, G. and Vogler, W. Ready simulation for concurrency: It's logical! Technical Report No. 2007-04, Computer Science Institute, University of Augsburg, Germany, April 2007. Abstract / Article / BibTeX.

This paper provides new insight into the connection between the trace-based lower part of van Glabbeek's linear-time, branching-time spectrum and its simulation-based upper part. We establish that ready simulation is fully abstract with respect to failures inclusion, when adding the conjunction operator that was proposed by the authors in [TCS 373(1-2):19-40] to the standard setting of labelled transition systems with (CSP-style) parallel composition. More precisely, we actually prove a stronger result by considering a coarser relation than failures inclusion, namely a preorder that relates processes with respect to inconsistencies that may arise under conjunctive composition. Ready simulation is also shown to satisfy standard logic properties and thus commends itself for studying mixed operational and logic languages.
Ezekiel, J., Lüttgen, G. and Siminiceanu, R. A parallel saturation algorithm on shared memory architectures. Technical Report 2007-01, National Institute of Aerospace, Virginia, January 2007. Abstract / Article / BibTeX.

Symbolic state-space generators are notoriously hard to parallelize. However, the Saturation algorithm implemented in the SMART verication tool differs from other sequential symbolic state-space generators in that it exploits the locality of firing events in asynchronous system models.

This paper explores whether event locality can be utilized to efficiently parallelize Saturation on shared-memory architectures. Conceptually, we propose to parallelize the firing of events within a decision diagram node, which is technically realized via a thread pool. We discuss the challenges involved in our parallel design and conduct experimental studies on its prototypical implementation. On a dual-processor dual-core PC, our studies show speed-ups for several example models, e.g., of up to 50% for a Kanban model, when compared to running our algorithm only on a single core.
Cataño, N. and Lüttgen, G. Enforcing correct programming of libraries: A case study on hash tables. Technical Report YCS-2006-406, Department of Computer Science, University of York, England, July 2006. Abstract / Article / BibTeX.

This paper presents the formalisation and correctness proofs of large parts of a hash table library used to represent multi-valued de- cision diagrams (MDDs). This data structure is used, for instance, in Saturation, a non-trivial algorithm used to store state spaces of asyn- chronous systems. We have conducted the correctness proofs of the main functionalities of the hash table in PVS. We outline a proof approach that can be re-used by practitioners interested in using formal methods to check their applications. We show how PVS can be used to discover inconsistencies in the implementation of an application, or to improve it.
Lüttgen, G. Formal verification & its role in testing. Technical Report YCS-2006-400, Department of Computer Science, University of York, England, May 2006. Abstract / Article / BibTeX.

This report surveys the role of formal verification techniques, especially model checking, in the testing of computer systems. While formal verification and testing have traditionally been perceived as disparate fields, recent research has brought them considerably closer together.
Atiya, D., Cataño, N. and Lüttgen, G. Towards a benchmark for model checkers of asynchronous concurrent systems. Technical Report YCS-2006-399, Department of Computer Science, University of York, England, April 2006. Abstract / Article / BibTeX.

Benchmarks, such as the established ISCAS benchmarks of digital circuits, have been successfully used to compare the relative merits of many model-checking tools and techniques employed for verifying synchronous systems. However, no benchmark for model checkers of asynchronous concurrent systems, such as communications protocols and distributed controllers, currently exists. This not only prevents a transparent evaluation of technologies in the field, but also hinders the accumulation and communication of insights into why and where particular technologies work better than others.

This paper takes a first step towards establishing a benchmark for asynchronous concurrent systems. It first discusses the underlying challenges when dealing with model-checking technologies for such systems. A prototype benchmark is then proposed, which is the result of an extensive survey and systematic classification of asynchronous concurrent systems studied in the literature. Finally, the proposed benchmark is evaluated against an established benchmarking theory.
Lüttgen, G. and Vogler, W. Conjunction on processes: Full-abstraction via ready-tree semantics. Technical Report YCS-2005-396, Department of Computer Science, University of York, England, December 2005. Abstract / Article / BibTeX.

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 paper introduces a conjunction operator on labelled transition systems capturing the basic intuition of "a and b = false", and considers a naive preorder that demands that an inconsistent specification can only be refined by an inconsistent implementation.

The main body of the paper is concerned with characterising the largest precongruence contained in the naive preorder. This characterisation will be 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 paper's results provide a foundation for, and an important step towards a unified framework that allows one to freely mix operators from process algebras and temporal logics.
White, D. and Lüttgen, G. Accessing databases from Esterel. Technical Report YCS-2004-384, Department of Computer Science, University of York, England, December 2004. Abstract / Article / BibTeX.

A current limitation in reactive systems design is the lack of database support in tools such as Esterel Studio. This report proposes a way of integrating databases and Esterel by providing an Application Programming Interface (API) for relational database use inside Esterel.

As databases and Esterel programs are often executed on different machines, result sets from database queries may be processed either locally and according to the synchrony hypothesis, or remotely along several reactive cycles. These different scenarios are reflected in the development of two APIs detailed in this report. Their utility is demonstrated by means of a case study modelling a warehouse storage system as might be used by a direct order company. The system employs a robot whose task it is to collect items from a customer's order and assemble them in one place. In addition to customer and order data, the underlying database stores spatial data detailing the position of items in the warehouse. Both robot and warehouse are implemented using the Lego Mindstorms robotics system.
Lüttgen, G. and Vogler, W. Bisimulation on speed: A unified approach. Technical Report No. 2004-15, Computer Science Institute, University of Augsburg, Germany, December 2004. Abstract / Article / BibTeX.

Two process-algebraic approaches have been developed for comparing two bisimulation-equivalent processes with respect to speed: the one of Moller-Tofts equips actions with lower time bounds, while the other by Lüttgen-Vogler considers upper time bounds instead.

This paper sheds new light onto both approaches by testifying to their close relationship and brings the research into bisimulation-based faster-than preorders to a close. We introduce a general, very intuitive concept of "faster-than", which is formalised by a notion of amortised faster-than preorder. When closing this preorder under all contexts, exactly the two faster-than preorders investigated by Moller/Tofts and Lüttgen/Vogler arise. For processes incorporating both lower and upper time bounds we also show that the largest precongruence contained in the amortised faster-than preorder is not a proper preorder but a timed bisimulation. In the light of this result we systematically investigate under which circumstances the amortised faster-than preorder degrades to an equivalence.
Lüttgen, G. and Vogler, W. Bisimulation on speed: Lower time bounds. Technical Report No. 2004-1, Computer Science Institute, University of Augsburg, Germany, January 2004. Abstract / Article / BibTeX.

More than a decade ago, Moller and Tofts published their seminal work on relating processes that are annotated with lower time bounds, with respect to speed. Their paper has left open many questions concerning the semantic theory for their suggested bisimulation-based faster-than preorder, the MT-preorder, which have not been addressed since. The encountered difficulties concern a general compositionality result, a complete axiom system for finite processes, and a convincing intuitive justification of the MT-preorder.

This paper solves these difficulties by developing and employing novel tools for reasoning in discrete-time process algebra, in particular a general commutation lemma relating the sequencing of action and clock transitions. Most importantly, it is proved that the MT-preorder is fully-abstract with respect to a natural amortized preorder that uses a simple bookkeeping mechanism for deciding whether one process is faster than another. Together these results reveal the intuitive roots of the MT-preorder as a faster-than relation, while testifying to its semantic elegance. This lifts some of the barriers that have so far hampered progress in semantic theories for comparing the speed of processes.
Cleaveland, R. and Lüttgen, G. A logical process calculus. ICASE Report No. 2002-26 (NASA/CR-2002-211759), Institute for Computer Applications in Science and Engineering (ICASE), NASA Langley Research Center, Hampton, VA, USA, August 2002. Abstract / Article / BibTeX.

This paper presents the Logical Process Calculus (LPC), a formalism that supports heterogeneous system specifications containing both operational and declarative subspecifications. Syntactically, LPC extends Milner's Calculus of Communicating Systems with operators from the alternation-free linear-time mu-calculus (LTmu). Semantically, LPC is equipped with a behavioral preorder that generalizes Hennessy's and De Nicola's must-testing preorder as well as LTmu's satisfaction relation, while being compositional for all LPC operators. From a technical point of view, the new calculus is distinguished by the inclusion of (i) both minimal and maximal fixed-point operators and (ii) an unimplementability predicate on process terms, which tags inconsistent specifications. The utility of LPC is demonstrated by means of an example highlighting the benefits of heterogeneous system specification.
Ciardo, G., Lüttgen, G. and Siminiceanu, R. . ICASE Report No. 2001-5 (NASA/CR-2001-210663), Institute for Computer Applications in Science and Engineering (ICASE), NASA Langley Research Center, Hampton, VA, USA, February 2001. Abstract / Article / BibTeX.

This paper presents a novel algorithm for generating state spaces of asynchronous systems using Multi-valued Decision Diagrams. In contrast to related work, the next-state function of a system is not encoded as a single Boolean function, but as cross-products of integer functions. This permits the application of various iteration strategies to build a system's state space. In particular, this paper introduces a new elegant strategy, called saturation, and implements it in the tool SMART. On top of usually performing several orders of magnitude faster than existing BDD-based state-space generators, the algorithm's required peak memory is often close to the final memory needed for storing the overall state spaces.
Lüttgen, G. and Vogler, W. A faster-than relation for asynchronous processes. ICASE Report No. 2001-2 (NASA/CR-2001-210651), Institute for Computer Applications in Science and Engineering (ICASE), NASA Langley Research Center, Hampton, VA, USA, January 2001. Abstract / Article / BibTeX.

This paper introduces a novel (bi)simulation-based faster-than preorder which relates asynchronous processes with respect to their worst-case timing behavior. The studies are conducted for a conservative extension of the process algebra CCS, called TACS, 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 this paper is in 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 paper also develops the semantic theory of TACS: it characterizes the largest precongruence contained in the faster-than preorder. A small example relating two implementations of a simple storage system testifies to the practical utility of the new theory.
Lüttgen, G. and Mendler, M. The intuitionism behind Statecharts steps. ICASE Report No. 2000-28 (NASA/CR-2000-210302), Institute for Computer Applications in Science and Engineering (ICASE), NASA Langley Research Center, Hampton, VA, USA, July 2000. Abstract / Article / BibTeX.

The semantics of Statecharts macro steps, as introduced by Pnueli and Shalev, lacks compositionality. This report first analyzes the compositionality problem and traces it back to the invalidity of the Law of the Excluded Middle. It then characterizes the semantics via a particular class of linear, intuitionistic Kripke models, namely stabilization sequences. This yields, for the first time in the literature, a simple fully-abstract semantics which interprets Pnueli and Shalev's concept of failure naturally. The results not only give insight into the semantic subtleties of Statecharts, but also provide a basis for an implementation, for developing algebraic theories for macro steps, and for comparing different Statecharts variants.
Lüttgen, G. and Mendler, M. What is in a step: A fully-abstract semantics for Statecharts macro steps via intuitionistic Kripke models. Research Memoranda CS-00-04, University of Sheffield, England, June 2000. Abstract / Article / BibTeX.

The semantics of Statecharts macro steps, as introduced by Pnueli and Shalev, lacks compositionality. This report first analyzes the compositionality problem and traces it back to the invalidity of the Law of the Excluded Middle. It then characterizes the semantics via a particular class of linear, intuitionistic Kripke models, namely stabilization sequences. This yields, for the first time in the literature, a simple fully-abstract semantics which interprets Pnueli and Shalev's concept of failure naturally. The results not only give insight into the semantic subtleties of Statecharts, but also provide a basis for an implementation, for developing algebraic theories for macro steps, and for comparing different Statecharts variants.
Cleaveland, R. and Lüttgen, G. Model checking is refinement: Relating Büchi testing and linear-time temporal logic. ICASE Report No. 2000-14 (NASA/CR-2000-210090), Institute for Computer Applications in Science and Engineering (ICASE), NASA Langley Research Center, Hampton, VA, USA, March 2000. Abstract / Article / BibTeX.

This paper develops a semantic foundation for reasoning about reactive systems specifications featuring combinations of labeled transition systems and formulas in linear-time temporal logic (LTL). Using Büchi automata as a semantic basis, the paper introduces two refinement preorders based on De Nicola and Hennessy's notion of may- and must-testing. Alternative characterizations for these relations are provided and used to show that the new preorders are conservative extensions of the traditional De Nicola and Hennessy preorders. The paper then establishes a tight connection between LTL formula satisfaction and the Büchi must-preorder. More precisely, it is shown that a labeled transition system satisfies an LTL formula if and only if it refines an appropriately defined Büchi automaton that can be constructed from the formula. Consequently, the Büchi must-preorder allows for a uniform treatment of traditional notions of process refinement and model checking. The implications of the novel theory are illustrated by means of a simple example system, in which some components are specified as transition systems and others as LTL formulas.
Lüttgen, G., von der Beeck, M. and Cleaveland, R. A compositional approach to Statecharts semantics. ICASE Report No. 2000-12 (NASA/CR-2000-210086), Institute for Computer Applications in Science and Engineering (ICASE), NASA Langley Research Center, Hampton, VA, USA, March 2000. Abstract / Article / BibTeX.

Statecharts is a visual language for specifying reactive system behavior. The formalism extends traditional finite-state machines with notions of hierarchy and concurrency, and it is used in many popular software design notations. A large part of the appeal of Statecharts derives from its basis in state machines, with their intuitive operational interpretation. The traditional semantics of Statecharts, however, suffers from a serious defect: it is not compositional, meaning that the behavior of system descriptions cannot be inferred from the behavior of their subsystems. Compositionality is a prerequisite for exploiting the modular structure of Statecharts for simulation, verification, and code generation, and it also provides the necessary foundation for reusability.

This paper suggests a new compositional approach to formalizing Statecharts semantics as flattened transition systems in which transitions represent system steps. The approach builds on ideas developed for timed process calculi and employs structural operational rules to define the transitions of a Statecharts expression in terms of the transitions of its subexpressions. It is first investigated for a simple dialect of Statecharts, with respect to a variant of Pnueli and Shalev's semantics, and is illustrated by means of a small example. To demonstrate its flexibility, the proposed approach is then extended to deal with practically useful features available in many Statecharts variants, namely state references, history states, and priority concepts along state hierarchies.
Lüttgen, G., Muñoz, C., Butler, R., Di Vito, B. and Miner, P. Towards a customizable PVS. ICASE Report No. 2000-4 (NASA/CR-2000-209851), Institute for Computer Applications in Science and Engineering (ICASE), NASA Langley Research Center, Hampton, VA, USA, January 2000. Abstract / Article / BibTeX.

PVS is a state-of-the-art theorem-proving tool developed by SRI International. It is used in a variety of academic and real-world applications by NASA and ICASE researchers, for whom tool customization and extensibility are becoming increasingly important issues. This paper shows, by referring to past experiences with several projects and case studies, that the customization features currently offered by PVS are often insufficient. It also suggests several improvements regarding PVS's customization in the short run and regarding its extensibility in the long run.
Ciardo, G., Lüttgen, G. and Siminiceanu, R. Efficient symbolic state-space construction for asynchronous systems. ICASE Report No. 99-50 (NASA/CR-1999-209827), Institute for Computer Applications in Science and Engineering (ICASE), NASA Langley Research Center, Hampton, VA, USA, December 1999. Abstract / Article / BibTeX.

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 paper, we develop a new algorithm for the symbolic generation of the state space 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, the algorithm supports intelligent cache management and achieves faster convergence via advanced iteration control. It is implemented in the tool SMART, and run-time results for several examples taken from the Petri net literature show that the algorithm performs about one order of magnitude faster than the best existing state-space generators.
Lüttgen, G., von der Beeck, M. and Cleaveland, R. Statecharts via process algebra. ICASE Report No. 99-42 (NASA/CR-1999-209713), Institute for Computer Applications in Science and Engineering (ICASE), NASA Langley Research Center, Hampton, VA, USA, October 1999. Abstract / Article / BibTeX.

Statecharts is a visual language for specifying the behavior of reactive systems. The language extends finite-state machines with concepts of hierarchy, concurrency, and priority. Despite its popularity as a design notation for embedded systems, precisely defining its semantics has proved extremely challenging. In this paper, a simple process algebra, called Statecharts Process Language (SPL), is presented, which is expressive enough for encoding Statecharts in a structure-preserving and semantics-preserving manner. It is established that the behavioral relation bisimulation, when applied to SPL, preserves Statecharts semantics.
Cleaveland, R., Lüttgen, G. and Natarajan, V. Analyzing mode confusion via model checking. ICASE Report No. 99-18 (NASA/CR-1999-209332), Institute for Computer Applications in Science and Engineering (ICASE), NASA Langley Research Center, Hampton, VA, USA, May 1999. Abstract / Article / BibTeX.

Mode confusion is one of the most serious problems in aviation safety. Today's complex digital flight decks make it difficult for pilots to maintain awareness of the actual states, or modes, of the flight deck automation. NASA Langley leads an initiative to explore how formal techniques can be used to discover possible sources of mode confusion. As part of this initiative, a flight guidance system was previously specified as a finite Mealy automaton, and the theorem prover PVS was used to reason about it.

The objective of the present paper is to investigate whether state-exploration techniques, especially model checking, are better able to achieve this task than theorem proving and also to compare several model-checking tools for the specific application. The flight guidance system is modeled and analyzed in Murphi, SMV, and Spin. The tools are compared regarding their system description language, their practicality for analyzing mode confusion, and their capabilities for error tracing and for animating diagnostic information. It turns out that their strengths are complementary.
Lüttgen, G., Bhat, G. and Cleaveland, R. A practical approach to implementing real-time semantics. ICASE Report No. 99-4 (NASA/CR-1999-208980), Institute for Computer Applications in Science and Engineering (ICASE), NASA Langley Research Center, Hampton, VA, USA, January 1999. Abstract / Article / BibTeX.

This paper investigates implementations of process algebras which are suitable for modeling concurrent real-time systems. It suggests an approach for efficiently implementing real-time semantics using dynamic priorities. For this purpose a process algebra with dynamic priority is defined, whose semantics corresponds one-to-one to traditional real-time semantics. The advantage of the dynamic-priority approach is that it drastically reduces the state-space sizes of the systems in question while preserving all properties of their functional and real-time behavior.

The utility of the technique is demonstrated by a case study which deals with the formal modeling and verification of the SCSI-2 bus-protocol. The case study is carried out in the Concurrency Workbench of North Carolina, an automated verification tool in which the process algebra with dynamic priority is implemented. It turns out that the state space of the bus-protocol model is about an order of magnitude smaller than the one resulting from real-time semantics. The accuracy of the model is proved by applying model checking for verifying several mandatory properties of the bus protocol.
Cleaveland, R., Lüttgen, G. and Natarajan, V. Priority in process algebras. ICASE Report No. 99-3 (NASA/CR-1999-208979), Institute for Computer Applications in Science and Engineering (ICASE), NASA Langley Research Center, Hampton, VA, USA, January 1999. Abstract / Article / BibTeX.

This paper surveys the semantic ramifications of extending traditional process algebras with notions of priority that allow for some transitions to be given precedence over others. These enriched formalisms allow one to model system features such as interrupts, prioritized choice, or real-time behavior.

Approaches to priority in process algebras can be classified according to whether the induced notion of pre-emption on transitions is global or local and whether priorities are static or dynamic. Early work in the area concentrated on global pre-emption and static priorities and led to formalisms for modeling interrupts and aspects of real-time, such as maximal progress, in centralized computing environments. More recent research has investigated localized notions of pre-emption in which the distribution of systems is taken into account, as well as dynamic priority approaches, i.e., those where priority values may change as systems evolve. The latter allows one to model behavioral phenomena such as scheduling algorithms and also enables the efficient encoding of real-time semantics.

Technically, this paper studies the different models of priorities by presenting extensions of Milner's Calculus of Communicating Systems (CCS) with static and dynamic priority as well as with notions of global and local pre-emption. In each case the operational semantics of CCS is modified appropriately, behavioral theories based on strong and weak bisimulation are given, and related approaches for different process-algebraic settings are discussed.
Cleaveland, R. and Lüttgen, G. An algebraic theory of distributed real-time. Technical Report TR-96-04, North Carolina State University, Raleigh, USA, March 1996. Abstract / Article / BibTeX.

This paper develops a real-time process algebra, TPLmc, for modeling and reasoning about distributed real-time systems. Like the algebra PMC, TPLmc includes operators for binding processes to different clocks; unlike PMC, however, TPLmc includes a version of the maximal progress assumption. Using simple examples, we motivate why these features are useful and in some cases necessary for modeling and verifying distributed systems; we also present a behavioral congruence based on Milner's observational equivalence and develop logical characterizations of the behavioral relations.
Cleaveland, R., Lüttgen, G. and Natarajan, V. A process algebra with distributed priorities. Technical Report TR-96-02, North Carolina State University, Raleigh, USA, March 1996. Abstract / Article / BibTeX.

This paper presents a process algebra for distributed systems in which some actions may take precedence over others. In contrast with existing approaches to priorities, our algebra only allows actions to take priority over others at the same "location" and therefore captures a notion of localized preemption. Using Park's and Milner's notion of strong bisimulation as a basis, we develop a behavioral congruence and axiomatize it for finite processes; we also derive an associated observational congruence. Simple examples are given that highlight the utility of the theory.
Geser, A., Knoop, J., Lüttgen, G., Rüthing, O. and Steffen, B. Non-monotone fixpoint iterations to resolve second order effects. Technical Report TR-96-01, North Carolina State University, Raleigh, USA, March 1996. Abstract / Article / BibTeX.

We present a new fixpoint theorem which guarantees the existence and the finite computability of the least common solution of a countable system of recursive equations over a wellfounded domain. The functions are only required to be increasing and delay-monotone, the latter being a property much weaker than monotonicity. We hold that wellfoundedness is a natural condition as it guarantees termination of every fixpoint computation algorithm. Our fixpoint theorem covers, under the wellfoundedness condition, all the known "synchronous" versions of fixpoint theorems. To demonstrate its power and versatility we contrast an application in data flow analysis, where known versions are applicable as well, to a practically relevant application in program optimization, which due to its second order effects, requires the full strength of our new theorem. In fact, the new theorem is central for establishing the optimality of the partial dead code elimination algorithm considered, which is implemented in the new release of the Sun SPARCompiler language systems.
Graf, S., Steffen, B. and Lüttgen, G. Compositional minimization of finite state systems using interface specifications. Technical Report MIP-9505, University of Passau, Germany, January 1995. Abstract / Article / BibTeX.

In this paper we present a method for the compositional construction of the minimal transition system that represents the semantics of a given distributed system. Our aim is to control the state explosion caused by the interleavings of actions of communicating parallel components by reduction steps that exploit global communication constraints given in terms of interface specifications. The effect of the method, which is developed for bisimulation semantics here, depends on the structure of the distributed system under consideration, and the accuracy of the interface specifications. However, its correctness does not: every "successful" construction is guaranteed to yield the desired minimal transition system, independent of the correctness of the interface specifications provided by the program designer.
Geser, A., Knoop, J., Lüttgen, G., Steffen, B. and Rüthing, O. Chaotic fixed point iterations. Technical Report MIP-9403, University of Passau, Germany, October 1994. Abstract / Article / BibTeX.

In this paper we present a new fixed point theorem applicable for a countable system of recursive equations over a wellfounded domain. Wellfoundedness is an essential feature of many computer science applications as it guarantees termination of the corresponding fixed point computation algorithms. Besides being a natural restriction, it marks a new area of application, where not even monotonicity is required. We demonstrate the power and versatility of our fixed point theorem, which under the wellfoundedness condition covers all the known "synchronous" versions of fixed point theorems, by means of applications in data flow analysis and program optimization.

^ Top

Book Reviews

Lüttgen, G.: Constraints Meet Concurrency. By Mauro, J. Published by Atlantis Press, 2014, ISBN 978-94-6239-066-9, 148 pages. AMS Mathematical Reviews, 2017. Review.
Lüttgen, G.: Directed Algebraic Topology and Concurrency. By Fajstrup, L., Goubault, E., Haucourt, E., Mimram, S. and Raussen, M. Published by Springer, 2016, ISBN 978-3-319-15397-1, 167 pages. AMS Mathematical Reviews, 2016. Review.
Lüttgen, G.: Unfoldings: A partial-order approach to model checking. By Esparza, J. and Heljanko, K. Published by Springer, 2008, ISBN 978-3-540-77425-9, 169 pages. AMS Mathematical Reviews, 2011. Review.
Lüttgen, G.: Modeling and verification using UML Statecharts. By Drusinsky, D. Published by Newnes Publishers, 2006, ISBN 0-7506-7617-5, 306 pages. Software Testing, Verification and Reliability 18(3):189-190, 2008. Review / BibTeX / DOI.

^ Top

All Other Works

Rupprecht, T., Boockmann, J. H., White, D. H. and Lüttgen, G. DSI: Automated detection of dynamic data structures in C programs and binary code. In W. Amme and T. S. Heinze, eds., 19th Colloquium on Programming Languages and Foundations of Programming (KPS 2017), vol. Math/Inf/02/2017 of Jenaer Schriften zur Mathematik und Informatik, pp. 134-147, Weimar, Germany, September 2017. Friedrich-Schiller-Universität Jena. Abstract / Article / BibTeX / URL.

Program comprehension is an important task for software engineers who maintain legacy code, as well as for reverse engineers who analyse binary executables such as malware. Detecting dynamic, i.e., pointer-based data structures is a particular challenge due to the complex usage of pointers found in real world software.

This paper presents the key results of the DFG-funded project "Learning Data Structure Behaviour from Executions of Pointer Programs" (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 structure with the help of a systematic taxonomy. The inferred data structure information is not only helpful for program comprehension but also for other use cases including software verification and software visualization.
White, D. H., Rupprecht, T. and Lüttgen, G. dsOli2: Discovery and comprehension of interconnected lists in C programs. In J. Knoop, ed., 18th Colloquium on Programming Languages and Foundations of Programming (KPS 2015), Pörtschach, Austria, October 2015. Technical University Vienna. Abstract / Article / BibTeX / URL.

Comprehension of C programs can be a challenging task, especially when they contain pointer-based dynamic data structures. Based on prior experience with our tool dsOli1, we report on work in progress concerning a new dynamic analysis for automated data structure identification that targets C source code. Our technique first applies a novel abstraction on the evolving memory structures observed at runtime for discovering the building blocks of complex data structures. By analyzing the interconnections between the building blocks, we are then able to identify trees, doubly-linked lists, skip lists, as well as relationships between these such as nesting. We give preliminary results from a prototype implementation, which aims to provide a natural language description of the identified data structures. This information will benefit software developers when code must be comprehended or modified.
Gareis, J., White, D., Lüttgen, G. and Ciardo, G. Improving variable ordering for Saturation by learning from small problem instances. Unpublished addendum to the final report of the grant Improving symbolic software verification via machine learning (BaCaTeC - Bavaria California Technology Center, grant no.: 5 [2012-2]), University of Bamberg, Germany, December 2014. Abstract / Article / BibTeX.

In the domain of symbolic model checking, Saturation is a popular exploration strategy for building a system's state space. A decision diagram is employed to encode the state space; however, its resulting size and thus time taken to build is highly dependent on the ordering of the system's variables. Heuristics for determining good orderings have thus far focused on the static, structural properties of the model. However, a system often exhibits complex dynamic behavior that is difficult to estimate statically.

In this work we propose that variable orderings be learnt from multiple executions of the Saturation algorithm on small problem instances, with the expectation that learnt variable orderings will also perform well when the problem is scaled up. The benefits are twofold: firstly, by learning orderings through executing the algorithm, we expect to capture some of the dynamic behavior, and secondly, as Saturation has proven difficult to parallelize, a machine learning step could prove an easy route to parallelization. To this end we detail two approaches, one for models that are of fixed-size and only scale in terms of the information passed between model components, and one for models with topologies that grow in a regular manner when scaled.
Lüttgen, G. and Mendler, M. When 1 clock is not enough. In L. Aceto and A. D. Gordon, eds., Intl. Workshop on Algebraic Process Calculi: The First Twenty Five Years and Beyond (PA 2005), vol. NS-05-3 of BRICS Notes Series, pp. 155-158, Bertinoro, Italy, August 2005. BRICS - Basic Research in Computer Science, Denmark. Abstract / Article / BibTeX.

Sometimes single-clock timed process algebras are insufficient for modelling systems in practice. For example, this is the case for systems-on-chip where a single clock cannot be physically implemented with the required accuracy, or globally-asynchronous locally-synchronous systems that are spatially distributed. This note revisits the few published approaches to multi-clock timed process algebras, namely PMC, CSA and CaSE which are all based on Nicollin and Sifakis' ATP and extend Milner's CCS. In contrast to timed automata and continuous-time process algebra, these algebras treat time as a qualitative rather than a quantitative concept: a clock is taken to be a synchronisation event with limited scope, orchestrating the computations conducted within its scope into a well-defined sequence of successive clock phases. However, PMC, CSA and CaSE differ in the choice of operators and semantic features; these shall be discussed here with the help of a novel, unified semantic framework.
White, D. and Lüttgen, G. Accessing databases from Esterel. In S. A. Edwards, N. Halbwachs, R. v. Hanxleden and T. Stauner, eds., Intl. Workshop on Synchronous Programming (SYNCHRON 2004), Schloss Dagstuhl Proceedings Series, Dagstuhl, Germany, July 2005. Abstract / Article / BibTeX.

A current limitation in reactive systems design is the lack of database support in tools such as Esterel Studio. This report proposes a way of integrating databases and Esterel by providing an Application Programming Interface (API) for relational database use inside Esterel.

As databases and Esterel programs are often executed on different machines, result sets from database queries may be processed either locally and according to the synchrony hypothesis, or remotely along several reactive cycles. These different scenarios are reflected in the development of two APIs detailed in this report. Their utility is demonstrated by means of a case study modelling a warehouse storage system as might be used by a direct order company. The system employs a robot whose task it is to collect items from a customer's order and assemble them in one place. In addition to customer and order data, the underlying database stores spatial data detailing the position of items in the warehouse. Both robot and warehouse are implemented using the Lego Mindstorms robotics system.
Lüttgen, G. Formal Methods for the quality assurance of digital systems. Research Quarterly, 7(4), Institute for Computer Applications in Science and Engineering, Universities Space Research Association, December 1998. Abstract / Article / BibTeX.

Formal Methods aim at improving the reliability and safety of digital systems by applying mathematical specification and verification techniques. This article gives an introduction to Formal Methods and illustrates them by means of an example dealing with parts of a flight-guidance system.
Lüttgen, G. Kompositionelle Minimierung endlicher verteilter Systeme. Diplomarbeit (MSc thesis). Rheinisch-Westfälische Technische Hochschule (RWTH) Aachen, Germany, March 1994. Abstract / Article / BibTeX.

In dieser Arbeit wird eine Methode zur kompositionellen Konstruktion eines im Sinne einer Bisimulationssemantik minimalen Transitionssystemen vorgestellt, welches das Verhalten eines betrachteten verteilten Systems charakterisiert. Um die während der Konstruktion im allgemeinen auftretende Zustandsexplosion weitgehend zu vermeiden, werden neben Minimierungsschritten auch Reduktionsschritte durchgeführt. 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. Dadurch kann die durch das Interleaving von Aktionen kommunizierender Parallelkomponenten verursachte Zustandsexplosion kontrolliert werden. 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.