Jansen, David N.: Erratum to: Model-checking continuous-time Markov chains by Aziz et al. Eprint arXiv: 1102.2079, 2011. Online version
Jansen, David N.: Understanding Fox and Glynn’s “Computing Poisson probabilities”. Nijmegen: Radboud Universiteit, 2011. (Technical report, ICIS-R11001) Online version
Katoen, Joost-Pieter; Zapreev, Ivan S.; Hahn, Ernst Moritz; Hermanns, Holger; Jansen, David N.: The ins and outs of the probabilistic model checker MRMC. Performance Evaluation 68 (2), 2011. pp. 90–104. Online version
Zhang, Lijun; Jansen, David N.; Nielson, Flemming; Hermanns, Holger: Automata-based CSL model checking. In: Aceto, Luca; Henzinger, Monika; Sgall, Jiří (eds.): Automata, languages and programming: ... ICALP. Part II. Berlin: Springer, 2011. (Lecture notes in computer science, 6756). pp. 271–282. Online version
Zhang, Lijun; Jansen, David N.; Nielson, Flemming; Hermanns, Holger: Automata-based CSL model checking. Eprint arXiv: 1104.4983, 2011. Online version
Berendsen, Jasper; Jansen, David N.; Schmaltz, Julien; Vaandrager, Frits W.: The axiomatization of override and update. Journal of applied logic 8 (1), 2010. pp. 141–150. Online version
Berendsen, Jasper; Jansen, David N.; Vaandrager, Frits: Fortuna: model checking priced probabilistic timed automata. In: QEST 2010: Seventh international conference on the quantitative evaluation of systems. Los Alamitos, CA: IEEE Computer Society, 2010. pp. 273–281. Online version
Jansen, D. N.; Klabes, S. G.; Wendler, E.: The impact of GSM-R on railway capacity. In: Ning, B.: Advanced train control systems. Southampton: WIT, 2010. pp. 143–152. Online information
Mader, Angelika; Bohnenkamp, Henrik; Usenko, Yaroslav S.; Jansen, David N.; Hurink, Johann; Hermanns, Holger: Synthesis and stochastic assessment of cost-optimal schedules. International journal on software tools for technology transfer 12 (5), 2010. pp. 305–318. Online version
Berendsen, Jasper; Chen, Taolue; Jansen, David N.: Undecidability of cost-bounded reachability in priced probabilistic timed automata. In: Chen, Jianer; Cooper, S. Barry (eds.): Theory and applications of models of computation: ... TAMC. Berlin: Springer, 2009. (Lecture notes in computer science, 5532). pp. 128–137. Online version
Errata:
Katoen, Joost-Pieter; Zapreev, Ivan S.; Hahn, Ernst Moritz; Hermanns, Holger; Jansen, David N.: The ins and outs of the probabilistic model checker MRMC. In: Sixth international conference on the quantitative evaluation of systems: QEST 2009. Los Alamitos, CA: IEEE Computer Society, 2009. pp. 167–176. Online version
Vaandrager, Frits; Jansen, David N.; Koopmans, Els: Een module over modelchecking voor het vwo. In: Vodegel, Frans; Loots, Marijke (ed.): NIOC proceedings. Hogeschool Utrecht, 2009. pp. 135–137. Online version
Jansen, D. N.; Klabes, S. G.; Wendler, E.: The impact of GSM-R on railway capacity. In: Allan, J.; Arias, E.; Brebbia, C. A.; Goodman, C.; Rumsey, A. F.; Sciutto, G.; Tomii, N.: Computers in railways XI. Southampton: WIT, 2008. pp. 233–242. Online version
Zhang, Lijun; Hermanns, Holger; Eisenbrand, Friedrich; Jansen, David N.: Flow faster: efficient decision algorithms for probabilistic simulations. Logical methods in computer science 4 (4), 2008. paper 6. Online version
Jansen, David N.; Katoen, Joost-Pieter; Oldenkamp, Marcel; Stoelinga, Mariëlle; Zapreev, Ivan: How fast and fat is your probabilistic model checker? An experimental performance comparison. In: Yorav, Karen (ed.): Hardware and software, verification and testing: ... Haifa verification conference, HVC. Berlin: Springer, 2008. (Lecture notes in computer science, 4899). pp. 69–85. Online version
Katoen, Joost-Pieter; Kemna, Tim; Zapreev, Ivan; Jansen, David N.: Bisimulation minimisation mostly speeds up probabilistic model checking. In: Grumberg, Orna; Huth, Michael (eds.): Tools and algorithms for the construction and analysis of systems: ... TACAS. Berlin: Springer, 2007. (Lecture notes in computer science, 4424). pp. 87–101. Online version
Zhang, Lijun; Hermanns, Holger; Eisenbrand, Friedrich; Jansen, David N.: Flow faster: efficient decision algorithms for probabilistic simulations. In: Grumberg, Orna; Huth, Michael (eds.): Tools and algorithms for the construction and analysis of systems: ... TACAS. Berlin: Springer, 2007. (Lecture notes in computer science, 4424). pp. 155–169. Online version
Berendsen, Jasper; Jansen, David N.; Katoen, Joost-Pieter: Probably on time and within budget: On reachability in priced probabilistic timed automata. In: Third international conference on the quantitative evaluation of systems: QEST 2006. Los Alamos, CA: IEEE Computer Society, 2006. pp. 311–322. Online version
Berendsen, Jasper; Jansen, David N.; Katoen, Joost-Pieter: Probably on time and within budget: On reachability in priced probabilistic timed automata. Enschede: Centre for Telematics and Information Technology, University of Twente, 2006. (Technical report, TR-CTIT-06-26) Online version
Mader, Angelika; Bohnenkamp, Henrik; Usenko, Yaroslav S.; Jansen, David N.; Hurink, Johann; Hermanns, Holger: Synthesis and stochastic assessment of cost-optimal schedules. Enschede: Centre for Telematics and Information Technology, University of Twente, 2006. (Technical report, TR-CTIT-06-14) Online version
Hermanns, Holger; Jansen, David N.; Usenko, Yaroslav S.: A comparative reliability analysis of ETCS train radio communications. Transregional Collaborative Research Center 14 AVACS, Germany, February 2005. (Technical report, 2) Online version
Hermanns, Holger; Jansen, David N.; Usenko, Yaroslav S.: From StoCharts to MoDeST: a comparative reliability analysis of train radio communications. In: Proceedings of the 5th international workshop on software and performance. Santa Fe, NM: ACM Press, 2005. pp. 13–23. Online version
Jansen, David N.; Hermanns, Holger: QoS modelling and analysis with UML-statecharts: the StoCharts approach. ACM SIGMETRICS Performance Evaluation Review, 32 (4), 2005. pp. 28–33. Online version
Zhang, Lijun; Hermanns, Holger; Jansen, David N.: Logic and model checking for hidden Markov models. In: Wang, Farn (ed.): Formal techniques for networked and distributed systems, FORTE 2005. Berlin: Springer, 2005. (Lecture notes in computer science, 3731) pp. 98–112. Online version
Zhang, Lijun; Hermanns, Holger; Jansen, David N.: Logic and model checking for hidden Markov models. Transregional Collaborative Research Center 14 AVACS, Germany, July 2005. (Technical report, 6) Online version
Bohnenkamp, Henrik C.; Hermanns, Holger; Jansen, David N.; Katoen, Joost-Pieter; Usenko, Yaroslav S.: An industrial-strength formal method: a modest survey. In: Margaria, Tiziana; Steffen, Bernhard; Philippou, Anna; Reitenspieß, Manfred (eds.): International symposium on leveraging applications of formal methods: ISoLA; preliminary proceedings. Dept. of Computer Science, University of Cyprus, 2004. (Technical Report, TR-2004-6) pp. 284–295.
Jansen, David N.; Hermanns, Holger: Dependability checking with StoCharts: Is train radio reliable enough for trains? In: QEST 2004: First international conference on the quantitative evaluation of systems. Los Alamos, CA: IEEE Computer Society, 2004. pp. 250–259. Online version
Jansen, David Nicolaas: Extensions of Statecharts: with probability, time, and stochastic timing. PhD thesis, University of Twente. Bern: Inmarks, 2003. Online version
Jansen, David N.; Hermanns, Holger; Katoen, Joost-Pieter: A QoS-oriented extension of UML statecharts. In: Stevens, Perdita; Whittle, Jon; Booch, Grady (eds.): «UML» 2003, the unified modeling language. Berlin: Springer, 2003. (Lecture notes in computer science, 2863) pp. 76–91. Online version
Eshuis, Rik; Jansen, David N.; Wieringa, Roel: Requirements-level semantics and model checking of object-oriented statecharts. Requirements Engineering, 7 (4, special issue on model checking), December 2002. pp. 243–263. Online version
Jansen, David N.: Probabilistic UML statecharts for specification and verification: a case study. In: Critical systems development with UML: proceedings of the UML'02 workshop. München: Technische Universität, 2002. (Technical report, TUM-I0208) pp. 121–131. Online version
Jansen, David N.; Hermanns, Holger; Katoen, Joost-Pieter: A probabilistic extension of UML statecharts: specification and verification. In: Damm, Werner; Olderog, Ernst-Rüdiger (eds.): Formal techniques in real-time and fault-tolerant systems: ... FTRTFT. Berlin: Springer, 2002. (Lecture notes in computer science, 2469) pp. 355–374. Online version
Jansen, David N.; Hermanns, Holger; Katoen, Joost-Pieter: A probabilistic extension of UML statecharts: specification and verification. Enschede: Centre for Telematics and Information Technology, University of Twente, 2002. (Technical report, TR-CTIT-02-31) Online version
Jansen, David N.; Wieringa, Roel J.: Extending CTL with actions and real time. Journal of logic and computation, 12 (4), 2002. pp. 607–621. Online version
Wieringa, Roel J.; Jansen, David N.: Techniques for reactive system design: the tools in TRADE. In: Dittrich, Klaus R.; Geppert, Andreas; Norrie, Moira C. (eds.): Advanced information systems engineering: ... CAiSE. Berlin: Springer, 2001. (Lecture notes in computer science, 2068) pp. 93–107. Online version
Jansen, David N.; Wieringa, Roel J.: Extending CTL with actions and real-time. In: International conference on temporal logic. s.l.: s.n., 2000. pp. 105–114. (An updated version appeared in the Journal of logic and computation 12 (4), 2002, see above.)
Jansen, David N.; Wieringa, Roel J.: Reducing the extensions of CTL with actions and real time. Enschede: Centre for Telematics and Information Technology, University of Twente, 2000. (Technical report, TR-CTIT-00-27) Online version
van de Goor, Martin: Indoor localization in wireless sensor networks. Finished March 2009.
Oldenkamp, Marcel: Experimental comparison of probabilistic model checkers. Finished May 2007. (See also our publication How fast and fat is your probabilistic model checker? in 2007.)
ter Horst, Ivo: Performance evaluation in an early development phase. Finished February 2007.
From the abstract: Performance evaluation of combat management systems at Thales Naval Nederland is
currently performed too late in the development process. Failure to meet performance goals
can be costly and should be avoided, so early discovery of problems is important. Instead
of the calculations in large Excel sheets which were used, this thesis presents a UML model
with which the structure and performance information of a system can clearly be defined.
Performance information can be added to all elements of the structural model of a system
in terms of budgets. A budget defines an amount of resources provided by the hardware
or required by the software system.
As the UML models of systems tend to grow large and a lot of budgets and constraints are
added, evaluation of the constraints becomes a hard task. Automatic constraint verification
is therefore provided by our System Verifier Tool, which integrates with Rational Software
Architect (RSA), the tool used within Thales to create UML models.
Kemna, Tim: Bisimulation Minimisation and Probabilistic Model Checking. Finished August 2006. (See also our publication Bisimulation minimisation mostly speeds up probabilistic model checking in 2007.)
Berendsen, Jasper: Reachability in Weighted Probabilistic Timed Automata. Finished December 2005. (See also our publications Probably on time and within budget in 2006.)
December 2011, David N. Jansen