Jean-Raymond Abrial (1996):
The B Book: Assigning Programs to Meanings.
Cambridge University Press,
doi:10.1017/CBO9780511624162.
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.
C. Baier & J. P. Katoen (2008):
Principles of Model Checking.
MIT Press,
New York.
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.
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.
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.
Matthias Fruth (2011):
Formal Methods for the Analysis of Wireless Network Protocols.
University of Oxford.
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.
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.
D. N. Jansen (2003):
Extensions of Statecharts with Probability, Time, and Stochastic Timing.
University of Twente,
Enschede.
Available at http://doc.utwente.nl/58230/.
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.
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.
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.
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.
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.
Bojan Nokovic & Emil Sekerinski (2010):
Analysis of Interrogator-tag Communication Protocols.
SQRL Report 60.
McMaster University.
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.
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.
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.
H.A. Oldenkamp (2007):
Probabilistic model checking : a comparison of tools.
University of Twente.
Available at http://essay.utwente.nl/591/.
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 http://profs.sci.univr.it/~segala/www/phd.html.
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.
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.
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.
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.
eptcs@eptcs.org