Ingo Pill, Dipl.-Ing. Dr.techn. Institute for Software Technology Graz University of Technology Brueckenkopfgasse 1/1 8010 Graz, Austria     Phone: ++43(0)316/873-5481 Secretary: ++43(0)316/873-5711       Fax: ++43(0)316/873-5706    E-Mail: ipill(at)ist.tugraz.at       WWW: http://www.ist.tugraz.at/pill

Current projects

• Model-Based Diagnosis - Active Tests

  One of the issues of model-based diagnosis is the fact that you might be faced with a multitude of different diagnoses depending on the situation/observations. In case cardinality, experience, etc. do not enable you to isolate a single diagnosis, further information is needed. Currently we are investigating ways to generate such ''tests'', which will enable you to isolate a single diagnosis with the information gathered with this test. Our work is related to systems where you for instance have some robot interacting with its environment, so that a temporal model is used.

• Diagnosis and Monitoring of Logistics Facilities

  For this project we collaborate with a company, so that we are restricted by an NDA and cannot reveal the details of this project and will publish general results with a substantial delay. In general we aim at the diagnosis and monitoring of industrial facilities in the context of logistics. A first paper on general considerations will be presented at the 7th IFAC Symposium on Fault Detection, Supervision and Safety of Technical Processes (SAFEPROCESS) in Barcelona, Spain June 30th - July 3rd 2009 in a paper called "A Practical Approach for the Online Diagnosis of Industrial Transportation Systems".

• Requirement Analysis: Property Simulation and Assurance - The RAT tool

  One of the main prerequisites for a successful use of formal properties in a design process is a deep understanding of the involved property language; not only to know what one wants to formulate, but how to do it, and most importantly what one has actually written. Property Simulation is a technique to explore the meaning of a property by simulating its behavior for user-defined scenarios. The designer can state requests like that value a shall become true at time step five, and then asks for witness or counterexample behavior of the property. Like HDL simulators property simulation uses waveforms to illustrate dynamic behavior. For an explanation of the result all subformulae are evaluated along the trace, whereby the result is shown as a set of waveforms organized in a tree relating to the property syntax. Property Assurance complements Property Simulation by supporting a more global perspective. By means of Propery Assurance a designer analyses the strictness of a specification (requirements) as a whole. The designer can specify assertions which must hold uniformly and possibilities depicting behavioral patterns which have to be feasible. So it is possible to check if the specification is strict enough to rule out unwanted behavior and whether it is not too strict to allow for certain desireable behavior. We implementated Property Simulation and Property Assurance for the PSL language in our RAT tool, which is a joint effort with Fondacione Bruno Kessler (former ITC Irst), Trento-Italy to provide an requirements analysis tool for high quality specifications. RAT integrates Property Simulation and Assurance to offer a powerful tool to manage and analyse requirements (specifications) whereas the obtained results can be saved in a project for future reference. RAT assists the designer in learning the language and writing high-quality requirements. Parts of this work were presented at the 43rd Design Automation Conference in San Francisco, 24-28th July 2006 in a paper called "Formal Analysis of Hardware Requirements", at ECAI 2006, and at the Computer Aided Verification Conference (CAV) 2007. Note that since September 2009, there is new functionality in the context of synthesis, so that the tool was renamed to RATSY and there was a major version bump to 2.0 .

• Automata Library for PSL

  Recently new expressive temporal logics like PSL and ForSpec have emerged. To use these languages in automata based approaches (e.g. for model checking) automata construction algorithms and libraries for these languages have to be developed. We are currently working on an implementation of an optimized construction library for PSL.

• Symbolic Implementation of Alternating Automata

  It is often necessary to create a non-deterministic version of an alternating automaton. We are currently working on an efficient implementation of this process, where we do not require an intermediate explicit version of the non-deterministic automaton but are able to derive a symbolic representation directly. Furthermore we work on optimizing this representation exploiting structural information of the alternating automaton. Parts of this work were presented at the 11th International Conference on Implementation and Application of Automata (CIAA) in Taipei, 21-23rd August 2006, in a paper called "Symbolic Implementation of Alternating Automata". Further results were published in our article "Symbolic Implementation of Alternating Automata" in the International Journal of Foundations of Computer Science in Vol.18/No.4 (August 2007).

Publications:

Upcoming

Papers

• A Practical Approach for the Online Diagnosis of Industrial Transportation Systems, I. Pill, G. Steinbauer, F. Wotawa, in 7th IFAC Symposium on Fault Detection, Supervision and Safety of Technical Processes (SAFEPROCESS) 2009, 1318-1323, the paper will be available at IFAC papersonline
• Rat: A tool for the formal analysis of requirements, R. Bloem, R. Cavada, I. Pill, M. Roveri, and A. Tchaltsev, in Computer Aided Verification (CAV) 2007, 263-267
• Symbolic Implementation of Alternating Automata, R.Bloem, A.Cimatti, I.Pill, M.Roveri, IJFCS: International Journal of Foundations of Computer Science, Volume 18, Number 4 (August 2007), pp. 727-742, World Scientific Publishing Company, link to paper on www.worldscinet.com
• Symbolic Implementation of Alternating Automata, R.Bloem, A.Cimatti, I.Pill, M.Roveri, and S.Semprini, CIAA '06: Proceedings of the 11th International Conference on Implementation and Application of Automata, LNCS 4094, pp. 208-218, Springer Verlag Berlin Heidelberg/Germany, ISBN 3-540-37213-X, in Taipei/Taiwan, 2006.
• Formal Analysis of Hardware Requirements, I.Pill, S.Semprini, R.Cavada, M.Roveri, R.Bloem, and A.Cimatti. DAC '06: Proceedings of the 43rd annual conference on design automation, pp 821-826, ACM Press New York/USA, ISBN 1-59593-381-6, in San Francisco/USA, 2006. Paper and slides are available at the conference archives: [paper 48.1]
• Systemverifikation im Designprozess heterogener mikroelektronischer Systeme, M.Pistauer, S.Kajtazovic, I.Pill, and Ch.Steger, Proceedings Analog2003, Heilbronn, Germany,pp. 43-48. VDE Verlag Berlin, Offenbach, ISBN 3-8007.2778-1. in Heilbronn/Germany, 2003. Paper is available at the conference archives: [pdf].

Theses

• Requirements Engineering and Efficient Verification of PSL Properties, Ingo Pill, PhD Thesis, Institute for Software Technology at Graz University of Technology, 2008, [pdf].
• Design and Implementation of a Cosimulation Environment for Heterogeneous Microelectronic Systems, Ingo Pill, Master's Thesis, Institute for Technical Informatics at Graz University of Technology, 2003, [pdf].

System Demonstrations