Weekly outline

  • General

    Project Seminar "Formal Methods II" (SS 2011)


    Time: Wednesday, 12:30-14:00. Place: Hagenberg Seminar Room. Start: March 16, 2010.


    If you would like to participate in this seminar but prefer another time or place (e.g. at the JKU campus), please contact Wolfgang Schreiner.


    In this seminar, we explore current research and systems for specifying and verifying computer programs (specification languages, program verifiers, model checkers, ...). This continues the seminar of the previous semester.


    To take part in the seminar, you have to enrol in the KUSSS system. If you also login in Moodle and register as a course participant, you will receive per email all messages posted in the Announcements forum and can yourself post messages in the Questions and Answers forum.


  • 16 March - 22 March

    March 16
    • Introduction and Organization
    • Wolfgang Schreiner: The RISC ProgramExplorer: Third Status Report
  • 11 May - 17 May

  • 15 June - 21 June

    June 15

    Finite automata over infinite alphabets

    I. E. Mens, Department of Mathematics, Aristotle University of Thessaloniki, Greece


    Reasoning on infinite state systems with finite control and infinite data, requires new automata models working over infinite alphabets. We introduce here such a model, named variable finite automaton on words over infinite alphabets (VFA). This model is based on an underlying non-deterministic finite automaton over a finite alphabet containing variable symbols. The underlying automaton computes its language, and then replaces the variable symbols with symbols from the infinite alphabet following certain rules. We show that the class of recognizable languages over infinite alphabets is closed under union and intersection but not under complementation. The emptiness, equality and universality problems are decidable.

    A Conceptual SOA-based Framework for e-Government Central Database

    Dr. Rebhi Baraka, Head of Software Development Department, Faculty of Information Technology, Islamic University of Gaza


    The Central Database is one of the core components in the e-Government technical framework. In this talk we shed some light on the current situation of the Central Database and its limitations. The talk will present a proposed Service Oriented Architecture (SOA) framework that integrates with the concept of Enterprise Service Bus (ESB) and Web services. The proposed conceptual framework will enhance interoperability, flexibility and manageability of the Central Database in the e-Government.

    inite automata over infinite alphabets
    
  • 13 July - 19 July

    Tuesday, July 19, 10:15

    The Impact of Heterogeneous Traffic on the Performance of Proxy Cache Servers

    Tamas Berczes, Faculty of Informatics, University of Debrecen, Hungary

    The focus of this talk is to examine the performance behavior of Proxy Cache servers when we use heterogeneous traffic. We describe the multi-class queuing network model of the Proxy Cache server, where we separate the requests in two classes by virtue of their size. If the size of the requested document is greater than average we put it into class a. In the opposite case, when the size of the requested file is small we put it into class b. We have calculated the overall response time with and without a Proxy Cache server. We analyzed how various factors affect the performance of a Proxy Cache server when we use heterogeneous traffic. In general when the arrival rate of requests increases, then the response time increases as well regardless of the existence of a Proxy Cache server. Increasing the percentage of the class a the response time increases too. When we use a higher percentage of the class a and we use a high arrival rate, then the response time gap is more significant between the cases with and without a Proxy Cache server. Using a low percentage of class a files, a low arrival rate and low cache hit rate probability we get higher response time in presence of a Proxy Cache server. Several numerical examples illustrate the effect of arrival, external arrival rate and the file size of class a and class b on the mean response times.