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 higher-order 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, on-line demos, and practical exercises for the participants. At the end of the course participants should be able to formalize functional programs and set-theoretic 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 post-doc 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 co-authored the de-facto 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 Higher-Order Logic' co-authored 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 specification-based testing will be examined. A general theory of behaviour observation based on the domain theory of program semantics will be introduced. Axioms of well-defined behaviour observation methods will be discussed. Problems in testing concurrent systems and component-based 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 agent-oriented 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 graph-based 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 component-based, 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 semi-formal 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 VDM-SL, 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 object-oriented methods, and advocates an transformational and evolutionary approach to constructing formal specifications from informal and then semi-formal 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 pre-post 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 three-step: informal, semi-formal, and formal specifications. It also explains how structured abstract design can be smoothly transformed into object-oriented 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 Springer-Verlag 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 half-day 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 well-founded 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 real-world applications of transformations will be described, including OO component reengineering (a task-specific refactoring), automated translation of JOVIAL to C (legacy software migration), test coverage and profiling analysis, and automated clone detection and removal (for million-line COBOL and Java systems). Short CV Hongjun Zheng, Ph.D., 1997, is performing research on generalized compiler framework for programming languages used in large-scale software evolution and maintenance environment. Dr. Zheng has served as committee member for computer-science 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, co-Chair of the 1997 International Conference on Software Reuse, Program co-Chair of the Working Conference on Reverse Engineering, and Program co-Chair 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 often-used 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 (1973-81): advanced system concepts, control structures and software for telecommunications; Intel, Oregon (1978, 1979): VLSI processor project.   University of Nijmegen, The Netherlands (1981--1994): 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).