Progress Reports

    
First Year
    
Final Report

    Journal papers

  1. C. BAIER, B. HAVERKORT, H. HERMANNS AND J.-P. KATOEN. Model-checking algorithms for continuous-time Markov chains. IEEE Transactions on Software Engineering, vol. 29, no. 6, pages 524-541, 2003.
  2. E. BRINKSMA, A. MADER AND A. FEHNKER. Verification and optimization of a PLC control schedule. International Journal on Software Tools for Technology Transfer, vol. 4(1), pages 21-3, 2002.
  3. P. BUCHHOLZ, J.-P. KATOEN, P. KEMPER AND C. TEPPER. Model-checking large structured Markov chains. Journal of Logic and Algebraic Programming, vol. 56, no. 1-2, pages 69-97, 2003.
  4. M.C.A. DEVILLERS, W.O.D. GRIFFIOEN, J.M.T. ROMIJN AND F.W. VAANDRAGER. Verification of a Leader Election Protocol - Formal Methods Applied to IEEE 1394. Formal Methods in System Design, vol. 16(3), pages 307-320, 2000.
  5. H. HERMANNS, J.-P. KATOEN, J. MEYER-KAYSER AND M. SIEGLE. A tool for model checking Markov chains. Int. Journal on Software Tools for Technology Transfer, vol. 4, no. 2, pages 153-172, 2003.
  6. H. HERMANNS, U. HERZOG AND J.-P. KATOEN. Process algebra for performance evaluation. Theoretical Computer Science, vol. 274, no. 1-2, pages 43-87, 2002.
  7. T. HUNE, J.M.T. ROMIJN, M.I.A. STOELINGA AND F.W. VAANDRAGER. Linear parametric model checking of timed automata. Journal of Logic and Algebraic Programming, vol. 52-53, pages 183-220, 2002.
  8. N.A. LYNCH, R. SEGALA, AND F.W. VAANDRAGER. Hybrid I/O automata. Information and Computation, vol. 185(1), pages 105-157, 2003.
  9. A. MADER, E. BRINKSMA, H. WUPPER, AND N. BAUER. Design of a PLC control program for a batch plant, VHS case study 1. European Journal of Control, vol. 7(4), pages 416-439, 2001.
  10. J.G. SPRINGINTVELD, F.W. VAANDRAGER AND P.R. D'ARGENIO. Testing timed automata. Theoretical Computer Science, vol. 254, Issue 1-2, pages 225-257, 2001.
  11. Books and edited volumes

  12. E. BRINKSMA AND K.G. LARSEN (EDITORS). Computer Aided Verification, 14th International Conference (CAV 2002) volume 2404 of Lecture Notes in Computer Science. Springer-Verlag, 2002.
  13. E. BRINKSMA, H. HERMANNS AND J.-P. KATOEN (EDITORS). Lectures on Formal Methods and Performance Analysis. volume 2090 in Lecture Notes in Computer Science (Tutorial). Springer-Verlag, 2001.
  14. H. HERMANNS. Interactive Markov Chains: The Quest for Quantified Quality. volume 2428 in Lecture Notes in Computer Science, 2002.
  15. J.-P. KATOEN AND P. STEVENS (EDITORS). Tools and Algorithms for the Construction and Analysis of Computer Systems. volume 2280 in Lecture Notes in Computer Science. Springer-Verlag, 2002.
  16. Conference contributions

  17. C. BAIER, B. HAVERKORT, H. HERMANNS AND J.-P. KATOEN. Model checking continuous-time Markov chains by transient analysis. In E.A. Emerson and A. Sistla, editors, Computer-Aided Verification (CAV), volume 1855 of Lecture Notes in Computer Science, pages 358-372, 2000.
  18. C. BAIER, J.-P. KATOEN, H. HERMANNS AND B. HAVERKORT. Simulation for continuous-time Markov chains. In L. Brim, P. Jancar, M. Kretinzki and A. Kucera, editors, Concurrency Theory (CONCUR), volume 2421 of Lecture Notes in Computer Science, pages 338-354, 2002.
  19. C. BAIER, B. HAVERKORT, H. HERMANNS AND J.-P. KATOEN. On the logical characterisation of performability properties. In U. Montanari, J.D.P. Rolim, E. Welzl, editors, Automata, Languages and Programming (ICALP), volume 1853 of Lecture Notes in Computer Science, pages 780-792, 2000.
  20. G. BEHRMANN, A. FEHNKER, T. HUNE, K.G. LARSEN, P. PETTERSSON, J.M.T. ROMIJN AND F. VAANDRAGER. Minimum-cost reachability for priced timed automata. In M.D. Di Benedetto and A.L. Sangiovanni-Vincentelli, editors, Proceedings HSCC'01, LNCS 2034, pages 147-164, 2001.
  21. G. BEHRMANN, T. HUNE AND F.W. VAANDRAGER. Distributed Timed Model Checking - How the Search Order Matters. In E.A. Emerson and A.P. Sistla, editors. Proceedings Computer-Aided Verification (CAV), LNCS 1855, pages 216-231, 2000.
  22. H. BOHNENKAMP, H. HERMANNS, J.-P. KATOEN AND R. KLAREN. The MoDeST modelling tool and its implementation. In P. Kemper and W.H. Sanders, editors, Modelling Techniques and Tools for Computer Performance Evaluation (TOOLS), volume 2794 of Lecture Notes in Computer Science, pages 116-133, 2003.
  23. H. BOHNENKAMP, P. VAN DER STOK, H. HERMANNS, AND F. VAANDRAGER. Cost-Optimisation of the IPv4 Zeroconf Protocol. In Proceedings of the International Conference on Dependable Systems and Networks (DSN'03), IEEE CS Press, pages 531-540, 2003.
  24. E. BRINKSMA AND A. MADER. Verification and optimization of a PLC control schedule. In K. Havelund, J. Penix, and W. Visser, editors, SPIN Model Checking and Software Verification, volume 1885 of Lecture Notes in Computer Science, pages 73-92, 2000.
  25. P.R. D'ARGENIO, H. HERMANNS, J.-P. KATOEN AND J. KLAREN. MoDeST: A Modelling language for Stochastic Timed systems. In L. de Alfaro and S. Gilmore, editors, Process Algebra and Probabilistic Methods, volume 2165 of Lecture Notes in Computer Science, pages 87-103, 2001.
  26. P.R. D'ARGENIO, J.-P. KATOEN AND E. BRINKSMA. Specification and analysis of soft real-time systems: quality and quantity. IEEE Real-Time Systems Symposium (RTSS), pages 104-114, IEEE CS Press, 1999.
  27. A. FEHNKER, M. ZHANG AND F.W. VAANDRAGER. Modeling and Verifying a Lego Car Using Hybrid I/O Automata. In Third International Conference on Quality Software (QSIC 2003), IEEE CS Press, 2003 (to appear). Full version in M. Broy and M. Pizka, editors. Models, Algebras, and Logic of Engineering Software, Nato ASI Series III: Computer and Systems Sciences, Volume 191, pages 385-402, IOS Press, 2003.
  28. B. HAVERKORT, L. CLOTH, H. HERMANNS, J.-P. KATOEN AND C. BAIER. Model-checking performability properties. International Conference on Dependable Systems and Networks (DSN), pages 103-113, IEEE CS Press, 2002.
  29. B. HAVERKORT, H. HERMANNS, AND J.-P. KATOEN. The use of model checking techniques for quantitative dependability evaluation. IEEE Symposium on Reliable Distributed Systems (SRDS), IEEE Computer Society Press, pp. 228-238, 2000.
  30. M. HENDRIKS, G. BEHRMANN, K.G. LARSEN, AND F. VAANDRAGER. Adding Symmetry Reduction to Uppaal. In P. Niebert and K.G. Larsen, editors, Proceedings First International Workshop on Formal Modeling and Analysis of Timed Systems (FORMATS 2003), 2003 (to appear).
  31. H. HERMANNS AND J.-P. KATOEN. Performance analysis := (process algebra + model checking) $\times$ Markov chains. In K.G. Larsen and M. Nielsen, editors, Concurrency Theory (CONCUR), volume 2154 of Lecture Notes in Computer Science, pages 59-82. 2001 (invited tutorial).
  32. H. HERMANNS, J.-P. KATOEN, J. MEYER-KAYSER AND M. SIEGLE. A Markov chain model checker. In S. Graf and M. Schwartzbach, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 1785 of Lecture Notes in Computer Science, pages 357-373, 2000.
  33. H. HERMANNS, J.-P. KATOEN, J. MEYER-KAYSER AND M. SIEGLE. Towards model checking stochastic process algebra. In W. Grieskamp, T. Santen and B. Stoddart, editors, Integrated Formal Methods (IFM), volume 1945 of Lecture Notes in Computer Science, pages 420-439, 2000.
  34. J.-P. KATOEN, M.Z. KWIATKOWSKA, G. NORMAN AND D. PARKER. Faster and symbolic CTMC model checking. In L. de Alfaro and S. Gilmore, editors, Process Algebra and Probabilistic Methods, volume 2165 of Lecture Notes in Computer Science, pages 23-38, 2001.
  35. K. G. LARSEN, G. BEHRMANN, H. BRINKSMA, A. FEHNKER, P. PETTERSSON, AND J. M. T. ROMIJN. As cheap as possible: Efficient cost-optimal reachability for priced timed automata. In G. Berry and P. Cousot, editors, Computer Aided Verification (CAV), volume 2102 of Lecture Notes in Computer Science, pages 493-505, 2001.
  36. N.A. LYNCH, R. SEGALA AND F.W. VAANDRAGER. Compositionality for Probabilistic Automata. In R. Amadio and D. Lugiez, editors. Proceedings 14th International Conference on Concurrency Theory (CONCUR 2003), LNCS 2761, pages 208-221. 2003.
  37. N.A. LYNCH, R. SEGALA AND F.W. VAANDRAGER. Hybrid I/O automata revisited. In M.D. Di Benedetto and A.L. Sangiovanni-Vincentelli, editors. Proceedings HSCC'01, LNCS 2034, pages 403-417, 2001.
  38. T. RUYS, R. LANGERAK, J.-P. KATOEN, D. LATELLA AND M. MASSINK. First passage time analysis of stochastic process algebra using partial orders. In T. Margaria and W. Yi, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 2031 of Lecture Notes in Computer Science, pages 220-236, 2001.
  39. M. STOELINGA AND F.W. VAANDRAGER. A Testing Scenario for Probabilistic Automata. In J.C.M. Baeten, J.K. Lenstra, J. Parrow and G.J. Woeginger, editors. Proceedings International Colloquium on Automata, Languages and Programming (ICALP), LNCS 2719, pages 407-418, 2003.
  40. D.K. KAYNAR, N.A. LYNCH, R. SEGALA, AND F.W. VAANDRAGER. A Framework for Modelling Timed Systems with Restricted Hybrid Automata. In Proceedings 24th IEEE International Real-Time Systems Symposium (RTSS03), 2003. IEEE Computer Society, pages 166-177, 2003.
  41. Other publications

  42. H. BOHNENKAMP, H. HERMANNS, M. ZHANG AND F. VAANDRAGER. Cost-Optimisation of the IPv4 Zeroconf Protocol. Proceedings of the 3rd PROGRESS Workshop on Embedded Systems, 2002.
  43. H. BOHNENKAMP, T. COURTNEY, D. DALY, S. DERISAWI, H. HERMANNS, J.-P. KATOEN, J. KLAREN, V. LAM AND W.H. SANDERS. On integrating the Möbius and Modest modeling tools. Proceedings International Conference on Dependable Systems and Networks (DSN), 2003 (tool demo paper).
  44. E. BRINKSMA AND H. HERMANNS. Process algebra and Markov chains. In H. Brinksma, H. Hermanns, and J. P. Katoen, editors, Lectures on Formal Methods and Performance Analysis, volume 2090 of Lecture Notes in Computer Science, pages 183-232, 2001.
  45. E. BRINKSMA AND J.-P. KATOEN. Hooggespannen verwachtingen model checking. Bits & Chips, vol. 3, no. 4, pages 31-33, 2001 (in Dutch).
  46. P.R. D'ARGENIO. A Compositional translation of stochastic automata into timed automata. CTIT Technical Report 00-08, 2000.
  47. P.R. D'ARGENIO AND J.-P. KATOEN. A theory of stochastic systems, part I: Stochastic automata. 2003, submitted.
  48. P.R. D'ARGENIO AND J.-P. KATOEN. A theory of stochastic systems, part II: Process algebra. 2003, submitted.
  49. P.R. D'ARGENIO, H. HERMANNS, J.-P. KATOEN AND J. KLAREN. Modelling stochastic systems (extended abstract). In F. Karelse, editor, 2nd Workshop on Embedded Systems pages 31-39, 2001.
  50. J. GORTER. Arrays and structures in Modest and Möbius. Stage report at University of Illinois at Urbana-Champaign, 2003.
  51. J. GORTER. Modeling and analysis of the UPnP liveness protocol. Master's thesis, Universiteit Twente, 2004.
  52. H. HERMANNS, J.-P. KATOEN, J. MEYER-KAYSER AND M. SIEGLE. A model checker for performance and dependability properties (extended abstract). In F. Karelse, editor, 2nd Workshop on Embedded Systems, pages 83-89, 2001.
  53. J.-P. KATOEN AND P.R. D'ARGENIO. General distributions in process algebra. In E. Brinksma, H. Hermanns, and J.-P. Katoen, editors, Lectures on Formal Methods and Performance Analysis (FMPA), volume 2090 of Lecture Notes in Computer Science, pages 375-424, 2001.
  54. J.-P. KATOEN. Real-time and probabilistic systems - Foreword. Theoretical Computer Science, vol. 282, no. 1, pages 1-3, 2002.
  55. B. GEBREMICHAEL, F.W. VAANDRAGER, AND M. ZHANG. Formal Models of Guaranteed and Best-Effort Services for Networks on Chip. 2004 (in preparation).
  56. M. ZHANG AND F.W. VAANDRAGER. Analysis of a Protocol for Dynamic Configuration of IPv4 Link Local Addresses using Uppaal. Technical Report NIII-R04XX, NIII, University of Nijmegen, 2004 (in preparation).


May 6, 2004
Henrik Bohnenkamp