Publikationen zum Fachbereich TLDA

Dissertationen und Habilitationen

• Adrianna Alexander. Komposition Temporallogischer Spezifikationen - Spezifikation und Verifikation von Systemen mit Temporal Logic of Distributed Actions. Dissertation, Humboldt-Universität zu Berlin, Mathematisch-Naturwissenschaftliche Fakultät II, September 2005.

  Abstract: This thesis introduces a new temporal logic, called Temporal Logic ofDistributed Actions, TLDA for short. TLDA is designed for compositional specification and verification of distributed systems. TLDA originates syntactically from an already established temporal logic, TLA. But TLDA, contrary to TLA and other known compositional temporal logics, is based semantically on a partial order structure, called distributed run. Compared to TLA, the use of this semantical model increases the expressiveness of TLDA. Both the system and its properties are described in one formalism: They are represented by a set of distributed runs and specified in TLDA by a temporal logic formula. Hence, the verification of a system is reduced to proving that the system specification implies the property specification. We provide a set of proof rules for this. We show that the composition of systems is specified by conjunction of the specifications of its components and, usually, the specification of the interaction between the components. Hence, the specification of a composed system can be derived from specifications of its components. Component properties are preserved in the process of composition. Thus, components can be verified separately and then be integrated into the composed system. This economises the effort for verification. Attuned for distributed runs we develop a semantical criterion for TLDA-formulas, called environmental invariance. We show that environmental invariant formulas are suited for the specification of system components. We prove that such environmental invariant formulas, due to their properties, supply a modular design of systems.

  

Konferenzbeiträge und Beiträge auf Workshops

• Adrianna Alexander. Composition of Temporal Logic Specifications. In Jordi Cortadella and Wolfgang Reisig, editors, Applications and Theory of Petri Nets 2004, 25th International Conference (ICATPN 2004), number 3099 of Lecture Notes in Computer Science, pages 98-116, 2004. Springer-Verlag.

  Abstract: The Temporal Logic of Distributed Actions (TLDA) is a new temporal logic designed for the specification and verification of distributed systems. TLDA supports a modular design of systems: Subsystems can be specified and verified separately and then be integrated into one system. The properties of the subsystems will be preserved in this process. TLDA can be syntactically viewed as an extension of TLA. We propose a different semantical model based on partial order which increases the expressiveness of the logic.

  

