TUTORIALS
SCHEDULE
Tutorial 1 
20 Morning  21 Morning September 2004 
Tutorial 2 
20 September 2004 Morning 
Tutorial 3 
20 September 2004 Afternoon 
Tutorial 4 
21 September 2004 Morning 
Tutorial 5 
21 September 2004 Afternoon 
Tutorial 6 
21 September 2004 Afternoon 
The tutorials will be held in two meeting rooms. Participants
will only pay tutorial material fee which is 100 RMB or 13 USD. Because the
rooms can only contain 60 people, we will select the proper participants in
advance. The participants should send their CVs to us before Aug. 31,
2004.

TUTORIAL 1 
Theorem Proving with
Isabelle/HOL

Tobias Nipkow,
Technial University
Munich 
Abstract
Isabelle/HOL is an interactive theorem prover for HOL, a popular
version of higherorder logic. The purpose of this tutorial is to
familiarise students, researchers and practitioners with the basics of
specification and proof in Isabelle/HOL. The course combines traditional
lectures, online demos, and practical exercises for the participants. At
the end of the course participants should be able to formalize functional
programs and settheoretic system models and prove (with Isabelle's help)
simple properties about them. The following topics are covered:
 Datatypes and recursive functions
 Proof by structural induction and by simplification
 Proofs in propositional logic and predicate logic
 Set theory and inductively defined sets
 A language of readable proofs
Short CV
Tobias Nipkow received his Diplom (M.Sc.) in Informatics from the
Technical University Darmstadt in 1982 and his Ph.D. from the University
of Manchester in 1987. He was a postdoc at MIT and Cambridge University
before he became a professor for Theory of Programming at the Technical
University Munich in 1992. He is probably best known for his work in term
rewriting (where he coauthored the defacto standard reference 'Term
Rewriting and All That' with Franz Baader) and his work on the theorem
prover Isabelle (which lead to 'Isabelle/HOL. A Proof Assistant for
HigherOrder Logic' coauthored with Paulson and Wenzel).

TUTORIAL
2 
Formal Theories of
Software Testing

Hong Zhu, Oxford Brookes University, UK 
Abstract
Software testing has been considered as in a lack of solid
theoretical foundation for a long time. In the past 3 decades,
serious efforts have been attempted by researchers to lay a sound
foundation of software testing. A number of formal theories have
been advanced. In this tutorial, we will present a systematic
introduction the formal theories of software testing developed
over the past decades. It will consist of the following three
parts. Part 1 will give a brief introduction to the basic concepts
and methods of software testing. Formal definitions of the
concepts and testing methods will be presented. Part 2 will be
devoted to the axiomatic studies of software test adequacy
criteria. Various axiom systems will be
discussed and analysed.
The assessments of testing methods against axioms will be
reviewed. The results of the investigations on the relationships
between testing and software correctness and reliability through
interpretations of the axiom systems by inductive inferences will
be reported. Part 3 will focus on the problem of test oracle. The
theories and methods of automated test oracle based on the concept
of observation contexts in algebraic specificationbased testing
will be examined. A general theory of behaviour observation based
on the domain theory of program semantics will be introduced.
Axioms of welldefined behaviour observation methods will be
discussed. Problems in testing concurrent systems and
componentbased systems will also be examined.
Short CV
Dr. Hong Zhu is a senior lecturer in computing at the Department
of Computing of Oxford Brookes University in England, where he
chairs the Applied Formal Methods research group. He is also a
visiting professor at the National University of Defence
Technology of China sponsored by the Cheung Kong Scholars
Programme. His current research interests are in area of software
engineering and methodology, which include agentoriented software
development methodology and languages, software testing and
quality assurance, and web engineering.
URL:
http://wwwcms.brookes.ac.uk/~p0072431/zhuhomepage.html

TUTORIAL
3 
Formal Aspects of
Software Architecture

J L Fiadeiro,
University of Leicester 
Abstract
This tutorial presents a formal approach to Software Architecture.
The key architectural concepts  component, connector and
configuration  are formalised in CommUnity, a prototype
architectural description language that has a mathematical
semantics and is supported by a graphical tool. We show how the
principle of superposition can support the separation between
three main architectural concerns  computation, coordination and
distribution. Finally, we show how architectures enable the
incremental development and compositional evolution of systems
through graphbased reconfiguration techniques.
Short CV
José Luiz Fiadeiro is Professor of Software Science and
Engineering at the Department of Computer Science, University of
Leicester, where he leads a research group on Software
Specification and Design. His research interests include software
specification formalisms and methods, especially as applied to
componentbased, reactive systems, and their integration in the
wider area of General Systems Theory. His main contributions have
been in the formalisation of specification and program design
techniques using modal logics (temporal and dynamic), and of their
underlying modularisation principles using Category Theory. His
most recent work has focused on Software Architectures, including
semantics of architectural connectors and the impact of
coordination mechanisms in software evolution. He is now focusing
on the methodological and scientific challenges raised by Service
Oriented Computing. Josi has just published "Categories for
Software Engineering" with Springer, a book that provides all the
mathematical background necessary for the tutorial.

TUTORIAL 4 
Formal Engineering Methods
for Industrial Software Development  An Introduction to the SOFL
Specification Language and Method 
Shaoying Liu 
Abstract
Formal methods have been developed as a rigorous approach to computer
systems development over last three decades, but have been facing
challenges in fighting for industrial acceptance in general. One effective
way to deal with the challenges is to provide a formal but practical
specification language and method resulting from an appropriate
integration of existing formal methods and informal or semiformal methods
commonly used in industry. On the basis of our intensive research and
application experience over the last fifteen years, we have developed the
SOFL specification language and method for software development. As a
specification language, SOFL integrates VDMSL, Data Flow Diagrams, and
Petri Nets to provide an intuitive, rigorous, and comprehensible formal
notation for specifications at different levels. Compared to UML (Unified
Modeling Language), SOFL provides a simpler but systematic mechanism for
precisely defining the functions of system units and their integration,
and therefore avoids the difficulty in managing different kinds of
diagrams and their consistency in UML. As a method, it combines structured
methods and objectoriented methods, and advocates an transformational and
evolutionary approach to constructing formal specifications from informal
and then semiformal specifications; it integrates the idea of formal
proof and commonly used verification and validation techniques, such as
testing and reviews, to offer rigorous but practical verification
techniques.
After a brief description of the general principle of Formal
Engineering Methods, this tutorial offers a systematic introduction to the
SOFL specification language, method, process, and supporting tools.
Specifically, the tutorial is divided into three parts. The first part
includes the brief introduction to Formal Engineering Methods and the SOFL
specification language. In particular, we will focus on the explanation of
the idea of using the graphical notation, known as Condition Data Flow
Diagram (or CDFD for short), to model the architecture of a system, while
using the prepost notation to define the functionality of processes
occurring in CDFDs. The second part explains the SOFL method and process:
how SOFL can be used to construct a formal specification by taking a
threestep: informal, semiformal, and formal specifications. It also
explains how structured abstract design can be smoothly transformed into
objectoriented detailed design and programs. Finally, the third part of
the tutorial presents Rigorous Review and Specification Testing as two
practical techniques for verification and validation of specifications,
and demonstrates several tools we have built to support SOFL. Formal
Engineering Method for complex systems development.
Short CV
Shaoying Liu is a Professor in the Department of Computer Science at Hosei
University. He received the Ph.D in Formal Methods from the University of
Manchester, U.K. in 1992, and has 20 years experience in both research and
education in the area of Software Engineering and Formal Methods at Xi'an
Jiaotong University in China, University of York and Royal Holloway and
Bedford New College of the University of London in the U.K., and Hiroshima
City University and Hosei Univeristy in Japan, respectively. He was
invited as a Visiting Research Fellow by The Queen's University of Belfast
from December 1994 to February 1995, and an academic visitor to Oxford
University from December 1998 to February 1999. From 2003 he is also
invited as a Guest Professor to Shanghai Jiaotong University and Shanghai
University in China, respectively. Liu has published a book on Formal
Engineering Methods with SpringerVerlag in 2004 and published over 70
research papers in journals and international conferences. He is a member
of IEEE Computer Society, ACM, and Japan Society for Software Science and
Technology.
URL: http://cis.k.hosei.ac.jp/~sliu/

TUTORIAL
5 
Program Transformation
Systems: Theory and
Practice for Software Generation, Maintenance and Reengineering 
Hongjun Zheng
and Ira
Baxter, Semantic Designs, Inc., Austin, USA 
Abstract
This halfday tutorial provides an integrated view, built
over 20 years, of program transformation systems, on concepts,
vocabulary, mechanisms, and discussion of some existing
systems from this view. Software engineering and software
maintenance automation support will come from such
semantically founded tools.
Of particular interest to this conference, the tutorial
will elaborate a wellfounded theory of software maintenance
using the transformational perspective. It will describe a set of
practical transformation systems, and provide some application
experience based on DMS, the transformation toolset that
Semantic Designs is building. A number of realworld
applications of transformations will be described, including
OO component reengineering (a taskspecific refactoring),
automated translation of JOVIAL to C (legacy software
migration), test coverage and profiling analysis, and
automated clone detection and removal (for millionline COBOL
and Java systems).
Short CV
Hongjun Zheng, Ph.D., 1997, is performing research on
generalized compiler framework for programming languages used
in largescale software evolution and maintenance
environment. Dr. Zheng has served as committee member for
computerscience conferences, especially those focused on
software engineering and formal methods. He is member of ACM
and senior member of IEEE.
Ira Baxter has been building system software since 1969. He
acquired his Ph.D. with emphasis on software engineering and
reuse from the University of California at Irvine in 1990.
Dr. Baxter has been invited speaker at SSR'99, coChair of
the 1997 International Conference on Software Reuse, Program
coChair of the Working Conference on Reverse Engineering,
and Program coChair of the 2002 International Conference on
Software Maintenance, and has been a PC member of the
International Conference on Software Maintenance for a number
of years.

TUTORIAL
6 
Functional Predicate
Calculus and Generic Functionals in
Software Engineering 
Raymond Boute, University of Ghent, Belgium 
Abstract
By formal calculation we mean expression manipulation on the basis
of
syntax, ``letting the symbols do the work''. This is a valuable
complement
to (some might even say, replacement for) intuitive reasoning,
especially
when exploring new grounds where intuition is (still) clueless.
By this
tutorial, we wish to open for software engineers the same
possibilities
that calculus has offered to physicists and engineers in more
classical
areas (mechanical, electrical, ...).
This tutorial presents the principles of two interwoven formalisms
and
illustrates their applications to formal reasoning in various
aspects of
software engineering.
The first formalism is a discipline for designing generic
functionals,
some of which constitute generalizations of oftenused functionals
in
mathematics (composition, restriction, inverse, etc.), whereas
others are
new. A small collection of generic functionals and their
algebraic
properties appears sufficient for providing considerable
expressive and
calculational power in a wide diversity of fields, illustrated
with
examples in program transformation, data types, program semantics,
databases.
The second formalism is a functional predicate calculus, thus called
because predicates and quantifiers are functions and all algebraic laws
are
derived from the basic quantifier axioms using the axioms for function
equality. The laws are most elegantly expressed using generic functionals
and, conversely, the predicate calculus is most convenient for proving the
properties of the generic functionals, which explains the synergy. The
collection of laws necessary for conveniently covering the diversity of
logical arguments encountered in practice is larger than found in
traditional logic textbooks (a fact also made evident by the extensive
list
in Gries and Schneider's ``A Logical Introduction to Discrete
Math''). However, it is still very manageable, especially by proper
grouping. Its power resides in guiding the flow of the calculations by
the
shape of the formulas and, if used in this fashion, it makes the
development of logical arguments in continuous mathematics and in discrete
mathematics remarkably similar and, above all, easy and reliable.
This is illustrated by (a) general methods for reasoning about
functions, relations and proofs by induction (perhaps one of the most
important proof techniques in software engineering) and (b) showing how
theories of programming that are useful in program construction and
verification can be calculationally derived from a very simple model based
on ``program equations'' in a way similar to systems modelling in
classical
engineering. Other examples are kept available for illustration and
discussion as time permits.
Short CV
Education:
Ghent University: M.Sc.
Electrical/Mechanical Engineering (1966),
Electronics (1968).
Stanford University: M.Sc. (1969) and Ph.D.
(1973) in Electrical
Engineering and Computer Science.
Employment:
Bell Telephone Mfg. Cy., Belgium
(197381): advanced system concepts,
control structures and software for telecommunications; Intel, Oregon
(1978, 1979): VLSI processor project.
University of Nijmegen, The Netherlands
(19811994): full professor of
Informatics (teaching: computer architecture, operating systems, VLSI
design, computer networks and digital satellite communications; research:
functional programming, declarative functional formalisms).
University of Ghent, Belgium (since
1994): full professor of Computer
Science (teaching, research: mathematics for computer science, application
of formal methods in computing and electronics).

