A Software Engineering Problem.pdf

An Application of Isabelle/???: ???-??? Achim D. Brucker Information Security, ??? Zurich, Switzerland Computer supported Modeling and Reasoning, WS???? Zurich, January ??, ???? Motivation A Short Introduction to ???/??? Turning ???/??? Into a Strong Formal Method ???-??? Conclusions Bibliography Outline Motivation A Short Introduction to ???/??? Turning ???/??? Into a Strong Formal Method Formalizing UML Formalizing OCL ???-??? Conclusions Bibliography Achim D. Brucker An Application of Isabelle/???: ???-??? Motivation A Short Introduction to ???/??? Turning ???/??? Into a Strong Formal Method ???-??? Conclusions Bibliography ?e Situation Today: A So ware Engineering Problem ? So ware systems ? are becoming more and more complex. ? used in safety and security critical applications. ? Formal methods are one way to ensure the correctness.? But, formal methods are hardly used by industry. ? difficult to understand notation ? lack of tool support ? high costs ? Semi-formal methods, especially ???, are ? widely used in industry, but ? not strong enough for a formal methodologies. Achim D. Brucker An Application of Isabelle/???: ???-??? Motivation A Short Introduction to ???/??? Turning ???/??? Into a Strong Formal Method ???-??? Conclusions Bibliography Why Formal Methods are not widely accepted ? ? Only a few formal methods address industrial needs: ? support for object-oriented modeling and programming. ? formal tool support (model checkers, theorem provers, . . . ). ? integration in standard ????? tools and processes. ? Formal methods people and industrial so ware developer are o en speaking different languages. To tackle these challenges we provide a a formal foundation for (supporting object-orientation) for a industrial accepted specification languages (???/???) [?, ?]. Achim D. Brucker An Application of Isabelle/???: ???-??? Motivation A Short Introduction to ???/??? Turning ???/??? Into a Strong Formal Method ???-??? Conclusions Bibliography ?e Unified Modeling