@inproceedings(anderson1996model,
 author       = "Richard J Anderson and Paul Beame and Steve Burns and William Chan and Francesmary Modugno and David Notkin and Jon D Reese",
 year         = "1996",
 title        = "Model checking large software specifications",
 booktitle    = "ACM SIGSOFT Software Engineering Notes",
 volume       = "21",
 organization = "ACM",
 pages        = "156--166",
 doi          = "10.1145/239098.239127",
)
@book(baier/08,
 author       = "C. Baier and J.-P. Katoen",
 year         = "2008",
 title        = "Principles of model checking",
 publisher    = "MIT Press",
 address      = "Cambridge, MA, USA",
 url          = "http://mitpress.mit.edu/books/principles-model-checking",
 note         = "975 p.",
)
@inproceedings(baresi/12,
 author       = "L. Baresi and A. Morzenti and A. Motta and M. Rossi",
 year         = "2012",
 title        = "Towards the UML-Based Formal Verification of Timed Systems",
 booktitle    = "F. Meth. for Components and Objects",
 organization = "Springer",
 pages        = "267--286",
 doi          = "10.1007/978-3-642-25271-6",
)
@article(behrmann2004tutorial,
 author       = "G. Behrmann and A. David and K. Larsen",
 year         = "2004",
 title        = "A tutorial on uppaal",
 journal      = "Formal methods for the design of real-time systems",
 pages        = "33--35",
 doi          = "10.1007/978-3-540-30080-9-7",
)
@book(cockburn,
 author       = "Alistair Cockburn",
 year         = "2000",
 title        = "Writing Effective Use Cases",
 edition      = "1st",
 publisher    = "Addison-Wesley Longman Publishing Co., Inc.",
 address      = "Boston, MA, USA",
 url          = "http://dl.acm.org/citation.cfm?id=517669",
)
@article(cortellessa2002prima,
 author       = "V. Cortellessa and R. Mirandola",
 year         = "2002",
 title        = "PRIMA-UML: a performance validation incremental methodology on early UML diagrams",
 journal      = "SC Programming",
 volume       = "44",
 number       = "1",
 pages        = "101--129",
 doi          = "10.1016/S0167-6423(02)00033-3",
)
@book(debbabi/10,
 author       = "M. Debbabi and F. Hassa{\"i}ne and Y. Jarraya and A. Soeanu and L. Alawneh",
 year         = "2010",
 title        = "Verification and Validation in Systems Engineering",
 publisher    = "Springer",
 address      = "Berlin, Heidelberg - Germany",
 doi          = "10.1007/978-3-642-15228-3",
 note         = "270 p.",
)
@inproceedings(dubrovin2008symbolic,
 author       = "J. Dubrovin and T. Junttila",
 year         = "2008",
 title        = "Symbolic model checking of hierarchical UML state machines",
 booktitle    = "Application of Concurrency to System Design, 2008. 8th International Conference on",
 organization = "IEEE",
 pages        = "108--117",
 doi          = "10.1109/ACSD.2008.4574602",
)
@inproceedings(dwyer/99,
 author       = "M. B. Dwyer and G. S. Avrunin and J. C. Corbett",
 year         = "1999",
 title        = "Patterns in property specifications for finite-state verification",
 booktitle    = "Proceedings...",
 organization = "International Conference on Software Engineering (ICSE)",
 publisher    = "ACM",
 address      = "New York, NY, USA",
 pages        = "411--420",
 doi          = "10.1145/302405.302672",
)
@article(eshuis2006symbolic,
 author       = "R. Eshuis",
 year         = "2006",
 title        = "Symbolic model checking of UML activity diagrams",
 journal      = "ACM Transactions on Software Engineering and Methodology (TOSEM)",
 volume       = "15",
 number       = "1",
 pages        = "1--38",
 doi          = "10.1145/1125808.1125809",
)
@book(holzmann2004spin,
 author       = "G.J. Holzmann",
 year         = "2004",
 title        = "The SPIN model checker: Primer and reference manual",
 volume       = "1003",
 publisher    = "Addison-Wesley",
 url          = "http://spinroot.com/spin/Doc/Book_extras/",
)
@inproceedings(johnson2013incremental,
 author       = "K. Johnson and R. Calinescu and S. Kikuchi",
 year         = "2013",
 title        = "An Incremental Verification Framework for Component-based Software Systems",
 booktitle    = "Proceedings of the 16th International ACM Sigsoft Symposium on Component-based Software Engineering",
 series       = "CBSE '13",
 publisher    = "ACM",
 address      = "New York, NY, USA",
 pages        = "33--42",
 doi          = "10.1145/2465449.2465456",
)
@misc(NuSMV,
 author       = "FONDAZIONE BRUNO KESSLER",
 year         = "2011",
 title        = "NuSMV Home Page",
 url          = "http://nusmv.fbk.eu/",
)
@article(lam2007formalism,
 author       = "Vitus S. W. Lam",
 year         = "2007",
 title        = "A Formalism for Reasoning About UML Activity Diagrams",
 journal      = "Nordic J. of Computing",
 volume       = "14",
 number       = "1",
 pages        = "43--64",
 url          = "http://dl.acm.org/citation.cfm?id=1515784.1515786",
)
@inproceedings(merseguer2002compositional,
 author       = "J. Merseguer and J. Campos and S. Bernardi and S. Donatelli",
 year         = "2002",
 title        = "A Compositional Semantics for UML State Machines Aimed at Performance Evaluation",
 series       = "WODES '02",
 publisher    = "IEEE Computer Society",
 address      = "Washington, DC, USA",
 pages        = "295--",
 url          = "http://dl.acm.org/citation.cfm?id=832316.837588",
)
@inproceedings(mikk1998implementing,
 author       = "E. Mikk and Y. Lakhnech and M. Siegel and G.J. Holzmann",
 year         = "1998",
 title        = "Implementing statecharts in PROMELA/SPIN",
 booktitle    = "Industrial Strength Formal Specification Techniques, 1998.",
 organization = "IEEE",
 pages        = "90--101",
 doi          = "10.1109/WIFT.1998.766303",
)
@misc(umlref,
 author       = "The Object Management Group OMG",
 year         = "1997",
 title        = "OMG - Unified Modeling Language (OMG UML)",
 url          = "http://www.uml.org/",
)
@article(santiago/12,
 author       = "V. A. {Santiago J\'unior} and N. L. {Vijaykumar}",
 year         = "2012",
 title        = "Generating Model-Based Test Cases from Natural Language Requirements for Space Application Software",
 journal      = "Software Quality Journal",
 volume       = "20",
 number       = "1",
 pages        = "77--143",
 doi          = "10.1007/s11219-011-9155-6",
)
@article(schafer2001model,
 author       = "T. Sch{\"a}fer and A. Knapp and S. Merz",
 year         = "2001",
 title        = "Model checking UML state machines and collaborations",
 journal      = "Electronic Notes in Theoretical Computer Science",
 volume       = "55",
 number       = "3",
 pages        = "357--369",
 doi          = "10.1016/S1571-0661(04)00262-2",
)
@inproceedings(uchitel2001workbench,
 author       = "Sebastian Uchitel and Jeff Kramer",
 year         = "2001",
 title        = "A workbench for synthesising behaviour models from scenarios",
 booktitle    = "Proceedings of the 23rd intern. conference on Software engineering",
 organization = "IEEE Computer Society",
 pages        = "188--197",
 doi          = "10.1109/ICSE.2001.919093",
)
@article(woodcock/09,
 author       = "J. Woodcock and P. G. Larsen and J. Bicarregui and J. Fitzgerald",
 year         = "2009",
 title        = "Formal methods: Practice and experience",
 journal      = "ACM Computing Surveys",
 volume       = "41",
 number       = "4",
 pages        = "19:1--19:36",
 doi          = "10.1145/1592434.1592436",
)