TCS / Research / Publications / Publications of the project
Symbolic Methods for UML Behavioural Diagrams (SMUML)

Helsinki University of Technology, 
     Laboratory for Theoretical Computer Science

Publications of the project
Symbolic Methods for UML Behavioural Diagrams (SMUML)

2008

15Vesa Ojala. Counterexample analysis for automated refinement of data abstracted state machine models. Master's thesis, Helsinki University of Technology, Department of Information and Computer Science, 2008.
PostScript (1 MB)
GZipped PostScript (572 kB)
PDF (532 kB)
Info
14Jori Dubrovin, Tommi Junttila, and Keijo Heljanko. Symbolic step encodings for object based communicating state machines. In Gilles Barthe and Frank S. de Boer, editors, Proceedings of the 10th IFIP International Conference on Formal Methods for Open Object-based Distributed Systems (FMOODS'08), volume 5051 of Lecture Notes in Computer Science, pages 96–112. Springer, 2008.
Info
See www.tcs.hut.fi ...
13Jori Dubrovin and Tommi Junttila. Symbolic model checking of hierarchical UML state machines. In Jonathan Billington, Zhenhua Duan, and Maciej Koutny, editors, Proceedings of the 8th International Conference on Application of Concurrency to System Design (ACSD'08), pages 108–117. IEEE Press, 2008.
Info
See ieeexplore.ieee.org ...

2007

12Jori Dubrovin and Tommi Junttila. Symbolic model checking of hierarchical UML state machines. Technical Report B23, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, December 2007.
PostScript (879 kB)
GZipped PostScript (449 kB)
PDF (223 kB)
Info
11Jori Dubrovin, Tommi Junttila, and Keijo Heljanko. Symbolic step encodings for object based communicating state machines. Technical Report B24, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, December 2007.
PostScript (984 kB)
GZipped PostScript (462 kB)
PDF (265 kB)
Info
10Vesa Ojala. A slicer for UML state machines. Technical Report B25, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, December 2007.
PostScript (830 kB)
GZipped PostScript (265 kB)
PDF (307 kB)
Info
9Jori Dubrovin. SMUML/Suboco 1.10 — an SMT-based UML bounded model checker, 2007. Computer program.
Info
See www.tcs.hut.fi ...
8Jori Dubrovin. SMUML/Uboco 1.10 — a translator from UML models to NuSMV programs, 2007. Computer program.
Info
See www.tcs.hut.fi ...
7Tommi Junttila. SMUML/proco version 2.00 — a translator from UML models to Promela, 2007. Computer program.
Info
See www.tcs.hut.fi ...
6Tommi Junttila. PySMT version 0.50 — a Python front-end for satisfiability modulo theories solvers, 2007. Computer program.
Info
See www.tcs.hut.fi ...
5Vesa Ojala. SMUML/slicer 1.0.0 — a slicer for slicing UML state machines, 2007. Computer program.
Info
See www.tcs.hut.fi ...
4Vesa Ojala. SMUML/canal 1.0.0 — a counterexample analysator for analyzing abstract counterexamples from data abstracted UML models, 2007. Computer program.
Info
See www.tcs.hut.fi ...

2006

3Jori Dubrovin. Jumbala — an action language for UML state machines. Research Report A101, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, March 2006.
NOTE: Reprint of Master's thesis; see URL below.
PostScript (809 kB)
GZipped PostScript (307 kB)
PDF (499 kB)
Info
See www.tcs.hut.fi ...
2Jori Dubrovin. Jumbala — an action language for UML state machines. Master's thesis, Helsinki University of Technology, Department of Engineering Physics and Mathematics, 2006.
Info
See www.tcs.hut.fi ...
1Toni Jussila, Jori Dubrovin, Tommi Junttila, Timo Latvala, and Ivan Porres. Model checking dynamic and hierarchical UML state machines. In MoDeVa: Model Development, Validation and Verification; 3rd International Workshop, Genova, Italy, October 2006, pages 94–110, 2006.
Info
See modeva.itee.uq.edu.au ...

[TCS main] [Contact Info] [Personnel] [Research] [Publications] [Software] [Studies] [News Archive] [Links]
Latest update: 19 January 2010.