1. Jean-Raymond Abrial (1996): The B Book: Assigning Programs to Meanings. Cambridge University Press, doi:10.1017/CBO9780511624162.
  2. Adnan Aziz, Vigyan Singhal, Felice Balarin, RobertK. Brayton & AlbertoL. Sangiovanni-Vincentelli (1995): It usually works: The temporal logic of stochastic systems. In: Pierre Wolper: Computer Aided Verification, Lecture Notes in Computer Science 939. Springer Berlin Heidelberg, pp. 155–165, doi:10.1007/3-540-60045-0\voidb@x width0.5em48.
  3. C. Baier & J. P. Katoen (2008): Principles of Model Checking. MIT Press, New York.
  4. Edmund M. Clarke & E.Allen Emerson (1982): Design and synthesis of synchronization skeletons using branching time temporal logic. In: Dexter Kozen: Logics of Programs, Lecture Notes in Computer Science 131. Springer Berlin Heidelberg, pp. 52–71, doi:10.1007/BFb0025774.
  5. Edmund M. Clarke & Paolo Zuliani (2011): Statistical Model Checking for Cyber-Physical Systems. In: Tevfik Bultan & Pao-Ann Hsiung: Automated Technology for Verification and Analysis, Lecture Notes in Computer Science 6996. Springer Berlin Heidelberg, pp. 1–12, doi:10.1007/978-3-642-24372-1\voidb@x width0.5em1.
  6. Rik Eshuis, David N. Jansen & Roel Wieringa (2002): Requirements-Level Semantics and Model Checking of Object-Oriented Statecharts. Requirements Engineering V7(4), pp. 243–263, doi:10.1007/s007660200019.
  7. Matthias Fruth (2011): Formal Methods for the Analysis of Wireless Network Protocols. University of Oxford.
  8. David Harel & Hillel Kugler (2004): The Rhapsody Semantics of Statecharts (or, On the Executable Core of the UML). In: Hartmut Ehrig, Werner Damm, Jörg Desel, Martin Große-Rhode, Wolfgang Reif, Eckehard Schnieder & Engelbert Westkämper: Integration of Software Specification Techniques for Applications in Engineering, Lecture Notes in Computer Science 3147. Springer Berlin Heidelberg, pp. 325–354, doi:10.1007/978-3-540-27863-4\voidb@x width0.5em19.
  9. David Harel & Amnon Naamad (1996): The STATEMATE Semantics of Statecharts. ACM Trans. Softw. Eng. Methodol. 5(4), pp. 293–333, doi:10.1145/235321.235322.
  10. D. N. Jansen (2003): Extensions of Statecharts with Probability, Time, and Stochastic Timing. University of Twente, Enschede. Available at
  11. D.N. Jansen, H. Hermanns & J.P. Katoen (2002): A probabilistic extension of UML statecharts: Specification and Verification.. In: W. Damm & E.-R. Olderog: Formal Techniques in Real-Time and Fault-Tolerant Systems, Lecture Notes in Computer Science 2469. Springer, Oldenburg, Germany, pp. 355–374, doi:10.1007/3-540-45739-9.
  12. Marta Kwiatkowska, Gethin Norman & David Parker (2009): Stochastic Games for Verification of Probabilistic Timed Automata. In: Proceedings of the 7th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS '09. Springer-Verlag, Berlin, Heidelberg, pp. 212–227, doi:10.1007/978-3-642-04368-0\voidb@x width0.5em17.
  13. Marta Kwiatkowska, Gethin Norman & David Parker (2011): PRISM 4.0: Verification of Probabilistic Real-Time Systems. In: Ganesh Gopalakrishnan & Shaz Qadeer: Computer Aided Verification, Lecture Notes in Computer Science 6806. Springer Berlin Heidelberg, pp. 585–591, doi:10.1007/978-3-642-22110-1\voidb@x width0.5em47.
  14. Marta Kwiatkowska, Gethin Norman, Jeremy Sproston & Fuzhi Wang (2007): Symbolic model checking for probabilistic timed automata. Information and Computation 205(7), pp. 1027 – 1077, doi:10.1016/j.ic.2007.01.004. Available at
  15. Marta Z. Kwiatkowska, Gethin Norman, David Parker & Jeremy Sproston (2006): Performance analysis of probabilistic timed automata using digital clocks. Formal Methods in System Design 29(1), pp. 33–78, doi:10.1007/s10703-006-0005-2.
  16. Florian Leitner-Fischer & Stefan Leue (2011): QuantUM: Quantitative Safety Analysis of UML Models. In: Mieke Massink & Gethin Norman: Proceedings Ninth Workshop on Quantitative Aspects of Programming Languages, Saarbrücken, Germany, April 1-3, 2011, Electronic Proceedings in Theoretical Computer Science 57. Open Publishing Association, pp. 16–30, doi:10.4204/EPTCS.57.2.
  17. Gerald Löttgen & Michael Mendler (2000): Fully-Abstract Statecharts Semantics via Intuitionistic Kripke Models.. In: ICALP, Lecture Notes in Computer Science 1853. Springer, pp. 163–174, doi:10.1007/3-540-45022-X\voidb@x width0.5em14. Available at
  18. Carroll Morgan, Annabelle McIver & Karen Seidel (1996): Probabilistic Predicate Transformers. ACM Trans. Program. Lang. Syst. 18(3), pp. 325–353, doi:10.1145/229542.229547. Available at
  19. Bojan Nokovic & Emil Sekerinski (2010): Analysis of Interrogator-tag Communication Protocols. SQRL Report 60. McMaster University.
  20. Bojan Nokovic & Emil Sekerinski (2013): pState: A probabilistic statecharts translator. In: Embedded Computing (MECO), 2013 2nd Mediterranean Conference on, pp. 29–32, doi:10.1109/MECO.2013.6601339.
  21. Bojan Nokovic & Emil Sekerinski (2014): Verification and Code Generation for Timed Transitions in pCharts. In: Proceedings of the 2014 International C* Conference on Computer Science #38; Software Engineering, C3S2E '14. ACM, New York, NY, USA, pp. 3:1–3:10, doi:10.1145/2641483.2641522.
  22. G. Norman, D. Parker & J. Sproston (2012): Model checking for probabilistic timed automata. Formal Methods in System Design, pp. 1–27, doi:10.1007/s10703-012-0177-x.
  23. H.A. Oldenkamp (2007): Probabilistic model checking : a comparison of tools. University of Twente. Available at
  24. Roberto Segala (1995): Modelling and Verification of Randomized Distributed Real Time Systems. Ph.D. thesis, Technical Report MIT/LCS/TR-676. Massachusetts Institute of Technology. Available at
  25. E. Sekerinski (2008): Verifying Statecharts with State Invariants. In: Proceedings of the 13th IEEE International Conference on on Engineering of Complex Computer Systems. IEEE Computer Society, Washington, DC, USA, pp. 7–14, doi:10.1109/ICECCS.2008.40.
  26. E. Sekerinski & R. Zurob (2001): iState: A Statechart Translator. In M. Gogolla and C. Kobryn, editors UML 2001 - The Unified Modeling Language, 4th International Conference, Lecture Notes in Computer Science 2185, pages 376-390, Toronto, Canada, doi:10.1007/3-540-45441-1\voidb@x width0.5em28.
  27. Emil Sekerinski (2009): Design Verification with State Invariants. In: Kevin Lano: UML 2 Semantics and Applications. John Wiley & Sons, pp. 317–347, doi:10.1002/9780470522622.
  28. Yefei Zhao, Zongyuan Yang, Jinkui Xie & Qiang Liu (2010): Quantitative Analysis of System Based on Extended UML State Diagrams and Probabilistic Model Checking. JSW 5(7), pp. 793–800, doi:10.4304/jsw.5.7.793-800.

Comments and questions to:
For website issues: