2008-nii-hol-z-tutorial

Phoiv

Le téléchargement nécessite un accès à la bibliothèque YouScribe
Tout savoir sur nos offres

101 pages

English

Le téléchargement nécessite un accès à la bibliothèque YouScribe
Tout savoir sur nos offres

A propos
Informations
Extrait

Description

Informations

Publié par	Phoiv
Nombre de lectures	19
Langue	English

Extrait

Analysing
Z Specifications
with HOL-Z
Burkhart WolffAchim Brucker
Universität des SaarlandesSAP Research,
66041 Saarbrücken, GermanyVincenz-Priessnitz-Str 1
wolff@wjp.cs.uni-sb.de76131 Karlsruhe, Germany
achim.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 speciﬁcation 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 reﬁnement 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 speciﬁcations and formal proof on reﬁnements. 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
reﬁnement 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”, => HOL-CSP)
● data-oriented refinement (“top-down”, => HOL-Z)
● object-oriented refinement (“top-down, MDE”, =>HOL-OCL)
● test-oriented (“reverse-engineering”,
=> HOL-TestGen
● code-verification (“bottom-up”, =>HOL-Boogie/C)
according the needs of my “clients”
Outline of HOL-Z Tutorial
● Motivation and Introduction
● Foundations: Z, HOL and Z-Semantics in HOL
● The HOL-Z System
● Advanced Modelling Scenarios
● Theorem Proving in HOL-Z

● Case Studies
● ConclusionMotivation and Introduction
Motivation and Introduction
Why Z ?
Motivation and Introduction
Why Z ?
● Z is:
– a fairly old, but a mathematically well-defined FM
– ISO standardized (ISO/IEC 13568:2002, Intern. Standard.)
– inofficial publication standard for FM papers
– has nice text books (Spivey's “Z Referece Manual”,
Woodcocks & Davies “Using Z”, ...)
– ... but few proof-environments
(CadiZ (experimental), Z/EVES (outdated),
ProofPower (HOL4 - based),
HOL-Z (Isabelle/HOL - based))Motivation and Introduction
Why Z ?
● what can you do with Z:
– top-down refinement development method
(forward-simulation, backward-simulation)
– generate code, animators (ZAP, ...)
– it can be used for test-case generation, too.
Motivation and Introduction
Why Z in HOL?
● Z Semantics via Embedding in
Higher-Order Logic (HOL)
– Advantage I : Greatly Simplifies Semantics!
– Advantage II: Gives Basis for TOOL-SUPPORT
within HOL provers
(Isabelle, HOL4, ...)