University of Bamberg
open search form
You are here

Information Systems and Applied Computer Sciences

Software Technologies Research Group

  1.  University of bamberg
  2. Faculties
  3. Information Systems and Applied Computer Sciences
  4. Subject groups
  5. Computer Science
  6. Software Technologies Research Group
  7. Research
  8. Heterogeneous Software Specification

Heterogeneous Software Specification

This research topic concerns the theoretical foundations and practical utility of the growing number of languages for specifying reactive systems software that enrich state machine notations with logic connectives. Examples are the Interface Theories of de Alfaro/Henzinger and Caillaud et al., which consider logic conjunction, and the Contractual State Machines of Paige et al., which incorporate temporal logic.  While these heterogeneous languages promise more concise specifications and are accompanied by modern refinement-based approaches to software design, they lack mathematically robust semantics that respect the concurrency inherent in reactive systems.

Our research applies the setting of Logic Labelled Transition Systems (Logic LTS), which was co-developed by us, to fix this shortcoming. This will pave the way for advanced tool support, including the development of automated refinement checkers for Interface Theories and Contractual State Machines. Future work will also extend Logic LTS so as to capture complex safety, liveness and fairness properties, thereby allowing us to develop richer Interface Theories. It is anticipated that this will permit more concise descriptions of reactive systems software, thereby aiding programmers in software specification and design.

This research is conducted in collaboration with Prof. Walter Vogler (University of Augsburg, Germany) and supported under project title Foundations of Heterogeneous Specifications Using State Machines and Temporal Logic by the German Research Foundation (DFG, grant no. LU 1748/3-1). International project partners are Dr. Benoit Caillaud (IRISA, France), Prof. Rance Cleaveland (University of Maryland, USA), Prof. Richard Paige (University of York, U.K.) and Dr. Antti Siirtola (Aalto University, Finland).

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

Publications:

  • 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.