2008-nii-hol-z-tutorial

Analysing Z Specificationswith HOL-Z Burkhart WolffAchim BruckerUniversität des SaarlandesSAP Research,66041 Saarbrücken, GermanyVincenz-Priessnitz-Str 1wolff@wjp.cs.uni-sb.de76131 Karlsruhe, Germanyachim.brucker@sap.com Abstract The increasing complexity of todays software systems makes modeling an important phase during the software development process, both, on the level of requirement analysis and the system design. The ISO-standardized specification language Z can be used for a formal underpinning of these activities. In particular, the Z Method allows for relating Requirements and System Designs via formal refinement notions. In this tutorial we present the interactive theorem prover environment HOL-Z (built as plug-in of Isabelle/HOL) that supports formal reasoning over Z specifications and formal proof on refinements. The system achieved meanwhile a reasonable degree of auto–mation such that several substantial case studies (CVS Server, DARMA funded by Hitachi) had been realized, involving both refinement as well as temporal reasoning. My Credo's and My Background ● Thesis: THERE IS NO SINGLE FORMAL METHOD ● Thesis: FORMAL METHODS MUST BE INTEGRATED INTO A (COMPANY-SPECIFIC) SE – WORKFLOW● Thesis: TOOL-CHAINS MUST FOLLOW METHOD AND WORKFLOW/PRAGMATICS, I.E. THE METHODOLOGY. My Credo's and My Background ● I am a Formal Methods Engineer.I designed Tool-Chains for:● process-oriented refinement(“top-down”, => ...