Automated Validation & Verification of UML/OCL Models Using Satisfiability Solvers

Nils Przigoda is a system engineer at the Mobility Division of the Siemens AG, in Braunschweig, Germany. He received two Diploma degrees, one in mathematics and one in computer science, from the University of Bremen, Germany, in 2013. From 2013 to 2017, he did his doctorate in the Group for Computer Architecture at the University of Bremen and finished it in May 2017 with Dr. rer. nat. degree. Afterwards he switched from academia to industry by joining the Siemens AG in 2017. His research interests are in the design of reversible and quantum circuits as well as in the verification of formal models using SAT and SMT solvers. Nils Przigoda published several papers on international conferences such as ASP-DAC, DAC, MODELS and was Mathemacher des Monats (math maker of the month) as announced by the DMV (German Mathematical Society) in November, 2015. Robert Wille is a full professor at the Johannes Kepler University Linz. From 2002 to 2006, Robert Wille studied computer science (Diploma) at the University of Bremen. After successfully completing his doctorate in 2009 (summa cum laude), he worked as postdoc at the University of Bremen and, since 2013, as Senior Researcher in the Cyber-Physical Systems department of the German Research Center for Artificial Intelligence (DFKI). Besides that, he served as lecturer at the University of Applied Science Bremen from 2010 to 2012 and was a guest professor for Technical Computer Science at the University of Potsdam in 2012 as well as for Embedded Systems at the Technical University of Dresden in 2013/2014. In 2014, he completed his habilitation and, since October 2015, he is a full professor at the Johannes Kepler University Linz and head of the Department for Integrated Circuit and System Design. Robert Wille's expertise is in the development of design technologies for various application areas - with a particular focus on the design, verification, and test of circuits and systems for conventional and emerging technologies. Judith Przigoda (née Peters) is a system engineer at the OHB System AG. From 2007 to 2012, she studied computer science at the University of Lübeck, Germany, and received her Master degree in 2012. Afterwards, she moved to the University of Bremen for her doctorate studies. In 2015, she received the A. Richard Newton Young Student Fellow Award of the DAC. Later in 2015, she finished her doctorate (Dr.-Ing.). Her particular interests are embedded systems as well as their design and development. The specification of embedded systems as well as optimizations in the development process are parts of her research. In the recent years, she focused on timing issues in the formal specification of embedded systems. Since 2016, Judith Przigoda works at the satellite ground systems department of the OHB System AG, where her main focus are specifications and system design for satellite systems. Rolf Drechsler received the Diploma and Dr. phil. nat. degrees in computer science from the Johann Wolfgang Goethe University in Frankfurt am Main, Frankfurt am Main, Germany, in 1992 and 1995, respectively. He worked at the Institute of Computer Science, Albert-Ludwigs University, Freiburg im Breisgau, Germany, from 1995 to 2000, and at the Corporate Technology Department, Siemens AG, Munich, Germany, from 2000 to 2001. Since October 2001, Rolf Drechsler is full professor and head of the Group of Computer Architecture, Institute of Computer Science, at the University of Bremen, Germany. In 2011, he additionally became the Director of the Cyber-Physical Systems Group at the German Research Center for Artificial Intelligence (DFKI) in Bremen. His current research interests include the development and design of data structures and algorithms with a focus on circuit and system design. He is an IEEE Fellow.

Introduction.- A Formal Interpretation of UML/OCL.- A Symbolic Formulation for Models.- Structural Aspects.- Behavioral Aspects.- Timing Aspects.- Reducing Instance Sizes with Ground Setting Properties.- Re-utilizing Verification Results of UML/OCL Models.- Conclusion.- Nomenclature.- Appendix A Class Inheritance.- Appendix B An SMT Instance with an unknown Result.- Appendix C Contradictory XOR definitions.- Index.