Universität Bamberg
Suche öffnen
Sie befinden sich hier:

Fakultät Wirtschaftsinformatik und Angewandte Informatik

Lehrstuhl Softwaretechnik und Programmiersprachen

  1.  Otto-Friedrich-Universität Bamberg
  2. Fakultäten
  3. Wirtschaftsinformatik und Angewandte Informatik
  4. Professuren und Lehrstühle
  5. Informatik
  6. Lehrstuhl Softwaretechnik und Programmiersprachen
  7. Forschung
  8. Heterogene Software Spezifikation

Heterogene Software Spezifikation

Ziel dieses Forschungsthemas ist die Verbesserung der theoretischen Grundlagen sowie der Anwendbarkeit von Formalismen zur Spezifikation reaktiver Systeme, welche Zustandsautomaten mit logischen Operatoren kombinieren. Aktuelle Beispiele hierzu sind die Interface-Theorien von de Alfaro/Henzinger und Caillaud et al., die Konjunktion betrachten, und die Contractual State Machines von Paige et al., die temporale Logikoperatoren beinhalten. Obwohl diese heterogene Sprachen mehr Prägnanz beim Spezifizieren versprechen und von modernen, verfeinerungsbasierten Ansätzen des Software-Entwurfs begleitet werden, fehlt ihnen eine mathematisch robuste Semantik, die auch die Nebenläufigkeitsaspekte reaktiver Systeme berücksichtigt.

Unsere Forschung soll diese Unzulänglichkeiten mittels Techniken der Logic Labelled Transition Systems (Logic LTS), die von uns erforscht worden sind, beheben. Dies wird die Entwicklung neuer Software-Werkzeuge ermöglichen, einschließlich automatischer Verfeinerungs-Checker für Interface-Theorien und Contractual State Machines. Weiterhin soll Logic LTS so erweitert werden, dass Sicherheits-, Lebendigkeits- und Fairnesseigenschaften in Spezifikationen eingebettet und somit reichhaltigere Interface-Theorien entwickelt werden können. Dies wird eine prägnantere Beschreibung von Software für reaktive Systeme ermöglichen und dadurch Programmierer bei der Software-Spezifikation und dem Software-Entwurf unterstützen.

Dieses Forschungsprojekt findet in Kollaboration mit Prof. Walter Vogler (Universität Augsburg) statt und wird unter dem Titel Grundlagen heterogener Spezifikationen mittels Zustandsmaschinen und temporaler Logik von der Deutschen Forschungsgemeinschaft gefördert (DFG, Projekt-Nr. LU 1748/3-1). Internationale Projektpartner sind Dr. Benoit Caillaud (IRISA, Frankreich), Prof. Rance Cleaveland (University of Maryland, USA), Prof. Richard Paige (University of York, Großbritannien) und Dr. Antti Siirtola (Aalto University, Finnland).

Kontakt: Prof. Dr. Gerald Lüttgen, Sascha Fendrich

Publikationen:

  • Lüttgen, G. and Vogler, W. Modal Interface Automata. Logical Methods in Computer Science, 9(3:4), 2013.
  • Lüttgen, G. and Vogler, W. Richer Interface Automata with optimistic and pessimistic compatibility. In H. Treharne and S. Schneider, eds., 13th Intl. Workshop onAutomated Verification of Critical Systems (AVoCS 2013), Guildford, England, September 2013. To appear in Electronic Communications of the EASST.
  • 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.
  • Lüttgen, G. and Vogler, W. Safe reasoning with Logic LTS. Theoretical Computer Science, 412(28):3337-3357, 2011. Bergstra Festschrift.
  • Lüttgen, G. and Vogler, W. Ready simulation for concurrency: It's logical! Information and Computation, 208:845-867, 2010.
  • 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.
  • 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.
  • 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.