• Adrianna Alexander and Wolfgang Reisig. Compositional Temporal Logic Based on Partial Order. In 11th International Symposium on Temporal Representation and Reasoning (TIME'04), pages 125-132, 2004. IEEE Computer Society.

  Abstract: The Temporal Logic of Distributed Actions (TLDA) is a new temporal logic designed for the specification and verification of distributed systems. The logic supports a compositional design of systems: subsystems can be specified separately and then be integrated into one system. TLDA can be syntactically viewed as an extension of TLA. We propose a different semantical model based on partial order which increases the expressiveness of the logic.

  

• Adrianna Alexander and Wolfgang Reisig. Logic of Involved Variables - System Specification with Temporal Logic of Distributed Actions. In Proc. of the 3rd International Conference on Application of Concurrency to System Design (ACSD'03), Guimaraes, Portugal, pages 167-176, June 2003. IEEE Computer Society.

  Abstract: The Temporal Logic of Distributed Actions (TLDA) is a new temporal logic designed for the specification and verification of distributed systems. TLDA can be syntactically viewed as a slight extension of TLA. We propose a different semantical model based on partial order which evidently increases the expressiveness of the logic. Local variable updates in a system are explicitly modeled and expressed by TLDA formulas. Consequently, we can distinguish between concurrency and nondeterministic choice. All valuable features of TLA (composition is conjunction, implementation is implication) are retained. In addition, we are able to describe some important phenomena and properties typical for distributed systems.

  

Technische Berichte

• Adrianna Foremniak and Wolfgang Reisig. A Temporal Logic of Distributed Actions (TLDA). Informatik-Berichte 140, Humboldt-Universität zu Berlin, 2000.

Studien- und Diplomarbeiten

• Niels Lohmann. Formale Fundierung und effizientere Algorithmen für die schrittbasierte TLDA-Interleavingsemantik. Diplomarbeit, Humboldt-Universität zu Berlin, September 2005.

  Abstract: Die Temporal Logic of Distributed Actions (TLDA) ist eine neue temporale Logik miteiner Halbordnungssemantik und eignet sich somit zur Spezifikation verteilter Systeme. Allerdings existieren für TLDA noch keine Werkzeuge, die die Spezifikation und Verifikation unterstützen. Die Verfügbarkeit solcher Werkzeuge trägt jedoch entscheidend zur Verbreitung der Logik bei. In [Loh05] wurde mit der Ausarbeitung und Implementierung einer schrittbasierten Interleavingsemantik für TLDA die Grundlage für die Entwicklung eines expliziten TLDA-Modelcheckers gelegt. Der genaue Zusammenhang zwischen der Halbordnungs- und Interleavingsemantik wurde jedoch nicht bewiesen. Außerdem handelt es sich bei der Implementierung der Interleavingsemantik um einen Brute-Force-Prototyp, der nur für sehr einfach Spezifikationen in der Lage ist das Transitionssystem zu konstruieren. Die formale Fundierung sowie die Ausarbeitung effizienter Algorithmen und Datenstrukturen ist Inhalt dieser Arbeit. Anhand mehrerer Fallstudien untersuchen wir die Leistungsfähigkeit des erweiterten Prototyps und illustrieren die Beziehung zwischen der Halbordnungs- und Interleavingsemantik.

  

• Niels Lohmann. Implementierung einer schrittbasierten Interleavingsemantik für die Temporal Logic of Distributed Actions (TLDA). Studienarbeit, Humboldt-Universität zu Berlin, June 2005.

  Abstract: Die Temporal Logic of Distributed Actions (TLDA) ist eine temporale Logik mit einer Halbordnungssemantik und eignet sich somit zur Spezifikation verteilter Systeme. Allerdings gibt es noch wenig Erfahrung bei der computergestützten Verifikation halbordnungsbasierter Formalismen. Viele bekannte effiziente Algorithmen des expliziten Modelchecking setzen ein Transitionssystem und somit eine Interleavingsemantik voraus. In dieser Arbeit wird eine Interleavingsemantik für TLDA vorgeschlagen und ein Prototyp entwickelt, der für eine bestimmte Klasse von TLDA-Spezifikationen das Transitionssystem aufbaut. Die entwickelte Semantik soll zusammen mit dem Prototypen die Grundlage für die weitere Arbeit an einem Modelchecker für TLDA sein.

  

• Lars Kuhtz. TLDA und Petrinetze. Studienarbeit, Humboldt-Universität zu Berlin, April 2004.

• Peter Massuthe. Verfeinerungstechniken der Temporal Logic of Distributed Actions TLDA. Diplomarbeit, Humboldt-Universität zu Berlin, March 2004.

  Abstract: TLDA, die Temporal Logic of Distributed Actions, ist eine neue temporale Logik zur Spezifikation verteilter Systeme. Sie basiert auf halbgeordneten Abläufen. Diese Logik hat noch keinen formalen Verfeinerungsbegriff. Die Entwicklung von Methoden zur Unterstützung der Entwicklung komplexer TLDA-Spezifikationen durch schrittweise Verfeinerung ist Inhalt der vorliegenden Arbeit. Wir unterscheiden dabei zwischen Datenverfeinerung und Transitionsverfeinerung. Die Anwendbarkeit dieser Methoden wird anhand mehrerer mittelgroßer Fallstudien gezeigt. Weiterhin beschäftigen wir uns mit der Bewahrung von Eigenschaften durch Daten- und Transitionsverfeinerungsschritte. Diese Arbeit richtet sich vor allem an die Modellierer verteilter Systeme mit formalen Spezifikationsmethoden, insbesondere temporalen Logiken.

  

zurück zur Übersicht